Merge pull request #2085 from tautschnig/from_expr-cleanup

Use from_{expr,type} matching the language of the expression/type

Author: Daniel Kroening

src/analyses/constant_propagator.cpp

@@ -13,6 +13,7 @@ Author: Peter Schrammel
 
 #ifdef DEBUG
 #include <iostream>
+#include <util/format_expr.h>
 #endif
 
 #include <util/find_symbols.h>
@@ -219,7 +220,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
   const namespacet &ns)
 {
 #ifdef DEBUG
-  std::cout << "two_way_propagate_rec: " << from_expr(ns, "", expr) << '\n';
+  std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
 #endif
 
   bool change=false;
@@ -379,7 +380,7 @@ void constant_propagator_domaint::valuest::output(
 
   for(const auto &p : replace_const.expr_map)
   {
-    out << ' ' << p.first << "=" << from_expr(ns, "", p.second) << '\n';
+    out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
   }
 }
 

src/analyses/goto_check.cpp

@@ -28,7 +28,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/cprover_prefix.h>
 #include <util/options.h>
 
-#include <langapi/language_util.h>
+#include <langapi/language.h>
+#include <langapi/mode.h>
 
 #include "local_bitvector_analysis.h"
 
@@ -80,9 +81,8 @@ class goto_checkt
   void check_rec(
     const exprt &expr,
     guardt &guard,
-    bool address,
-    const irep_idt &mode);
-  void check(const exprt &expr, const irep_idt &mode);
+    bool address);
+  void check(const exprt &expr);
 
   void bounds_check(const index_exprt &expr, const guardt &guard);
   void div_by_zero_check(const div_exprt &expr, const guardt &guard);
@@ -94,8 +94,7 @@ class goto_checkt
     const dereference_exprt &expr,
     const guardt &guard,
     const exprt &access_lb,
-    const exprt &access_ub,
-    const irep_idt &mode);
+    const exprt &access_ub);
   void integer_overflow_check(const exprt &expr, const guardt &guard);
   void conversion_check(const exprt &expr, const guardt &guard);
   void float_overflow_check(const exprt &expr, const guardt &guard);
@@ -141,6 +140,8 @@ class goto_checkt
   typedef std::pair<exprt, exprt> allocationt;
   typedef std::list<allocationt> allocationst;
   allocationst allocations;
+
+  irep_idt mode;
 };
 
 void goto_checkt::collect_allocations(
@@ -917,8 +918,7 @@ void goto_checkt::pointer_validity_check(
   const dereference_exprt &expr,
   const guardt &guard,
   const exprt &access_lb,
-  const exprt &access_ub,
-  const irep_idt &mode)
+  const exprt &access_ub)
 {
   if(!enable_pointer_check)
     return;
@@ -1274,7 +1274,8 @@ void goto_checkt::add_guarded_claim(
 
     goto_programt::targett t=new_code.add_instruction(type);
 
-    std::string source_expr_string=from_expr(ns, "", src_expr);
+    std::string source_expr_string;
+    get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
 
     t->guard.swap(new_expr);
     t->source_location=source_location;
@@ -1283,11 +1284,7 @@ void goto_checkt::add_guarded_claim(
   }
 }
 
-void goto_checkt::check_rec(
-  const exprt &expr,
-  guardt &guard,
-  bool address,
-  const irep_idt &mode)
+void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 {
   // we don't look into quantifiers
   if(expr.id()==ID_exists || expr.id()==ID_forall)
@@ -1298,26 +1295,26 @@ void goto_checkt::check_rec(
     if(expr.id()==ID_dereference)
     {
       assert(expr.operands().size()==1);
-      check_rec(expr.op0(), guard, false, mode);
+      check_rec(expr.op0(), guard, false);
     }
     else if(expr.id()==ID_index)
     {
       assert(expr.operands().size()==2);
-      check_rec(expr.op0(), guard, true, mode);
-      check_rec(expr.op1(), guard, false, mode);
+      check_rec(expr.op0(), guard, true);
+      check_rec(expr.op1(), guard, false);
     }
     else
     {
       forall_operands(it, expr)
-        check_rec(*it, guard, true, mode);
+        check_rec(*it, guard, true);
     }
     return;
   }
 
   if(expr.id()==ID_address_of)
   {
     assert(expr.operands().size()==1);
-    check_rec(expr.op0(), guard, true, mode);
+    check_rec(expr.op0(), guard, true);
     return;
   }
   else if(expr.id()==ID_and || expr.id()==ID_or)
@@ -1334,7 +1331,7 @@ void goto_checkt::check_rec(
         throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
               op.pretty();
 
-      check_rec(op, guard, false, mode);
+      check_rec(op, guard, false);
 
       if(expr.id()==ID_or)
         guard.add(not_exprt(op));
@@ -1359,19 +1356,19 @@ void goto_checkt::check_rec(
       throw msg;
     }
 
-    check_rec(expr.op0(), guard, false, mode);
+    check_rec(expr.op0(), guard, false);
 
     {
       guardt old_guard=guard;
       guard.add(expr.op0());
-      check_rec(expr.op1(), guard, false, mode);
+      check_rec(expr.op1(), guard, false);
       guard.swap(old_guard);
     }
 
     {
       guardt old_guard=guard;
       guard.add(not_exprt(expr.op0()));
-      check_rec(expr.op2(), guard, false, mode);
+      check_rec(expr.op2(), guard, false);
       guard.swap(old_guard);
     }
 
@@ -1384,7 +1381,7 @@ void goto_checkt::check_rec(
     const dereference_exprt &deref=
       to_dereference_expr(member.struct_op());
 
-    check_rec(deref.op0(), guard, false, mode);
+    check_rec(deref.op0(), guard, false);
 
     exprt access_ub=nil_exprt();
 
@@ -1394,13 +1391,13 @@ void goto_checkt::check_rec(
     if(member_offset.is_not_nil() && size.is_not_nil())
       access_ub=plus_exprt(member_offset, size);
 
-    pointer_validity_check(deref, guard, member_offset, access_ub, mode);
+    pointer_validity_check(deref, guard, member_offset, access_ub);
 
     return;
   }
 
   forall_operands(it, expr)
-    check_rec(*it, guard, false, mode);
+    check_rec(*it, guard, false);
 
   if(expr.id()==ID_index)
   {
@@ -1462,21 +1459,21 @@ void goto_checkt::check_rec(
       to_dereference_expr(expr),
       guard,
       nil_exprt(),
-      size_of_expr(expr.type(), ns),
-      mode);
+      size_of_expr(expr.type(), ns));
 }
 
-void goto_checkt::check(const exprt &expr, const irep_idt &mode)
+void goto_checkt::check(const exprt &expr)
 {
   guardt guard;
-  check_rec(expr, guard, false, mode);
+  check_rec(expr, guard, false);
 }
 
 void goto_checkt::goto_check(
   goto_functiont &goto_function,
-  const irep_idt &mode)
+  const irep_idt &_mode)
 {
   assertions.clear();
+  mode = _mode;
 
   local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
   local_bitvector_analysis=&local_bitvector_analysis_obj;
@@ -1497,7 +1494,7 @@ void goto_checkt::goto_check(
        i.is_target())
       assertions.clear();
 
-    check(i.guard, mode);
+    check(i.guard);
 
     // magic ERROR label?
     for(const auto &label : error_labels)
@@ -1523,20 +1520,20 @@ void goto_checkt::goto_check(
 
       if(statement==ID_expression)
       {
-        check(i.code, mode);
+        check(i.code);
       }
       else if(statement==ID_printf)
       {
         forall_operands(it, i.code)
-          check(*it, mode);
+          check(*it);
       }
     }
     else if(i.is_assign())
     {
       const code_assignt &code_assign=to_code_assign(i.code);
 
-      check(code_assign.lhs(), mode);
-      check(code_assign.rhs(), mode);
+      check(code_assign.lhs());
+      check(code_assign.rhs());
 
       // the LHS might invalidate any assertion
       invalidate(code_assign.lhs());
@@ -1576,7 +1573,7 @@ void goto_checkt::goto_check(
       }
 
       forall_operands(it, code_function_call)
-        check(*it, mode);
+        check(*it);
 
       // the call might invalidate any assertion
       assertions.clear();
@@ -1585,7 +1582,7 @@ void goto_checkt::goto_check(
     {
       if(i.code.operands().size()==1)
       {
-        check(i.code.op0(), mode);
+        check(i.code.op0());
         // the return value invalidate any assertion
         invalidate(i.code.op0());
       }

src/analyses/goto_rw.cpp

@@ -633,6 +633,8 @@ void guarded_range_domaint::output(
     if(itr!=begin())
       out << ";";
     out << itr->first << ":" << itr->second.first;
+    // we don't know what mode (language) we are in, so we rely on the default
+    // language to be reasonable for from_expr
     out << " if " << from_expr(ns, "", itr->second.second);
   }
   out << "]";

src/analyses/invariant_set.cpp

@@ -131,6 +131,8 @@ std::string inv_object_storet::build_string(const exprt &expr) const
 
   // we also like "address_of" and "reference_to"
   // if the object is constant
+  // we don't know what mode (language) we are in, so we rely on the default
+  // language to be reasonable for from_expr
   if(is_constant_address(expr))
     return from_expr(ns, "", expr);
 
@@ -884,7 +886,6 @@ std::string inv_object_storet::to_string(
   unsigned a,
   const irep_idt &identifier) const
 {
-  // return from_expr(ns, "", get_expr(a));
   return id2string(map[a]);
 }
 

src/analyses/local_may_alias.cpp

@@ -457,7 +457,10 @@ void local_may_aliast::output(
           if(loc_info.aliases.find(j)==i)
           {
             assert(j<objects.size());
-            out << ' ' << from_expr(ns, "", objects[j]);
+            irep_idt identifier = "";
+            if(objects[j].id() == ID_symbol)
+              identifier = to_symbol_expr(objects[j]).get_identifier();
+            out << ' ' << from_expr(ns, identifier, objects[j]);
           }
 
         out << " }";

src/cbmc/bmc.cpp

@@ -239,17 +239,16 @@ void bmct::show_program()
   {
     std::cout << "// " << step.source.pc->location_number << " ";
     std::cout << step.source.pc->source_location.as_string() << "\n";
+    const irep_idt &function = step.source.pc->function;
 
     if(step.is_assignment())
     {
-      std::string string_value=
-        from_expr(ns, "", step.cond_expr);
+      std::string string_value = from_expr(ns, function, step.cond_expr);
       std::cout << "(" << count << ") " << string_value << "\n";
 
       if(!step.guard.is_true())
       {
-        std::string string_value=
-          from_expr(ns, "", step.guard);
+        std::string string_value = from_expr(ns, function, step.guard);
         std::cout << std::string(std::to_string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
@@ -258,15 +257,13 @@ void bmct::show_program()
     }
     else if(step.is_assert())
     {
-      std::string string_value=
-        from_expr(ns, "", step.cond_expr);
+      std::string string_value = from_expr(ns, function, step.cond_expr);
       std::cout << "(" << count << ") ASSERT("
                 << string_value <<") " << "\n";
 
       if(!step.guard.is_true())
       {
-        std::string string_value=
-          from_expr(ns, "", step.guard);
+        std::string string_value = from_expr(ns, function, step.guard);
         std::cout << std::string(std::to_string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
@@ -275,15 +272,13 @@ void bmct::show_program()
     }
     else if(step.is_assume())
     {
-      std::string string_value=
-        from_expr(ns, "", step.cond_expr);
+      std::string string_value = from_expr(ns, function, step.cond_expr);
       std::cout << "(" << count << ") ASSUME("
                 << string_value <<") " << "\n";
 
       if(!step.guard.is_true())
       {
-        std::string string_value=
-          from_expr(ns, "", step.guard);
+        std::string string_value = from_expr(ns, function, step.guard);
         std::cout << std::string(std::to_string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
@@ -292,25 +287,22 @@ void bmct::show_program()
     }
     else if(step.is_constraint())
     {
-      std::string string_value=
-        from_expr(ns, "", step.cond_expr);
+      std::string string_value = from_expr(ns, function, step.cond_expr);
       std::cout << "(" << count << ") CONSTRAINT("
                 << string_value <<") " << "\n";
 
       count++;
     }
     else if(step.is_shared_read() || step.is_shared_write())
     {
-      std::string string_value=
-        from_expr(ns, "", step.ssa_lhs);
+      std::string string_value = from_expr(ns, function, step.ssa_lhs);
       std::cout << "(" << count << ") SHARED_"
                 << (step.is_shared_write()?"WRITE":"READ")
                 << "(" << string_value <<")\n";
 
       if(!step.guard.is_true())
       {
-        std::string string_value=
-          from_expr(ns, "", step.guard);
+        std::string string_value = from_expr(ns, function, step.guard);
         std::cout << std::string(std::to_string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }