Fix regression tests

Author: qinheping

regression/cbmc/Quantifiers1/quantifier-with-function-call.desc

@@ -1,9 +1,8 @@
 CORE
 quantifier-with-function-call.c
 
-^EXIT=134$
+^EXIT=6$
 ^SIGNAL=0$
-^Invariant check failed
-^Reason: quantifier must not contain side effects
+quantifier must not contain function calls
 --
 ^warning: ignoring

regression/validate-trace-xml-schema/check.py

@@ -75,6 +75,7 @@
     ['integer-assignments1', 'test.desc'],
     # this test is expected to abort, thus producing invalid XML
     ['String_Abstraction17', 'test.desc']
+    ['Quantifiers1', 'quantifier-with-function-call.desc']
 ]))
 
 # TODO maybe consider looking them up on PATH, but direct paths are

src/ansi-c/c_typecheck_expr.cpp

@@ -316,10 +316,16 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
       }
     }
 
-    if(expr.id() == ID_lambda && has_subexpr(where, ID_side_effect))
+    if(has_subexpr(
+      where,
+      [&](const exprt &subexpr)
+      {
+        return can_cast_expr<side_effect_exprt>(subexpr) &&
+               can_cast_expr<side_effect_expr_function_callt>(subexpr);
+      }))
     {
       error().source_location = expr.source_location();
-      error() << "lambda expressions must not contain side effects" << eom;
+      error() << "quantifier must not contain function calls" << eom;
       throw 0;
     }
 

src/ansi-c/goto-conversion/goto_clean_expr.cpp

@@ -48,6 +48,140 @@ static symbol_exprt find_base_symbol(const exprt &expr)
   }
 }
 
+static exprt convert_statement_expression(
+  const quantifier_exprt &qex,
+  const code_expressiont &code,
+  const irep_idt &mode,
+  goto_convertt &converter)
+{
+  goto_programt where;
+  converter.goto_convert(code, where, mode);
+  where.compute_location_numbers();
+
+  natural_loops_mutablet natural_loops(where);
+  INVARIANT(
+    natural_loops.loop_map.size() == 0,
+    "quantifier must not contain side effects");
+
+  // `last` is the instruction corresponding to the last expression in the
+  // statement expression.
+  goto_programt::const_targett last;
+  for(goto_programt::const_targett it = where.instructions.begin();
+      it != where.instructions.end();
+      ++it)
+  {
+    // `last` is an other-instruction.
+    if(it->is_other())
+    {
+      last = it;
+    }
+  }
+  auto last_expr =
+    expr_try_dynamic_cast<code_expressiont>(last->get_other())->expression();
+
+  // `pathes` contains all the `targett` we are iterating over.
+  std::vector<goto_programt::const_targett> pathes;
+  pathes.push_back(where.instructions.begin());
+  std::vector<std::pair<exprt, replace_symbolt>> path_conditions_and_value_maps;
+  path_conditions_and_value_maps.push_back(
+    std::make_pair(true_exprt(), replace_symbolt()));
+
+  std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
+  // All bounded variables are local.
+  declared_symbols.insert(qex.variables().begin(), qex.variables().end());
+
+  exprt res = true_exprt();
+
+  // Visit the quantifeir body along `pathes`.
+  while(!pathes.empty())
+  {
+    auto &current_it = pathes.back();
+    auto &path_condition = path_conditions_and_value_maps.back().first;
+    auto &value_map = path_conditions_and_value_maps.back().second;
+    INVARIANT(
+      current_it != where.instructions.end(),
+      "Quantifier body must have a unique end expression.");
+
+    // Add all local-declared symbols into `declared_symbols`.
+    if(current_it->is_decl())
+    {
+      declared_symbols.insert(current_it->decl_symbol());
+    }
+    // ASSIGN lhs := rhs
+    // Add the replace lhr <- value_map(rhs) to the current value_map.
+    if(current_it->is_assign())
+    {
+      // Check that if lhs is a declared symbol.
+      auto lhs = current_it->assign_lhs();
+      INVARIANT(
+        declared_symbols.count(find_base_symbol(lhs)),
+        "quantifier must not contain side effects");
+      exprt rhs = current_it->assign_rhs();
+      INVARIANT(
+        !has_subexpr(rhs, ID_function_call),
+        "quantifier must not contain side effects");
+      value_map.replace(rhs);
+      value_map.set(to_symbol_expr(current_it->assign_lhs()), rhs);
+    }
+    // GOTO label
+    // -----------
+    // Move the current targett to label.
+    // or
+    // IF cond GOTO label
+    // ----------
+    // Move the current targett to targett+1 with path condition
+    // path_condition && !cond;
+    // and add a new path starting from label with path condition
+    // path_condition && cond.
+    if(current_it->is_goto())
+    {
+      if(current_it->has_condition())
+      {
+        auto next_it = current_it->targets.front();
+        exprt copy_path_condition = path_condition;
+        replace_symbolt copy_symbol_map = value_map;
+        path_condition =
+          and_exprt(path_condition, not_exprt(current_it->condition()));
+        path_conditions_and_value_maps.push_back(std::make_pair(
+          and_exprt(copy_path_condition, current_it->condition()),
+          copy_symbol_map));
+        current_it++;
+        pathes.push_back(next_it);
+      }
+      else
+      {
+        current_it = current_it->targets.front();
+      }
+      continue;
+    }
+    // EXPRESSION(expr)
+    // The last instruction is an exression statement.
+    // We add the predicate path_condition ==> value_map(expr) to res.
+    if(current_it == last)
+    {
+      exprt copy_of_last_expr = last_expr;
+      value_map.replace(copy_of_last_expr);
+      res = and_exprt(res, implies_exprt(path_condition, copy_of_last_expr));
+      path_conditions_and_value_maps.pop_back();
+      pathes.pop_back();
+      continue;
+    }
+    // DEAD symbol
+    // Remove symbol from declared_symbols.
+    if(current_it->is_dead())
+    {
+      declared_symbols.erase(current_it->decl_symbol());
+    }
+    // Unsupported instructions.
+    if(current_it->is_function_call())
+    {
+      UNREACHABLE;
+    }
+    current_it++;
+  }
+  return res;
+}
+
 symbol_exprt goto_convertt::make_compound_literal(
   const exprt &expr,
   goto_programt &dest,
@@ -491,137 +625,7 @@ goto_convertt::clean_expr_resultt goto_convertt::clean_expr(
       code.operands()[0].get_named_sub()[ID_statement].id() ==
         ID_statement_expression)
     {
-      goto_programt where;
-      goto_convert(code, where, mode);
-      where.compute_location_numbers();
-
-      natural_loops_mutablet natural_loops(where);
-      INVARIANT(
-        natural_loops.loop_map.size() == 0,
-        "quantifier must not contain side effects");
-
-      // `last` is the instruction corresponding to the last expression in the
-      // statement expression.
-      goto_programt::const_targett last;
-      for(goto_programt::const_targett it = where.instructions.begin();
-          it != where.instructions.end();
-          ++it)
-      {
-        // `last` is an other-instruction.
-        if(it->is_other())
-        {
-          last = it;
-        }
-      }
-      auto last_expr =
-        expr_try_dynamic_cast<code_expressiont>(last->get_other())
-          ->expression();
-
-      // `pathes` contains all the `targett` we are iterating over.
-      std::vector<goto_programt::const_targett> pathes;
-      pathes.push_back(where.instructions.begin());
-      std::vector<std::pair<exprt, replace_symbolt>>
-        path_conditions_and_value_maps;
-      path_conditions_and_value_maps.push_back(
-        std::make_pair(true_exprt(), replace_symbolt()));
-
-      std::unordered_set<symbol_exprt, irep_hash> declared_symbols;
-      // All bounded variables are local.
-      declared_symbols.insert(qex.variables().begin(), qex.variables().end());
-
-      exprt res = true_exprt();
-
-      // Visit the quantifeir body along `pathes`.
-      while(!pathes.empty())
-      {
-        auto &current_it = pathes.back();
-        auto &path_condition = path_conditions_and_value_maps.back().first;
-        auto &value_map = path_conditions_and_value_maps.back().second;
-        INVARIANT(
-          current_it != where.instructions.end(),
-          "Quantifier body must have a unique end expression.");
-
-        // Add all local-declared symbols into `declared_symbols`.
-        if(current_it->is_decl())
-        {
-          declared_symbols.insert(current_it->decl_symbol());
-        }
-        // ASSIGN lhs := rhs
-        // Add the replace lhr <- value_map(rhs) to the current value_map.
-        if(current_it->is_assign())
-        {
-          // Check that if lhs is a declared symbol.
-          auto lhs = current_it->assign_lhs();
-          INVARIANT(
-            declared_symbols.count(find_base_symbol(lhs)),
-            "quantifier must not contain side effects");
-          exprt rhs = current_it->assign_rhs();
-          INVARIANT(
-            !has_subexpr(rhs, ID_function_call),
-            "quantifier must not contain side effects");
-          value_map.replace(rhs);
-          value_map.set(to_symbol_expr(current_it->assign_lhs()), rhs);
-        }
-        // GOTO label
-        // -----------
-        // Move the current targett to label.
-        // or
-        // IF cond GOTO label
-        // ----------
-        // Move the current targett to targett+1 with path condition
-        // path_condition && !cond;
-        // and add a new path starting from label with path condition
-        // path_condition && cond.
-        if(current_it->is_goto())
-        {
-          if(current_it->has_condition())
-          {
-            auto next_it = current_it->targets.front();
-            exprt copy_path_condition = path_condition;
-            replace_symbolt copy_symbol_map = value_map;
-            path_condition = simplify_expr(
-              and_exprt(path_condition, not_exprt(current_it->condition())),
-              ns);
-            path_conditions_and_value_maps.push_back(std::make_pair(
-              simplify_expr(
-                and_exprt(copy_path_condition, current_it->condition()), ns),
-              copy_symbol_map));
-            current_it++;
-            pathes.push_back(next_it);
-          }
-          else
-          {
-            current_it = current_it->targets.front();
-          }
-          continue;
-        }
-        // EXPRESSION(expr)
-        // The last instruction is an exression statement.
-        // We add the predicate path_condition ==> value_map(expr) to res.
-        if(current_it == last)
-        {
-          exprt copy_of_last_expr = last_expr;
-          value_map.replace(copy_of_last_expr);
-          res =
-            and_exprt(res, implies_exprt(path_condition, copy_of_last_expr));
-          path_conditions_and_value_maps.pop_back();
-          pathes.pop_back();
-          continue;
-        }
-        // DEAD symbol
-        // Remove symbol from declared_symbols.
-        if(current_it->is_dead())
-        {
-          declared_symbols.erase(current_it->decl_symbol());
-        }
-        // Unsupported instructions.
-        if(current_it->is_function_call())
-        {
-          UNREACHABLE;
-        }
-        current_it++;
-      }
-
+      auto res = convert_statement_expression(qex, code, mode, *this);
       qex.where() = res;
       return clean_expr(res, mode, result_is_used);
     }