Merge pull request #4533 from diffblue/goto_symex_decision_procedure

goto_symex now uses decision_proceduret API

Author: tautschnig

src/goto-checker/bmc_util.cpp

@@ -56,9 +56,9 @@ ssa_step_matches_failing_property(const irep_idt &property_id)
 {
   return [property_id](
            symex_target_equationt::SSA_stepst::const_iterator step,
-           const prop_convt &prop_conv) {
+           const decision_proceduret &decision_procedure) {
     return step->is_assert() && step->get_property_id() == property_id &&
-           prop_conv.l_get(step->cond_literal).is_false();
+           decision_procedure.get(step->cond_handle).is_false();
   };
 }
 
@@ -103,19 +103,6 @@ void output_error_trace(
   }
 }
 
-void freeze_guards(
-  const symex_target_equationt &equation,
-  prop_convt &prop_conv)
-{
-  for(const auto &step : equation.SSA_steps)
-  {
-    if(!step.guard_literal.is_constant())
-      prop_conv.set_frozen(step.guard_literal);
-    if(step.is_assert() && !step.cond_literal.is_constant())
-      prop_conv.set_frozen(step.cond_literal);
-  }
-}
-
 /// outputs an error witness in graphml format
 void output_graphml(
   const goto_tracet &goto_trace,

src/goto-checker/bmc_util.h

@@ -60,8 +60,6 @@ void output_error_trace(
   const trace_optionst &,
   ui_message_handlert &);
 
-void freeze_guards(const symex_target_equationt &, prop_convt &);
-
 void output_graphml(const goto_tracet &, const namespacet &, const optionst &);
 void output_graphml(
   const symex_target_equationt &,

src/goto-checker/counterexample_beautification.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/symbol.h>
 #include <util/threeval.h>
 
-#include <solvers/prop/literal_expr.h>
 #include <solvers/prop/prop_minimize.h>
 
 counterexample_beautificationt::counterexample_beautificationt(
@@ -41,7 +40,7 @@ void counterexample_beautificationt::get_minimization_list(
       it->is_assignment() &&
       it->assignment_type == symex_targett::assignment_typet::STATE)
     {
-      if(!prop_conv.l_get(it->guard_literal).is_false())
+      if(!prop_conv.get(it->guard_handle).is_false())
       {
         const typet &type = it->ssa_lhs.type();
 
@@ -78,10 +77,14 @@ counterexample_beautificationt::get_failed_property(
         equation.SSA_steps.begin();
       it != equation.SSA_steps.end();
       it++)
+  {
     if(
-      it->is_assert() && prop_conv.l_get(it->guard_literal).is_true() &&
-      prop_conv.l_get(it->cond_literal).is_false())
+      it->is_assert() && prop_conv.get(it->guard_handle).is_true() &&
+      prop_conv.get(it->cond_handle).is_false())
+    {
       return it;
+    }
+  }
 
   UNREACHABLE;
   return equation.SSA_steps.end();
@@ -95,7 +98,7 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
   failed = get_failed_property(boolbv, equation);
 
   // lock the failed assertion
-  boolbv.set_to(literal_exprt(failed->cond_literal), false);
+  boolbv.set_to(failed->cond_handle, false);
 
   {
     log.status() << "Beautifying counterexample (guards)" << messaget::eom;
@@ -113,8 +116,9 @@ operator()(boolbvt &boolbv, const symex_target_equationt &equation)
         it->is_assignment() &&
         it->assignment_type != symex_targett::assignment_typet::HIDDEN)
       {
-        if(!it->guard_literal.is_constant())
-          guard_count[it->guard_literal]++;
+        literalt l = boolbv.convert(it->guard_handle);
+        if(!l.is_constant())
+          guard_count[l]++;
       }
 
       // reached failed assertion?

src/goto-checker/goto_symex_fault_localizer.cpp

@@ -58,10 +58,11 @@ const SSA_stept &goto_symex_fault_localizert::collect_guards(
       step.assignment_type == symex_targett::assignment_typet::STATE &&
       !step.ignore)
     {
-      if(!step.guard_literal.is_constant())
+      literalt l = solver.convert(step.guard_handle);
+      if(!l.is_constant())
       {
         auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
-        localization_points.emplace(step.guard_literal, emplace_result.first);
+        localization_points.emplace(l, emplace_result.first);
       }
     }
 
@@ -90,7 +91,7 @@ bool goto_symex_fault_localizert::check(
   }
 
   // lock the failed assertion
-  assumptions.push_back(!failed_step.cond_literal);
+  assumptions.push_back(!solver.convert(failed_step.cond_handle));
 
   solver.set_assumptions(assumptions);
 

src/goto-checker/goto_symex_fault_localizer.h

@@ -18,6 +18,8 @@ Author: Peter Schrammel
 
 #include <goto-symex/symex_target_equation.h>
 
+#include <solvers/prop/prop_conv.h>
+
 #include "fault_localization_provider.h"
 
 class goto_symex_fault_localizert

src/goto-checker/goto_symex_property_decider.cpp

@@ -36,7 +36,7 @@ exprt goto_symex_property_decidert::goalt::as_expr() const
   exprt::operandst conjuncts;
   conjuncts.reserve(instances.size());
   for(const auto &inst : instances)
-    conjuncts.push_back(literal_exprt(inst->cond_literal));
+    conjuncts.push_back(inst->cond_handle);
   return conjunction(conjuncts);
 }
 

src/goto-checker/multi_path_symex_checker.cpp

@@ -72,9 +72,6 @@ multi_path_symex_checkert::prepare_property_decider(propertiest &properties)
   std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
     properties, equation, property_decider, ui_message_handler);
 
-  if(options.get_bool_option("localize-faults"))
-    freeze_guards(equation, property_decider.get_solver());
-
   return solver_runtime;
 }
 

src/goto-symex/build_goto_trace.cpp

@@ -20,13 +20,12 @@ Author: Daniel Kroening
 
 #include <goto-programs/goto_functions.h>
 
-#include <solvers/prop/prop_conv.h>
-#include <solvers/prop/prop.h>
+#include <solvers/decision_procedure.h>
 
 #include "partial_order_concurrency.h"
 
 static exprt build_full_lhs_rec(
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   const exprt &src_original, // original identifiers
   const exprt &src_ssa)      // renamed identifiers
@@ -39,17 +38,18 @@ static exprt build_full_lhs_rec(
   if(id==ID_index)
   {
     // get index value from src_ssa
-    exprt index_value=prop_conv.get(to_index_expr(src_ssa).index());
+    exprt index_value = decision_procedure.get(to_index_expr(src_ssa).index());
 
     if(index_value.is_not_nil())
     {
       simplify(index_value, ns);
       index_exprt tmp=to_index_expr(src_original);
       tmp.index()=index_value;
-      tmp.array()=
-        build_full_lhs_rec(prop_conv, ns,
-          to_index_expr(src_original).array(),
-          to_index_expr(src_ssa).array());
+      tmp.array() = build_full_lhs_rec(
+        decision_procedure,
+        ns,
+        to_index_expr(src_original).array(),
+        to_index_expr(src_ssa).array());
       return std::move(tmp);
     }
 
@@ -58,22 +58,29 @@ static exprt build_full_lhs_rec(
   else if(id==ID_member)
   {
     member_exprt tmp=to_member_expr(src_original);
-    tmp.struct_op()=build_full_lhs_rec(
-      prop_conv, ns,
+    tmp.struct_op() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
       to_member_expr(src_original).struct_op(),
       to_member_expr(src_ssa).struct_op());
   }
   else if(id==ID_if)
   {
     if_exprt tmp2=to_if_expr(src_original);
 
-    tmp2.false_case()=build_full_lhs_rec(prop_conv, ns,
-      tmp2.false_case(), to_if_expr(src_ssa).false_case());
+    tmp2.false_case() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      tmp2.false_case(),
+      to_if_expr(src_ssa).false_case());
 
-    tmp2.true_case()=build_full_lhs_rec(prop_conv, ns,
-      tmp2.true_case(), to_if_expr(src_ssa).true_case());
+    tmp2.true_case() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      tmp2.true_case(),
+      to_if_expr(src_ssa).true_case());
 
-    exprt tmp=prop_conv.get(to_if_expr(src_ssa).cond());
+    exprt tmp = decision_procedure.get(to_if_expr(src_ssa).cond());
 
     if(tmp.is_true())
       return tmp2.true_case();
@@ -85,16 +92,19 @@ static exprt build_full_lhs_rec(
   else if(id==ID_typecast)
   {
     typecast_exprt tmp=to_typecast_expr(src_original);
-    tmp.op()=build_full_lhs_rec(prop_conv, ns,
-      to_typecast_expr(src_original).op(), to_typecast_expr(src_ssa).op());
+    tmp.op() = build_full_lhs_rec(
+      decision_procedure,
+      ns,
+      to_typecast_expr(src_original).op(),
+      to_typecast_expr(src_ssa).op());
     return std::move(tmp);
   }
   else if(id==ID_byte_extract_little_endian ||
           id==ID_byte_extract_big_endian)
   {
     byte_extract_exprt tmp = to_byte_extract_expr(src_original);
     tmp.op() = build_full_lhs_rec(
-      prop_conv, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
+      decision_procedure, ns, tmp.op(), to_byte_extract_expr(src_ssa).op());
 
     // re-write into big case-split
   }
@@ -169,7 +179,8 @@ static void update_internal_field(
 
 /// Replace nondet values that appear in \p type by their values as found by
 /// \p solver.
-static void replace_nondet_in_type(typet &type, const prop_convt &solver)
+static void
+replace_nondet_in_type(typet &type, const decision_proceduret &solver)
 {
   if(type.id() == ID_array)
   {
@@ -182,7 +193,8 @@ static void replace_nondet_in_type(typet &type, const prop_convt &solver)
 
 /// Replace nondet values that appear in the type of \p expr and its
 /// subexpressions type by their values as found by \p solver.
-static void replace_nondet_in_type(exprt &expr, const prop_convt &solver)
+static void
+replace_nondet_in_type(exprt &expr, const decision_proceduret &solver)
 {
   replace_nondet_in_type(expr.type(), solver);
   for(auto &sub : expr.operands())
@@ -192,7 +204,7 @@ static void replace_nondet_in_type(exprt &expr, const prop_convt &solver)
 void build_goto_trace(
   const symex_target_equationt &target,
   ssa_step_predicatet is_last_step_to_keep,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
@@ -218,14 +230,14 @@ void build_goto_trace(
   {
     if(
       last_step_to_keep == target.SSA_steps.end() &&
-      is_last_step_to_keep(it, prop_conv))
+      is_last_step_to_keep(it, decision_procedure))
     {
       last_step_to_keep = it;
     }
 
     const SSA_stept &SSA_step = *it;
 
-    if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
+    if(!decision_procedure.get(SSA_step.guard_handle).is_true())
       continue;
 
     if(it->is_constraint() ||
@@ -250,7 +262,7 @@ void build_goto_trace(
         // these are just used to get the time stamp -- the clock type is
         // computed to be of the minimal necessary size, but we don't need to
         // know it to get the value so just use typeless
-        exprt clock_value = prop_conv.get(
+        exprt clock_value = decision_procedure.get(
           symbol_exprt::typeless(partial_order_concurrencyt::rw_clock_id(it)));
 
         const auto cv = numeric_cast<mp_integer>(clock_value);
@@ -342,7 +354,7 @@ void build_goto_trace(
       goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
 
       for(auto &arg : goto_trace_step.function_arguments)
-        arg = prop_conv.get(arg);
+        arg = decision_procedure.get(arg);
 
       // update internal field for specific variables in the counterexample
       update_internal_field(SSA_step, goto_trace_step, ns);
@@ -359,15 +371,20 @@ void build_goto_trace(
       if(SSA_step.original_full_lhs.is_not_nil())
       {
         goto_trace_step.full_lhs = build_full_lhs_rec(
-          prop_conv, ns, SSA_step.original_full_lhs, SSA_step.ssa_full_lhs);
-        replace_nondet_in_type(goto_trace_step.full_lhs, prop_conv);
+          decision_procedure,
+          ns,
+          SSA_step.original_full_lhs,
+          SSA_step.ssa_full_lhs);
+        replace_nondet_in_type(goto_trace_step.full_lhs, decision_procedure);
       }
 
       if(SSA_step.ssa_full_lhs.is_not_nil())
       {
-        goto_trace_step.full_lhs_value = prop_conv.get(SSA_step.ssa_full_lhs);
+        goto_trace_step.full_lhs_value =
+          decision_procedure.get(SSA_step.ssa_full_lhs);
         simplify(goto_trace_step.full_lhs_value, ns);
-        replace_nondet_in_type(goto_trace_step.full_lhs_value, prop_conv);
+        replace_nondet_in_type(
+          goto_trace_step.full_lhs_value, decision_procedure);
       }
 
       for(const auto &j : SSA_step.converted_io_args)
@@ -378,7 +395,7 @@ void build_goto_trace(
         }
         else
         {
-          exprt tmp = prop_conv.get(j);
+          exprt tmp = decision_procedure.get(j);
           goto_trace_step.io_args.push_back(tmp);
         }
       }
@@ -388,7 +405,7 @@ void build_goto_trace(
         goto_trace_step.cond_expr = SSA_step.cond_expr;
 
         goto_trace_step.cond_value =
-          prop_conv.l_get(SSA_step.cond_literal).is_true();
+          decision_procedure.get(SSA_step.cond_handle).is_true();
       }
 
       if(ssa_step_it == last_step_to_keep)
@@ -400,31 +417,33 @@ void build_goto_trace(
 void build_goto_trace(
   const symex_target_equationt &target,
   symex_target_equationt::SSA_stepst::const_iterator last_step_to_keep,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
-  const auto is_last_step_to_keep = [last_step_to_keep](
-    symex_target_equationt::SSA_stepst::const_iterator it, const prop_convt &) {
-    return last_step_to_keep == it;
-  };
+  const auto is_last_step_to_keep =
+    [last_step_to_keep](
+      symex_target_equationt::SSA_stepst::const_iterator it,
+      const decision_proceduret &) { return last_step_to_keep == it; };
 
   return build_goto_trace(
-    target, is_last_step_to_keep, prop_conv, ns, goto_trace);
+    target, is_last_step_to_keep, decision_procedure, ns, goto_trace);
 }
 
 static bool is_failed_assertion_step(
   symex_target_equationt::SSA_stepst::const_iterator step,
-  const prop_convt &prop_conv)
+  const decision_proceduret &decision_procedure)
 {
-  return step->is_assert() && prop_conv.l_get(step->cond_literal).is_false();
+  return step->is_assert() &&
+         decision_procedure.get(step->cond_handle).is_false();
 }
 
 void build_goto_trace(
   const symex_target_equationt &target,
-  const prop_convt &prop_conv,
+  const decision_proceduret &decision_procedure,
   const namespacet &ns,
   goto_tracet &goto_trace)
 {
-  build_goto_trace(target, is_failed_assertion_step, prop_conv, ns, goto_trace);
+  build_goto_trace(
+    target, is_failed_assertion_step, decision_procedure, ns, goto_trace);
 }