Fix two infinite loops in codegen (#1779)

This PR fixes infinite lops in the reaching definitions and dead storage
code.

The two added test files are based on ones from Solidity:
-
https://github.com/ethereum/solidity/blob/develop/test/libsolidity/smtCheckerTests/loops/do_while_break_2.sol
-
https://github.com/ethereum/solidity/blob/develop/test/libsolidity/smtCheckerTests/loops/do_while_break_2_fail.sol

If you add `dbg!(block_no)` between the next two lines and run Solang on
either of the test files, you will find that a block is visited
repeatedly:
https://github.com/hyperledger-solang/solang/blob/279ee911260d74c78acace41d753c5376a7e942e/src/codegen/reaching_definitions.rs#L56-L57

If you fix that infinite loop and add `dbg!(block_no)` between the next
two lines, you will again find that a block is visited repeatedly:
https://github.com/hyperledger-solang/solang/blob/279ee911260d74c78acace41d753c5376a7e942e/src/codegen/dead_storage.rs#L109-L110

In both cases, the problem appears to be that edges are added to the
`blocks_todo` queue unconditionally.

My understanding of these algorithms is that they try to iterate to a
fixpoint. Hence, I changed each loop so that:
- a flag records whether a _state change_ has occurred
- at the end of each loop iteration, the edge is added to the queue only
if the flag is set

Furthermore, I analyzed each loop to try to determine what constitutes a
state change. On this point, I invite scrutiny.

Nits are welcome on anything, though.

Signed-off-by: Samuel Moelius <sam@moeli.us>

Author: smoelius

src/codegen/dead_storage.rs

@@ -141,11 +141,11 @@ fn reaching_definitions(cfg: &mut ControlFlowGraph) -> (Vec<Vec<Vec<Transfer>>>,
         );
 
         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,20 +155,26 @@ fn reaching_definitions(cfg: &mut ControlFlowGraph) -> (Vec<Vec<Vec<Transfer>>>,
                         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();
                     }
                 }
 
                 // merge storage stores
                 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);
+            }
         }
     }
 

src/codegen/reaching_definitions.rs

@@ -65,30 +65,42 @@ 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,
                     // this is a loop. This is an analysis we use later at the
                     // 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);
+                }
             }
         }
     }

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.

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()