Allows simplification of expressions containing non-const

Previously, abstract_objectt::expression_transform returned top
whenever one of the subexpressions of an operator was non-const,
which didn't allow simplification in situations like
int x = 0;
int y = nondet_int();
int z = x * y;

The old behavior would've replaced x * y with 0 * y,
with this change it will correctly simplify it to 0 instead.

Author: hannes-steffenhagen-diffblue

regression/goto-analyzer-simplify/simplify-complex-expression/main.c

@@ -0,0 +1,11 @@
+int nondet_int(void);
+
+int main(void)
+{
+  int r = nondet_int();
+  r = r + 1;
+  if(r == 2) {
+    return 1;
+  }
+  return 0;
+}

regression/goto-analyzer-simplify/simplify-complex-expression/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--variable
+r == 2
+^SIGNAL=0$
+^EXIT=6$
+--
+--
+
+Checks for a bug that occurred while changing the simplifier,
+where a variable would be replaced by the RHS of its last assignment,
+even if the value of that expression had changed since then;
+Most egregiously when the RHS contained the symbol on the LHS (thus leading
+to a recursive definition).

regression/goto-analyzer-simplify/simplify-multiply-by-zero/main.c

@@ -0,0 +1,8 @@
+int nondet_int(void);
+
+int main(void)
+{
+  int K = nondet_int();
+  int x = 0;
+  return K * x;
+}

regression/goto-analyzer-simplify/simplify-multiply-by-zero/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+"--variable"
+^SIGNAL=0$
+^EXIT=6$
+main#return_value = 0;
+--
+--
+Tests that a multiplication
+of variable*variable can be simplified
+if one of the variables can be evaluated to 0.

src/analyses/variable-sensitivity/abstract_object.cpp

@@ -184,17 +184,18 @@ abstract_object_pointert abstract_objectt::expression_transform(
 {
   exprt constant_replaced_expr=expr;
   constant_replaced_expr.operands().clear();
+
+  // Two passes over the expression - one for simplification,
+  // another to check if there are any top subexpressions left
   for(const exprt &op : expr.operands())
   {
     abstract_object_pointert lhs_abstract_object=environment.eval(op, ns);
     const exprt &lhs_value=lhs_abstract_object->to_constant();
-
     if(lhs_value.is_nil())
     {
-      // One of the values is not resolvable to a constant
-      // so we can't really do anything more with
-      // this expression and should just return top for the result
-      return environment.abstract_object_factory(expr.type(), ns, true, false);
+      // do not give up if a sub-expression is not a constant,
+      // because the whole expression may still be simplified in some cases
+      constant_replaced_expr.operands().push_back(op);
     }
     else
     {
@@ -204,7 +205,19 @@ abstract_object_pointert abstract_objectt::expression_transform(
     }
   }
 
-  exprt simplified=simplify_expr(constant_replaced_expr, ns);
+  exprt simplified = simplify_expr(constant_replaced_expr, ns);
+
+  for(const exprt &op : simplified.operands())
+  {
+    abstract_object_pointert lhs_abstract_object = environment.eval(op, ns);
+    const exprt &lhs_value = lhs_abstract_object->to_constant();
+    if(lhs_value.is_nil())
+    {
+      return environment.abstract_object_factory(
+        simplified.type(), ns, true, false);
+    }
+  }
+
   return environment.abstract_object_factory(simplified.type(), simplified, ns);
 }