Merge pull request #151 from tautschnig/symex-improvements

Symex improvements

Author: Daniel Kroening

src/path-symex/path_symex.cpp

@@ -422,6 +422,14 @@ void path_symext::assign_rec(
       var_state.value=propagate(ssa_rhs)?ssa_rhs:nil_exprt();
     }
   }
+  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());
+
+    assign_rec(state, guard, new_lhs, new_rhs);
+  }
   else if(ssa_lhs.id()==ID_member)
   {
     #ifdef DEBUG
@@ -541,14 +549,30 @@ void path_symext::assign_rec(
 
     assert(operands.size()==components.size());
 
-    for(std::size_t i=0; i<components.size(); i++)
+    if(ssa_rhs.id()==ID_struct &&
+       ssa_rhs.operands().size()==components.size())
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          member_exprt(ssa_rhs, components[i].get_name(), components[i].type()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      exprt::operandst::const_iterator lhs_it=operands.begin();
+      forall_operands(it, ssa_rhs)
+      {
+        assign_rec(state, guard, *lhs_it, *it);
+        ++lhs_it;
+      }
+    }
+    else
+    {
+      for(std::size_t i=0; i<components.size(); i++)
+      {
+        exprt new_rhs=
+          ssa_rhs.is_nil()?ssa_rhs:
+          simplify_expr(
+            member_exprt(
+              ssa_rhs,
+              components[i].get_name(),
+              components[i].type()),
+            state.var_map.ns);
+        assign_rec(state, guard, operands[i], new_rhs);
+      }
     }
   }
   else if(ssa_lhs.id()==ID_array)
@@ -564,36 +588,30 @@ void path_symext::assign_rec(
     const exprt::operandst &operands=ssa_lhs.operands();
 
     // split up into elements
-    for(std::size_t i=0; i<operands.size(); i++)
+    if(ssa_rhs.id()==ID_array &&
+       ssa_rhs.operands().size()==operands.size())
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          index_exprt(
-            ssa_rhs,
-            from_integer(i, index_type()), array_type.subtype()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      exprt::operandst::const_iterator lhs_it=operands.begin();
+      forall_operands(it, ssa_rhs)
+      {
+        assign_rec(state, guard, *lhs_it, *it);
+        ++lhs_it;
+      }
     }
-  }
-  else if(ssa_lhs.id()==ID_vector)
-  {
-    const vector_typet &vector_type=
-      to_vector_type(state.var_map.ns.follow(ssa_lhs.type()));
-
-    const exprt::operandst &operands=ssa_lhs.operands();
-
-    // split up into elements
-    for(std::size_t i=0; i<operands.size(); i++)
+    else
     {
-      exprt new_rhs=
-        ssa_rhs.is_nil()?ssa_rhs:
-        simplify_expr(
-          index_exprt(
-            ssa_rhs,
-            from_integer(i, index_type()), vector_type.subtype()),
-          state.var_map.ns);
-      assign_rec(state, guard, operands[i], new_rhs);
+      for(std::size_t i=0; i<operands.size(); i++)
+      {
+        exprt new_rhs=
+          ssa_rhs.is_nil()?ssa_rhs:
+          simplify_expr(
+            index_exprt(
+              ssa_rhs,
+              from_integer(i, index_type()),
+              array_type.subtype()),
+            state.var_map.ns);
+        assign_rec(state, guard, operands[i], new_rhs);
+      }
     }
   }
   else if(ssa_lhs.id()==ID_string_constant ||

src/path-symex/path_symex_state.cpp

@@ -41,12 +41,6 @@ path_symex_statet initial_state(
   return s;
 }
 
-loc_reft path_symex_statet::get_pc() const
-{
-  assert(current_thread<threads.size());
-  return threads[current_thread].pc;
-}
-
 void path_symex_statet::output(const threadt &thread, std::ostream &out) const
 {
   out << "  PC: " << thread.pc << '\n';

src/path-symex/path_symex_state.h

@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
 #define CPROVER_PATH_SYMEX_PATH_SYMEX_STATE_H
 
+#include <util/invariant.h>
+
 #include "locs.h"
 #include "var_map.h"
 #include "path_symex_history.h"
@@ -111,11 +113,9 @@ struct path_symex_statet
     current_thread=_thread;
   }
 
-  loc_reft get_pc() const;
-
   goto_programt::const_targett get_instruction() const
   {
-    return locs[get_pc()].target;
+    return locs[pc()].target;
   }
 
   bool is_executable() const
@@ -145,6 +145,7 @@ struct path_symex_statet
 
   loc_reft pc() const
   {
+    PRECONDITION(current_thread<threads.size());
     return threads[current_thread].pc;
   }
 

src/path-symex/path_symex_state_read.cpp

@@ -247,7 +247,14 @@ exprt path_symex_statet::instantiate_rec(
     {
       irep_idt id="symex::nondet"+std::to_string(var_map.nondet_count);
       var_map.nondet_count++;
-      return symbol_exprt(id, src.type());
+
+      auxiliary_symbolt nondet_symbol;
+      nondet_symbol.name=id;
+      nondet_symbol.base_name=id;
+      nondet_symbol.type=src.type();
+      var_map.new_symbols.add(nondet_symbol);
+
+      return nondet_symbol.symbol_expr();
     }
     else
       throw "instantiate_rec: unexpected side effect "+id2string(statement);

src/path-symex/var_map.h

@@ -18,12 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/namespace.h>
 #include <util/type.h>
 #include <util/std_expr.h>
+#include <util/symbol_table.h>
 
 class var_mapt
 {
 public:
   explicit var_mapt(const namespacet &_ns):
-    ns(_ns), shared_count(0), local_count(0), nondet_count(0), dynamic_count(0)
+    ns(_ns.get_symbol_table(), new_symbols),
+    shared_count(0),
+    local_count(0),
+    nondet_count(0),
+    dynamic_count(0)
   {
   }
 
@@ -93,7 +98,8 @@ class var_mapt
 
   void init(var_infot &var_info);
 
-  const namespacet &ns;
+  const namespacet ns;
+  symbol_tablet new_symbols;
 
   void output(std::ostream &) const;
 

src/symex/path_search.cpp

@@ -68,9 +68,9 @@ path_searcht::resultt path_searcht::operator()(
       statet &state=tmp_queue.front();
 
       // record we have seen it
-      loc_data[state.get_pc().loc_number].visited=true;
+      loc_data[state.pc().loc_number].visited=true;
 
-      debug() << "Loc: #" << state.get_pc().loc_number
+      debug() << "Loc: #" << state.pc().loc_number
               << ", queue: " << queue.size()
               << ", depth: " << state.get_depth();
       for(const auto &s : queue)
@@ -102,10 +102,13 @@ path_searcht::resultt path_searcht::operator()(
 
       if(number_of_steps%1000==0)
       {
+        time_periodt running_time=current_time()-start_time;
         status() << "Queue " << queue.size()
-                 << " thread " << state.get_current_thread()
+                 << " thread " << state.get_current_thread()+1
                  << '/' << state.threads.size()
-                 << " PC " << state.pc() << messaget::eom;
+                 << " PC " << state.pc()
+                 << " [" << number_of_steps << " steps, "
+                 << running_time << "s]" << messaget::eom;
       }
 
       // an error, possibly?
@@ -264,34 +267,90 @@ bool path_searcht::drop_state(const statet &state)
 {
   goto_programt::const_targett pc=state.get_instruction();
 
+  const source_locationt &source_location=pc->source_location;
+
+  if(!source_location.is_nil() &&
+     last_source_location!=source_location)
+  {
+    debug() << "SYMEX at file " << source_location.get_file()
+            << " line " << source_location.get_line()
+            << " function " << source_location.get_function()
+            << eom;
+
+    last_source_location=source_location;
+  }
+
   // depth limit
-  if(depth_limit_set && state.get_depth()>depth_limit)
+  if(depth_limit>=0 && state.get_depth()>depth_limit)
     return true;
 
   // context bound
-  if(context_bound_set && state.get_no_thread_interleavings()>context_bound)
+  if(context_bound>=0 && state.get_no_thread_interleavings()>context_bound)
     return true;
 
   // branch bound
-  if(branch_bound_set && state.get_no_branches()>branch_bound)
+  if(branch_bound>=0 && state.get_no_branches()>branch_bound)
     return true;
 
   // unwinding limit -- loops
-  if(unwind_limit_set && state.get_instruction()->is_backwards_goto())
+  if(unwind_limit>=0 && pc->is_backwards_goto())
   {
+    bool stop=false;
+
     for(const auto &loop_info : state.unwinding_map)
       if(loop_info.second>unwind_limit)
-        return true;
+      {
+        stop=true;
+        break;
+      }
+
+    const irep_idt id=goto_programt::loop_id(pc);
+    path_symex_statet::unwinding_mapt::const_iterator entry=
+      state.unwinding_map.find(state.pc());
+    debug() << (stop?"Not unwinding":"Unwinding")
+      << " loop " << id << " iteration "
+      << (entry==state.unwinding_map.end()?-1:entry->second)
+      << " (" << unwind_limit << " max)"
+      << " " << source_location
+      << " thread " << state.get_current_thread() << eom;
+
+    if(stop)
+      return true;
   }
 
   // unwinding limit -- recursion
-  if(unwind_limit_set && state.get_instruction()->is_function_call())
+  if(unwind_limit>=0 && pc->is_function_call())
   {
+    bool stop=false;
+
     for(const auto &rec_info : state.recursion_map)
       if(rec_info.second>unwind_limit)
-        return true;
+      {
+        stop=true;
+        break;
+      }
+
+    exprt function=to_code_function_call(pc->code).function();
+    const irep_idt id=function.get(ID_identifier); // could be nil
+    path_symex_statet::recursion_mapt::const_iterator entry=
+      state.recursion_map.find(id);
+    if(entry!=state.recursion_map.end())
+      debug() << (stop?"Not unwinding":"Unwinding")
+        << " recursion " << id << " iteration "
+        << entry->second
+        << " (" << unwind_limit << " max)"
+        << " " << source_location
+        << " thread " << state.get_current_thread() << eom;
+
+    if(stop)
+      return true;
   }
 
+  // search time limit (--max-search-time)
+  if(time_limit>=0 &&
+     current_time().get_t()>start_time.get_t()+time_limit*1000)
+    return true;
+
   if(pc->is_assume() &&
      simplify_expr(pc->guard, ns).is_false())
   {