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

Daniel Kroening · web-flow · commit 8cd4490db23b · 2017-09-12T15:44:11.000+01:00
Symex trace fix
diff --git a/regression/Makefile b/regression/Makefile
@@ -12,6 +12,7 @@ DIRS = ansi-c \
        invariants \
        strings \
        strings-smoke-tests \
+       symex \
        test-script \
        # Empty last line
 
diff --git a/regression/symex/show-trace1/main.c b/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, "");
 }
diff --git a/regression/symex/show-trace1/test.desc b/regression/symex/show-trace1/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---show-trace
+--trace
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/src/path-symex/path_symex.cpp b/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);
     }
diff --git a/src/path-symex/path_symex_class.h b/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
 
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
@@ -26,23 +26,24 @@ Author: Daniel Kroening, kroening@kroening.com
 #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

Original file line number	Diff line number	Diff line change
`@@ -129,7 +129,7 @@ void path_symext::assign(`
`129`	`129`
`130`	`130`	`// start recursion on lhs`
`131`	`131`	`exprt::operandst _guard; // start with empty guard`
`132`		`- assign_rec(state, _guard, ssa_lhs, ssa_rhs);`
	`132`	`+ assign_rec(state, _guard, lhs, ssa_lhs, ssa_rhs);`
`133`	`133`	`}`
`134`	`134`
`135`	`135`	`inline static typet c_sizeof_type_rec(const exprt &expr)`
`@@ -347,6 +347,7 @@ void path_symext::symex_va_arg_next(`
`347`	`347`	`void path_symext::assign_rec(`
`348`	`348`	`path_symex_statet &state,`
`349`	`349`	`exprt::operandst &guard,`
	`350`	`+ const exprt &full_lhs,`
`350`	`351`	`const exprt &ssa_lhs,`
`351`	`352`	`const exprt &ssa_rhs)`
`352`	`353`	`{`
`@@ -376,17 +377,17 @@ void path_symext::assign_rec(`
`376`	`377`
`377`	`378`	`// increase the SSA counter and produce new SSA symbol expression`
`378`	`379`	`var_info.increment_ssa_counter();`
`379`		`- symbol_exprt new_lhs=var_info.ssa_symbol();`
	`380`	`+ symbol_exprt new_ssa_lhs=var_info.ssa_symbol();`
`380`	`381`
`381`	`382`	`#ifdef DEBUG`
`382`		`- std::cout << "new_lhs: " << new_lhs.get_identifier() << '\n';`
	`383`	`+ std::cout << "new_ssa_lhs: " << new_ssa_lhs.get_identifier() << '\n';`
`383`	`384`	`#endif`
`384`	`385`
`385`	`386`	`// record new state of lhs`
`386`	`387`	`{`
`387`	`388`	`// reference is not stable`
`388`	`389`	`path_symex_statet::var_statet &var_state=state.get_var_state(var_info);`
`389`		`- var_state.ssa_symbol=new_lhs;`
	`390`	`+ var_state.ssa_symbol=new_ssa_lhs;`
`390`	`391`	`}`
`391`	`392`
`392`	`393`	`// rhs nil means non-det assignment`
`@@ -398,11 +399,11 @@ void path_symext::assign_rec(`
`398`	`399`	`else`
`399`	`400`	`{`
`400`	`401`	`// consistency check`
`401`		`- if(!base_type_eq(ssa_rhs.type(), new_lhs.type(), state.var_map.ns))`
	`402`	`+ if(!base_type_eq(ssa_rhs.type(), new_ssa_lhs.type(), state.var_map.ns))`
`402`	`403`	`{`
`403`	`404`	`#ifdef DEBUG`
`404`	`405`	`std::cout << "ssa_rhs: " << ssa_rhs.pretty() << '\n';`
`405`		`- std::cout << "new_lhs: " << new_lhs.pretty() << '\n';`
	`406`	`+ std::cout << "new_ssa_lhs: " << new_ssa_lhs.pretty() << '\n';`
`406`	`407`	`#endif`
`407`	`408`	`throw "assign_rec got different types";`
`408`	`409`	`}`
`@@ -413,8 +414,8 @@ void path_symext::assign_rec(`
`413`	`414`
`414`	`415`	`if(!guard.empty())`
`415`	`416`	`step.guard=conjunction(guard);`
`416`		`- step.full_lhs=ssa_lhs;`
`417`		`- step.ssa_lhs=new_lhs;`
	`417`	`+ step.full_lhs=full_lhs;`
	`418`	`+ step.ssa_lhs=new_ssa_lhs;`
`418`	`419`	`step.ssa_rhs=ssa_rhs;`
`419`	`420`
`420`	`421`	`// propagate the rhs?`
`@@ -425,10 +426,10 @@ void path_symext::assign_rec(`
`425`	`426`	`else if(ssa_lhs.id()==ID_typecast)`
`426`	`427`	`{`
`427`	`428`	`// dereferencing might yield a typecast`
`428`		`- const exprt &new_lhs=to_typecast_expr(ssa_lhs).op();`
`429`		`- typecast_exprt new_rhs(ssa_rhs, new_lhs.type());`
	`429`	`+ const exprt &new_ssa_lhs=to_typecast_expr(ssa_lhs).op();`
	`430`	`+ typecast_exprt new_rhs(ssa_rhs, new_ssa_lhs.type());`
`430`	`431`
`431`		`- assign_rec(state, guard, new_lhs, new_rhs);`
	`432`	`+ assign_rec(state, guard, full_lhs, new_ssa_lhs, new_rhs);`
`432`	`433`	`}`
`433`	`434`	`else if(ssa_lhs.id()==ID_member)`
`434`	`435`	`{`
`@@ -454,17 +455,17 @@ void path_symext::assign_rec(`
`454`	`455`
`455`	`456`	`with_exprt new_rhs(struct_op, member_name, ssa_rhs);`
`456`	`457`
`457`		`- assign_rec(state, guard, struct_op, new_rhs);`
	`458`	`+ assign_rec(state, guard, full_lhs, struct_op, new_rhs);`
`458`	`459`	`}`
`459`	`460`	`else if(compound_type.id()==ID_union)`
`460`	`461`	`{`
`461`	`462`	`// rewrite into byte_extract, and do again`
`462`	`463`	`exprt offset=from_integer(0, index_type());`
`463`	`464`
`464`	`465`	`byte_extract_exprt`
`465`		`- new_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());`
	`466`	`+ new_ssa_lhs(byte_update_id(), struct_op, offset, ssa_rhs.type());`
`466`	`467`
`467`		`- assign_rec(state, guard, new_lhs, ssa_rhs);`
	`468`	`+ assign_rec(state, guard, full_lhs, new_ssa_lhs, ssa_rhs);`
`468`	`469`	`}`
`469`	`470`	`else`
`470`	`471`	`throw "assign_rec: member expects struct or union type";`
`@@ -496,12 +497,12 @@ void path_symext::assign_rec(`
`496`	`497`
`497`	`498`	`// true`
`498`	`499`	`guard.push_back(cond);`
`499`		`- assign_rec(state, guard, lhs_if_expr.true_case(), ssa_rhs);`
	`500`	`+ assign_rec(state, guard, full_lhs, lhs_if_expr.true_case(), ssa_rhs);`
`500`	`501`	`guard.pop_back();`
`501`	`502`
`502`	`503`	`// false`
`503`	`504`	`guard.push_back(not_exprt(cond));`
`504`		`- assign_rec(state, guard, lhs_if_expr.false_case(), ssa_rhs);`
	`505`	`+ assign_rec(state, guard, full_lhs, lhs_if_expr.false_case(), ssa_rhs);`
`505`	`506`	`guard.pop_back();`
`506`	`507`	`}`
`507`	`508`	`else if(ssa_lhs.id()==ID_byte_extract_little_endian \|\|`
`@@ -533,9 +534,9 @@ void path_symext::assign_rec(`
`533`	`534`	`new_rhs.offset()=byte_extract_expr.offset();`
`534`	`535`	`new_rhs.value()=ssa_rhs;`
`535`	`536`
`536`		`- const exprt new_lhs=byte_extract_expr.op();`
	`537`	`+ const exprt new_ssa_lhs=byte_extract_expr.op();`
`537`	`538`
`538`		`- assign_rec(state, guard, new_lhs, new_rhs);`
	`539`	`+ assign_rec(state, guard, full_lhs, new_ssa_lhs, new_rhs);`
`539`	`540`	`}`
`540`	`541`	`else if(ssa_lhs.id()==ID_struct)`
`541`	`542`	`{`
`@@ -555,7 +556,7 @@ void path_symext::assign_rec(`
`555`	`556`	`exprt::operandst::const_iterator lhs_it=operands.begin();`
`556`	`557`	`forall_operands(it, ssa_rhs)`
`557`	`558`	`{`
`558`		`- assign_rec(state, guard, lhs_it, it);`
	`559`	`+ assign_rec(state, guard, full_lhs, lhs_it, it);`
`559`	`560`	`++lhs_it;`
`560`	`561`	`}`
`561`	`562`	`}`
`@@ -571,7 +572,7 @@ void path_symext::assign_rec(`
`571`	`572`	`components[i].get_name(),`
`572`	`573`	`components[i].type()),`
`573`	`574`	`state.var_map.ns);`
`574`		`- assign_rec(state, guard, operands[i], new_rhs);`
	`575`	`+ assign_rec(state, guard, full_lhs, operands[i], new_rhs);`
`575`	`576`	`}`
`576`	`577`	`}`
`577`	`578`	`}`
`@@ -594,7 +595,7 @@ void path_symext::assign_rec(`
`594`	`595`	`exprt::operandst::const_iterator lhs_it=operands.begin();`
`595`	`596`	`forall_operands(it, ssa_rhs)`
`596`	`597`	`{`
`597`		`- assign_rec(state, guard, lhs_it, it);`
	`598`	`+ assign_rec(state, guard, full_lhs, lhs_it, it);`
`598`	`599`	`++lhs_it;`
`599`	`600`	`}`
`600`	`601`	`}`
`@@ -610,7 +611,7 @@ void path_symext::assign_rec(`
`610`	`611`	`from_integer(i, index_type()),`
`611`	`612`	`array_type.subtype()),`
`612`	`613`	`state.var_map.ns);`
`613`		`- assign_rec(state, guard, operands[i], new_rhs);`
	`614`	`+ assign_rec(state, guard, full_lhs, operands[i], new_rhs);`
`614`	`615`	`}`
`615`	`616`	`}`
`616`	`617`	`}`
`@@ -1090,6 +1091,10 @@ void path_symext::operator()(`
`1090`	`1091`	`{`
`1091`	`1092`	`// just needs to be recorded`
`1092`	`1093`	`}`
	`1094`	`+ else if(statement==ID_output)`
	`1095`	`+ {`
	`1096`	`+ // just needs to be recorded`
	`1097`	`+ }`
`1093`	`1098`	`else`
`1094`	`1099`	`throw "unexpected OTHER statement: "+id2string(statement);`
`1095`	`1100`	`}`