diff --git a/src/codegen/dead_storage.rs b/src/codegen/dead_storage.rs index b26942240..abf808efd 100644 --- a/src/codegen/dead_storage.rs +++ b/src/codegen/dead_storage.rs @@ -141,11 +141,11 @@ fn reaching_definitions(cfg: &mut ControlFlowGraph) -> (Vec>>, ); for edge in cfg.blocks[block_no].successors() { + let mut changed = false; + if !block_vars.contains_key(&edge) { - blocks_todo.insert(edge); - block_vars.insert(edge, vec![vars.clone()]); + changed |= block_vars.insert(edge, vec![vars.clone()]).is_none(); } else if block_vars[&edge][0] != vars { - blocks_todo.insert(edge); let block_vars = block_vars .get_mut(&edge) .expect("block vars must contain edge"); @@ -155,10 +155,11 @@ fn reaching_definitions(cfg: &mut ControlFlowGraph) -> (Vec>>, for (incoming_def, storage) in defs { if !entry.contains_key(incoming_def) { entry.insert(*incoming_def, storage.clone()); + changed = true; } } } else { - block_vars[0].vars.insert(*var_no, defs.clone()); + changed |= block_vars[0].vars.insert(*var_no, defs.clone()).is_none(); } } @@ -166,9 +167,14 @@ fn reaching_definitions(cfg: &mut ControlFlowGraph) -> (Vec>>, for store in &vars.stores { if !block_vars[0].stores.iter().any(|(def, _)| *def == store.0) { block_vars[0].stores.push(store.clone()); + changed = true; } } } + + if changed { + blocks_todo.insert(edge); + } } } diff --git a/src/codegen/reaching_definitions.rs b/src/codegen/reaching_definitions.rs index 24ff49294..c0234ff19 100644 --- a/src/codegen/reaching_definitions.rs +++ b/src/codegen/reaching_definitions.rs @@ -65,19 +65,27 @@ pub fn find(cfg: &mut ControlFlowGraph) { for edge in cfg.blocks[block_no].successors() { if cfg.blocks[edge].defs != vars { - blocks_todo.insert(edge); + let mut changed = false; + // merge incoming set for (var_no, defs) in &vars { if let Some(entry) = cfg.blocks[edge].defs.get_mut(var_no) { for (incoming_def, incoming_modified) in defs { if let Some(e) = entry.get_mut(incoming_def) { - *e |= *incoming_modified; + if !*e && *incoming_modified { + *e = true; + changed = true; + } } else { - entry.insert(*incoming_def, *incoming_modified); + changed |= + entry.insert(*incoming_def, *incoming_modified).is_none(); } } } else { - cfg.blocks[edge].defs.insert(*var_no, defs.clone()); + changed |= cfg.blocks[edge] + .defs + .insert(*var_no, defs.clone()) + .is_none(); } // If a definition from a block executed later reaches this block, @@ -85,10 +93,14 @@ pub fn find(cfg: &mut ControlFlowGraph) { // common subexpression elimination. for (incoming_def, _) in defs { if incoming_def.block_no >= edge { - cfg.blocks[edge].loop_reaching_variables.insert(*var_no); + changed |= cfg.blocks[edge].loop_reaching_variables.insert(*var_no); } } } + + if changed { + blocks_todo.insert(edge); + } } } } diff --git a/tests/codegen_testcases/solidity/do_while_break_2.sol b/tests/codegen_testcases/solidity/do_while_break_2.sol new file mode 100644 index 000000000..875f176be --- /dev/null +++ b/tests/codegen_testcases/solidity/do_while_break_2.sol @@ -0,0 +1,24 @@ +// RUN: --target polkadot --emit cfg + +contract C { + // CHECK: C::function::f + function f() public pure { + uint a = 0; + while (true) { + do { + break; + a = 2; + } while (true); + a = 1; + break; + } + assert(a == 1); + } +} +// ==== +// SMTEngine: all +// SMTSolvers: z3 +// ---- +// Warning 5740: (95-100): Unreachable code. +// Warning 5740: (114-118): Unreachable code. +// Info 1391: CHC: 1 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them. diff --git a/tests/codegen_testcases/solidity/do_while_break_2_fail.sol b/tests/codegen_testcases/solidity/do_while_break_2_fail.sol new file mode 100644 index 000000000..d5eed4b2e --- /dev/null +++ b/tests/codegen_testcases/solidity/do_while_break_2_fail.sol @@ -0,0 +1,24 @@ +// RUN: --target polkadot --emit cfg + +contract C { + // CHECK: C::function::f + function f() public pure { + uint a = 0; + while (true) { + do { + break; + a = 2; + } while (true); + a = 1; + break; + } + assert(a == 2); + } +} +// ==== +// SMTEngine: all +// SMTSolvers: z3 +// ---- +// Warning 5740: (95-100): Unreachable code. +// Warning 5740: (114-118): Unreachable code. +// Warning 6328: (147-161): CHC: Assertion violation happens here.\nCounterexample:\n\na = 1\n\nTransaction trace:\nC.constructor()\nC.f()