switch ssa_stept to handles

Daniel Kroening · Daniel Kroening · commit 17c6986e3ab7 · 2019-04-17T20:45:10.000+01:00
'Handles' more general than the literalt data structure, which is specific
to propositional, CNF-based SAT.
diff --git a/src/goto-checker/bmc_util.cpp b/src/goto-checker/bmc_util.cpp
@@ -58,7 +58,7 @@ ssa_step_matches_failing_property(const irep_idt &property_id)
            symex_target_equationt::SSA_stepst::const_iterator step,
            const prop_convt &prop_conv) {
     return step->is_assert() && step->get_property_id() == property_id &&
-           prop_conv.l_get(step->cond_literal).is_false();
+           prop_conv.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,
diff --git a/src/goto-checker/bmc_util.h b/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 &,
diff --git a/src/goto-checker/counterexample_beautification.cpp b/src/goto-checker/counterexample_beautification.cpp
@@ -41,7 +41,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 +78,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 +99,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 +117,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?
diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/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())
+      if(!step.guard_handle.is_constant())
       {
         auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);
-        localization_points.emplace(step.guard_literal, emplace_result.first);
+        literalt guard_literal = solver.convert(step.guard_handle);
+        localization_points.emplace(guard_literal, 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);
 
diff --git a/src/goto-checker/goto_symex_property_decider.cpp b/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);
 }
 
diff --git a/src/goto-checker/multi_path_symex_checker.cpp b/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;
 }
 
diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
@@ -225,7 +225,7 @@ void build_goto_trace(
 
     const SSA_stept &SSA_step = *it;
 
-    if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))
+    if(!prop_conv.get(SSA_step.guard_handle).is_true())
       continue;
 
     if(it->is_constraint() ||
@@ -388,7 +388,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();
+          prop_conv.get(SSA_step.cond_handle).is_true();
       }
 
       if(ssa_step_it == last_step_to_keep)
@@ -417,7 +417,7 @@ static bool is_failed_assertion_step(
   symex_target_equationt::SSA_stepst::const_iterator step,
   const prop_convt &prop_conv)
 {
-  return step->is_assert() && prop_conv.l_get(step->cond_literal).is_false();
+  return step->is_assert() && prop_conv.get(step->cond_handle).is_false();
 }
 
 void build_goto_trace(
diff --git a/src/goto-symex/ssa_step.h b/src/goto-symex/ssa_step.h
@@ -10,7 +10,6 @@ Author: Romain Brenguier <romain.brenguier@diffblue.com>
 #define CPROVER_GOTO_SYMEX_SSA_STEP_H
 
 #include <goto-programs/goto_trace.h>
-#include <solvers/prop/literal.h>
 
 #include "symex_target.h"
 
@@ -35,7 +34,7 @@ Author: Romain Brenguier <romain.brenguier@diffblue.com>
 /// which represent the condition guarding this step, i.e. what must hold for
 /// this step to be taken. Both `guard` and `cond_expr` will later be
 /// translated into verification condition for the SAT/SMT solver (or some
-/// other decision procedure), to be referred by their respective literals.
+/// other decision procedure), to be referred by their respective handles.
 /// Constraints usually arise from external conditions, such as memory models
 /// or partial orders: they represent assumptions with global effect.
 ///
@@ -136,7 +135,7 @@ class SSA_stept
   bool hidden = false;
 
   exprt guard;
-  literalt guard_literal;
+  exprt guard_handle;
 
   // for ASSIGNMENT and DECL
   ssa_exprt ssa_lhs;
@@ -146,7 +145,7 @@ class SSA_stept
 
   // for ASSUME/ASSERT/GOTO/CONSTRAINT
   exprt cond_expr;
-  literalt cond_literal;
+  exprt cond_handle;
   std::string comment;
 
   // for INPUT/OUTPUT
@@ -177,14 +176,14 @@ class SSA_stept
       type(_type),
       hidden(false),
       guard(static_cast<const exprt &>(get_nil_irep())),
-      guard_literal(const_literal(false)),
+      guard_handle(false_exprt()),
       ssa_lhs(static_cast<const ssa_exprt &>(get_nil_irep())),
       ssa_full_lhs(static_cast<const exprt &>(get_nil_irep())),
       original_full_lhs(static_cast<const exprt &>(get_nil_irep())),
       ssa_rhs(static_cast<const exprt &>(get_nil_irep())),
       assignment_type(symex_targett::assignment_typet::STATE),
       cond_expr(static_cast<const exprt &>(get_nil_irep())),
-      cond_literal(const_literal(false)),
+      cond_handle(false_exprt()),
       formatted(false),
       atomic_section_id(0),
       ignore(false)
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
@@ -18,7 +18,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/unwrap_nested_exception.h>
 
 #include <solvers/flattening/bv_conversion_exceptions.h>
-#include <solvers/prop/literal_expr.h>
 #include <solvers/prop/prop.h>
 #include <solvers/prop/prop_conv.h>
 
@@ -399,7 +398,7 @@ void symex_target_equationt::convert_guards(
   for(auto &step : SSA_steps)
   {
     if(step.ignore)
-      step.guard_literal=const_literal(false);
+      step.guard_handle = false_exprt();
     else
     {
       log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {
@@ -409,7 +408,7 @@ void symex_target_equationt::convert_guards(
 
       try
       {
-        step.guard_literal = prop_conv.convert(step.guard);
+        step.guard_handle = prop_conv.handle(step.guard);
       }
       catch(const bitvector_conversion_exceptiont &)
       {
@@ -429,7 +428,7 @@ void symex_target_equationt::convert_assumptions(
     if(step.is_assume())
     {
       if(step.ignore)
-        step.cond_literal=const_literal(true);
+        step.cond_handle = true_exprt();
       else
       {
         log.conditional_output(
@@ -440,7 +439,7 @@ void symex_target_equationt::convert_assumptions(
 
         try
         {
-          step.cond_literal = prop_conv.convert(step.cond_expr);
+          step.cond_handle = prop_conv.handle(step.cond_expr);
         }
         catch(const bitvector_conversion_exceptiont &)
         {
@@ -461,7 +460,7 @@ void symex_target_equationt::convert_goto_instructions(
     if(step.is_goto())
     {
       if(step.ignore)
-        step.cond_literal=const_literal(true);
+        step.cond_handle = true_exprt();
       else
       {
         log.conditional_output(
@@ -472,7 +471,7 @@ void symex_target_equationt::convert_goto_instructions(
 
         try
         {
-          step.cond_literal = prop_conv.convert(step.cond_expr);
+          step.cond_handle = prop_conv.handle(step.cond_expr);
         }
         catch(const bitvector_conversion_exceptiont &)
         {
@@ -534,7 +533,7 @@ void symex_target_equationt::convert_assertions(
       {
         step.converted = true;
         prop_conv.set_to_false(step.cond_expr);
-        step.cond_literal=const_literal(false);
+        step.cond_handle = false_exprt();
         return; // prevent further assumptions!
       }
       else if(step.is_assume())
@@ -573,7 +572,7 @@ void symex_target_equationt::convert_assertions(
       // do the conversion
       try
       {
-        step.cond_literal = prop_conv.convert(implication);
+        step.cond_handle = prop_conv.handle(implication);
       }
       catch(const bitvector_conversion_exceptiont &)
       {
@@ -583,17 +582,16 @@ void symex_target_equationt::convert_assertions(
       }
 
       // store disjunct
-      disjuncts.push_back(literal_exprt(!step.cond_literal));
+      disjuncts.push_back(not_exprt(step.cond_handle));
     }
     else if(step.is_assume())
     {
       // the assumptions have been converted before
       // avoid deep nesting of ID_and expressions
       if(assumption.id()==ID_and)
-        assumption.copy_to_operands(literal_exprt(step.cond_literal));
+        assumption.copy_to_operands(step.cond_handle);
       else
-        assumption=
-          and_exprt(assumption, literal_exprt(step.cond_literal));
+        assumption = and_exprt(assumption, step.cond_handle);
     }
   }
 

Original file line number	Diff line number	Diff line change
`@@ -58,10 +58,11 @@ const SSA_stept &goto_symex_fault_localizert::collect_guards(`
`58`	`58`	`step.assignment_type == symex_targett::assignment_typet::STATE &&`
`59`	`59`	`!step.ignore)`
`60`	`60`	`{`
`61`		`- if(!step.guard_literal.is_constant())`
	`61`	`+ if(!step.guard_handle.is_constant())`
`62`	`62`	`{`
`63`	`63`	`auto emplace_result = fault_location.scores.emplace(step.source.pc, 0);`
`64`		`- localization_points.emplace(step.guard_literal, emplace_result.first);`
	`64`	`+ literalt guard_literal = solver.convert(step.guard_handle);`
	`65`	`+ localization_points.emplace(guard_literal, emplace_result.first);`
`65`	`66`	`}`
`66`	`67`	`}`
`67`	`68`
`@@ -90,7 +91,7 @@ bool goto_symex_fault_localizert::check(`
`90`	`91`	`}`
`91`	`92`
`92`	`93`	`// lock the failed assertion`
`93`		`- assumptions.push_back(!failed_step.cond_literal);`
	`94`	`+ assumptions.push_back(!solver.convert(failed_step.cond_handle));`
`94`	`95`
`95`	`96`	`solver.set_assumptions(assumptions);`
`96`	`97`
Original file line number	Diff line number	Diff line change
`@@ -36,7 +36,7 @@ exprt goto_symex_property_decidert::goalt::as_expr() const`
`36`	`36`	`exprt::operandst conjuncts;`
`37`	`37`	`conjuncts.reserve(instances.size());`
`38`	`38`	`for(const auto &inst : instances)`
`39`		`- conjuncts.push_back(literal_exprt(inst->cond_literal));`
	`39`	`+ conjuncts.push_back(inst->cond_handle);`
`40`	`40`	`return conjunction(conjuncts);`
`41`	`41`	`}`
`42`	`42`
Original file line number	Diff line number	Diff line change
`@@ -72,9 +72,6 @@ multi_path_symex_checkert::prepare_property_decider(propertiest &properties)`
`72`	`72`	`std::chrono::duration<double> solver_runtime = ::prepare_property_decider(`
`73`	`73`	`properties, equation, property_decider, ui_message_handler);`
`74`	`74`
`75`		`- if(options.get_bool_option("localize-faults"))`
`76`		`- freeze_guards(equation, property_decider.get_solver());`
`77`		`-`
`78`	`75`	`return solver_runtime;`
`79`	`76`	`}`
`80`	`77`
Original file line number	Diff line number	Diff line change
`@@ -225,7 +225,7 @@ void build_goto_trace(`
`225`	`225`
`226`	`226`	`const SSA_stept &SSA_step = *it;`
`227`	`227`
`228`		`- if(prop_conv.l_get(SSA_step.guard_literal)!=tvt(true))`
	`228`	`+ if(!prop_conv.get(SSA_step.guard_handle).is_true())`
`229`	`229`	`continue;`
`230`	`230`
`231`	`231`	`if(it->is_constraint() \|\|`
`@@ -388,7 +388,7 @@ void build_goto_trace(`
`388`	`388`	`goto_trace_step.cond_expr = SSA_step.cond_expr;`
`389`	`389`
`390`	`390`	`goto_trace_step.cond_value =`
`391`		`- prop_conv.l_get(SSA_step.cond_literal).is_true();`
	`391`	`+ prop_conv.get(SSA_step.cond_handle).is_true();`
`392`	`392`	`}`
`393`	`393`
`394`	`394`	`if(ssa_step_it == last_step_to_keep)`
`@@ -417,7 +417,7 @@ static bool is_failed_assertion_step(`
`417`	`417`	`symex_target_equationt::SSA_stepst::const_iterator step,`
`418`	`418`	`const prop_convt &prop_conv)`
`419`	`419`	`{`
`420`		`- return step->is_assert() && prop_conv.l_get(step->cond_literal).is_false();`
	`420`	`+ return step->is_assert() && prop_conv.get(step->cond_handle).is_false();`
`421`	`421`	`}`
`422`	`422`
`423`	`423`	`void build_goto_trace(`
Original file line number	Diff line number	Diff line change
`@@ -18,7 +18,6 @@ Author: Daniel Kroening, [email protected]`
`18`	`18`	`#include <util/unwrap_nested_exception.h>`
`19`	`19`
`20`	`20`	`#include <solvers/flattening/bv_conversion_exceptions.h>`
`21`		`-#include <solvers/prop/literal_expr.h>`
`22`	`21`	`#include <solvers/prop/prop.h>`
`23`	`22`	`#include <solvers/prop/prop_conv.h>`
`24`	`23`
`@@ -399,7 +398,7 @@ void symex_target_equationt::convert_guards(`
`399`	`398`	`for(auto &step : SSA_steps)`
`400`	`399`	`{`
`401`	`400`	`if(step.ignore)`
`402`		`- step.guard_literal=const_literal(false);`
	`401`	`+ step.guard_handle = false_exprt();`
`403`	`402`	`else`
`404`	`403`	`{`
`405`	`404`	`log.conditional_output(log.debug(), [&step](messaget::mstreamt &mstream) {`
`@@ -409,7 +408,7 @@ void symex_target_equationt::convert_guards(`
`409`	`408`
`410`	`409`	`try`
`411`	`410`	`{`
`412`		`- step.guard_literal = prop_conv.convert(step.guard);`
	`411`	`+ step.guard_handle = prop_conv.handle(step.guard);`
`413`	`412`	`}`
`414`	`413`	`catch(const bitvector_conversion_exceptiont &)`
`415`	`414`	`{`
`@@ -429,7 +428,7 @@ void symex_target_equationt::convert_assumptions(`
`429`	`428`	`if(step.is_assume())`
`430`	`429`	`{`
`431`	`430`	`if(step.ignore)`
`432`		`- step.cond_literal=const_literal(true);`
	`431`	`+ step.cond_handle = true_exprt();`
`433`	`432`	`else`
`434`	`433`	`{`
`435`	`434`	`log.conditional_output(`
`@@ -440,7 +439,7 @@ void symex_target_equationt::convert_assumptions(`
`440`	`439`
`441`	`440`	`try`
`442`	`441`	`{`
`443`		`- step.cond_literal = prop_conv.convert(step.cond_expr);`
	`442`	`+ step.cond_handle = prop_conv.handle(step.cond_expr);`
`444`	`443`	`}`
`445`	`444`	`catch(const bitvector_conversion_exceptiont &)`
`446`	`445`	`{`
`@@ -461,7 +460,7 @@ void symex_target_equationt::convert_goto_instructions(`
`461`	`460`	`if(step.is_goto())`
`462`	`461`	`{`
`463`	`462`	`if(step.ignore)`
`464`		`- step.cond_literal=const_literal(true);`
	`463`	`+ step.cond_handle = true_exprt();`
`465`	`464`	`else`
`466`	`465`	`{`
`467`	`466`	`log.conditional_output(`
`@@ -472,7 +471,7 @@ void symex_target_equationt::convert_goto_instructions(`
`472`	`471`
`473`	`472`	`try`
`474`	`473`	`{`
`475`		`- step.cond_literal = prop_conv.convert(step.cond_expr);`
	`474`	`+ step.cond_handle = prop_conv.handle(step.cond_expr);`
`476`	`475`	`}`
`477`	`476`	`catch(const bitvector_conversion_exceptiont &)`
`478`	`477`	`{`
`@@ -534,7 +533,7 @@ void symex_target_equationt::convert_assertions(`
`534`	`533`	`{`
`535`	`534`	`step.converted = true;`
`536`	`535`	`prop_conv.set_to_false(step.cond_expr);`
`537`		`- step.cond_literal=const_literal(false);`
	`536`	`+ step.cond_handle = false_exprt();`
`538`	`537`	`return; // prevent further assumptions!`
`539`	`538`	`}`
`540`	`539`	`else if(step.is_assume())`
`@@ -573,7 +572,7 @@ void symex_target_equationt::convert_assertions(`
`573`	`572`	`// do the conversion`
`574`	`573`	`try`
`575`	`574`	`{`
`576`		`- step.cond_literal = prop_conv.convert(implication);`
	`575`	`+ step.cond_handle = prop_conv.handle(implication);`
`577`	`576`	`}`
`578`	`577`	`catch(const bitvector_conversion_exceptiont &)`
`579`	`578`	`{`
`@@ -583,17 +582,16 @@ void symex_target_equationt::convert_assertions(`
`583`	`582`	`}`
`584`	`583`
`585`	`584`	`// store disjunct`
`586`		`- disjuncts.push_back(literal_exprt(!step.cond_literal));`
	`585`	`+ disjuncts.push_back(not_exprt(step.cond_handle));`
`587`	`586`	`}`
`588`	`587`	`else if(step.is_assume())`
`589`	`588`	`{`
`590`	`589`	`// the assumptions have been converted before`
`591`	`590`	`// avoid deep nesting of ID_and expressions`
`592`	`591`	`if(assumption.id()==ID_and)`
`593`		`- assumption.copy_to_operands(literal_exprt(step.cond_literal));`
	`592`	`+ assumption.copy_to_operands(step.cond_handle);`
`594`	`593`	`else`
`595`		`- assumption=`
`596`		`- and_exprt(assumption, literal_exprt(step.cond_literal));`
	`594`	`+ assumption = and_exprt(assumption, step.cond_handle);`
`597`	`595`	`}`
`598`	`596`	`}`
`599`	`597`