Merge pull request diffblue#1373 from diffblue/symex-trace-fix

Symex trace fix

regression/Makefile

@@ -12,6 +12,7 @@ DIRS = ansi-c \
        invariants \
        strings \
        strings-smoke-tests \
+       symex \
        test-script \
        # Empty last line
 

regression/symex/show-trace1/main.c

@@ -4,12 +4,12 @@ int main()
 {
   int i, j, k;
 
-  i=input();
-  j=input();
-  k=input();
+  i=input(); // expect 2
+  j=input(); // expect 3
+  k=input(); // expect 6
 
   if(i==2)
     if(j==i+1)
       if(k==i*j)
-        assert(0);
+        __CPROVER_assert(0, "");
 }

regression/symex/show-trace1/test.desc

@@ -1,6 +1,6 @@
 CORE
 main.c
---show-trace
+--trace
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

src/path-symex/path_symex.cpp

@@ -129,7 +129,7 @@ void path_symext::assign(
 
   // start recursion on lhs
   exprt::operandst _guard; // start with empty guard
-  assign_rec(state, _guard, ssa_lhs, ssa_rhs);
+  assign_rec(state, _guard, lhs, ssa_lhs, ssa_rhs);
 }
 
 inline static typet c_sizeof_type_rec(const exprt &expr)
@@ -347,6 +347,7 @@ void path_symext::symex_va_arg_next(
 void path_symext::assign_rec(
   path_symex_statet &state,
   exprt::operandst &guard,
+  const exprt &full_lhs,
   const exprt &ssa_lhs,
   const exprt &ssa_rhs)
 {
@@ -376,17 +377,17 @@ void path_symext::assign_rec(
 
     // increase the SSA counter and produce new SSA symbol expression
     var_info.increment_ssa_counter();
-    symbol_exprt new_lhs=var_info.ssa_symbol();
+    symbol_exprt new_ssa_lhs=var_info.ssa_symbol();
 
     #ifdef DEBUG
-    std::cout << "new_lhs: " << new_lhs.get_identifier() << '\n';
+    std::cout << "new_ssa_lhs: " << new_ssa_lhs.get_identifier() << '\n';
     #endif
 
     // record new state of lhs
     {
       // reference is not stable
       path_symex_statet::var_statet &var_state=state.get_var_state(var_info);
-      var_state.ssa_symbol=new_lhs;
+      var_state.ssa_symbol=new_ssa_lhs;
     }
 
     // rhs nil means non-det assignment
@@ -398,11 +399,11 @@ void path_symext::assign_rec(
     else
     {
       // consistency check
-      if(!base_type_eq(ssa_rhs.type(), new_lhs.type(), state.var_map.ns))
+      if(!base_type_eq(ssa_rhs.type(), new_ssa_lhs.type(), state.var_map.ns))
       {
         #ifdef DEBUG
         std::cout << "ssa_rhs: " << ssa_rhs.pretty() << '\n';
-        std::cout << "new_lhs: " << new_lhs.pretty() << '\n';
+        std::cout << "new_ssa_lhs: " << new_ssa_lhs.pretty() << '\n';
         #endif
         throw "assign_rec got different types";
       }
@@ -413,8 +414,8 @@ void path_symext::assign_rec(
 
       if(!guard.empty())
         step.guard=conjunction(guard);
-      step.full_lhs=ssa_lhs;
-      step.ssa_lhs=new_lhs;
+      step.full_lhs=full_lhs;
+      step.ssa_lhs=new_ssa_lhs;
       step.ssa_rhs=ssa_rhs;
 
       // propagate the rhs?
@@ -425,10 +426,10 @@ void path_symext::assign_rec(
   else if(ssa_lhs.id()==ID_typecast)
   {
     // dereferencing might yield a typecast
-    const exprt &new_lhs=to_typecast_expr(ssa_lhs).op();
-    typecast_exprt new_rhs(ssa_rhs, new_lhs.type());
+    const exprt &new_ssa_lhs=to_typecast_expr(ssa_lhs).op();
+    typecast_exprt new_rhs(ssa_rhs, new_ssa_lhs.type());
 
-    assign_rec(state, guard, new_lhs, new_rhs);
+    assign_rec(state, guard, full_lhs, new_ssa_lhs, new_rhs);
   }
   else if(ssa_lhs.id()==ID_member)
   {
@@ -454,17 +455,17 @@ void path_symext::assign_rec(
 
       with_exprt new_rhs(struct_op, member_name, ssa_rhs);
 
-      assign_rec(state, guard, struct_op, new_rhs);
+      assign_rec(state, guard, full_lhs, struct_op, new_rhs);
     }
     else if(compound_type.id()==ID_union)
     {
       // rewrite into byte_extract, and do again
       exprt offset=from_integer(0, index_type());
 
       byte_extract_exprt
-        new_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());
+        new_ssa_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());
 
-      assign_rec(state, guard, new_lhs, ssa_rhs);
+      assign_rec(state, guard, full_lhs, new_ssa_lhs, ssa_rhs);
     }
     else
       throw "assign_rec: member expects struct or union type";
@@ -496,12 +497,12 @@ void path_symext::assign_rec(
 
     // true
     guard.push_back(cond);
-    assign_rec(state, guard, lhs_if_expr.true_case(), ssa_rhs);
+    assign_rec(state, guard, full_lhs, lhs_if_expr.true_case(), ssa_rhs);
     guard.pop_back();
 
     // false
     guard.push_back(not_exprt(cond));
-    assign_rec(state, guard, lhs_if_expr.false_case(), ssa_rhs);
+    assign_rec(state, guard, full_lhs, lhs_if_expr.false_case(), ssa_rhs);
     guard.pop_back();
   }
   else if(ssa_lhs.id()==ID_byte_extract_little_endian ||
@@ -533,9 +534,9 @@ void path_symext::assign_rec(
     new_rhs.offset()=byte_extract_expr.offset();
     new_rhs.value()=ssa_rhs;
 
-    const exprt new_lhs=byte_extract_expr.op();
+    const exprt new_ssa_lhs=byte_extract_expr.op();
 
-    assign_rec(state, guard, new_lhs, new_rhs);
+    assign_rec(state, guard, full_lhs, new_ssa_lhs, new_rhs);
   }
   else if(ssa_lhs.id()==ID_struct)
   {
@@ -555,7 +556,7 @@ void path_symext::assign_rec(
       exprt::operandst::const_iterator lhs_it=operands.begin();
       forall_operands(it, ssa_rhs)
       {
-        assign_rec(state, guard, *lhs_it, *it);
+        assign_rec(state, guard, full_lhs, *lhs_it, *it);
         ++lhs_it;
       }
     }
@@ -571,7 +572,7 @@ void path_symext::assign_rec(
               components[i].get_name(),
               components[i].type()),
             state.var_map.ns);
-        assign_rec(state, guard, operands[i], new_rhs);
+        assign_rec(state, guard, full_lhs, operands[i], new_rhs);
       }
     }
   }
@@ -594,7 +595,7 @@ void path_symext::assign_rec(
       exprt::operandst::const_iterator lhs_it=operands.begin();
       forall_operands(it, ssa_rhs)
       {
-        assign_rec(state, guard, *lhs_it, *it);
+        assign_rec(state, guard, full_lhs, *lhs_it, *it);
         ++lhs_it;
       }
     }
@@ -610,7 +611,7 @@ void path_symext::assign_rec(
               from_integer(i, index_type()),
               array_type.subtype()),
             state.var_map.ns);
-        assign_rec(state, guard, operands[i], new_rhs);
+        assign_rec(state, guard, full_lhs, operands[i], new_rhs);
       }
     }
   }
@@ -1090,6 +1091,10 @@ void path_symext::operator()(
       {
         // just needs to be recorded
       }
+      else if(statement==ID_output)
+      {
+        // just needs to be recorded
+      }
       else
         throw "unexpected OTHER statement: "+id2string(statement);
     }

src/path-symex/path_symex_class.h

@@ -93,6 +93,7 @@ class path_symext
   void assign_rec(
     path_symex_statet &state,
     exprt::operandst &guard, // instantiated
+    const exprt &full_lhs, // not instantiated, no recursion
     const exprt &ssa_lhs, // instantiated, recursion here
     const exprt &ssa_rhs); // instantiated
 

src/symex/symex_parse_options.cpp

@@ -26,23 +26,24 @@ Author: Daniel Kroening, [email protected]
 #include <cpp/cpp_language.h>
 #include <java_bytecode/java_bytecode_language.h>
 
-#include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/goto_convert_functions.h>
-#include <goto-programs/show_properties.h>
-#include <goto-programs/set_properties.h>
-#include <goto-programs/read_goto_binary.h>
-#include <goto-programs/loop_ids.h>
-#include <goto-programs/link_to_library.h>
 #include <goto-programs/goto_inline.h>
-#include <goto-programs/xml_goto_trace.h>
+#include <goto-programs/initialize_goto_model.h>
+#include <goto-programs/link_to_library.h>
+#include <goto-programs/loop_ids.h>
+#include <goto-programs/read_goto_binary.h>
 #include <goto-programs/remove_complex.h>
+#include <goto-programs/remove_exceptions.h>
 #include <goto-programs/remove_function_pointers.h>
+#include <goto-programs/remove_instanceof.h>
+#include <goto-programs/remove_returns.h>
 #include <goto-programs/remove_skip.h>
+#include <goto-programs/remove_unused_functions.h>
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
-#include <goto-programs/remove_exceptions.h>
-#include <goto-programs/remove_instanceof.h>
-#include <goto-programs/remove_unused_functions.h>
+#include <goto-programs/set_properties.h>
+#include <goto-programs/show_properties.h>
+#include <goto-programs/xml_goto_trace.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -304,6 +305,7 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     goto_check(options, goto_model);
 
     // remove stuff
+    remove_returns(goto_model);
     remove_complex(goto_model);
     remove_vector(goto_model);
     // remove function pointers