Merge pull request #8449 from tautschnig/use-boolean_negate

Use boolean_negate for immediate simplification

Author: tautschnig

src/goto-instrument/contracts/dynamic-frames/dfcc_contract_clauses_codegen.cpp

@@ -110,8 +110,8 @@ void dfcc_contract_clauses_codegent::encode_assignable_target_group(
     new_vars = cleaner.clean(condition, dest, language_mode);
 
   // Jump target if condition is false
-  auto goto_instruction = dest.add(
-    goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
+  auto goto_instruction = dest.add(goto_programt::make_incomplete_goto(
+    boolean_negate(condition), source_location));
 
   for(const auto &target : group.targets())
     encode_assignable_target(language_mode, target, dest);
@@ -199,8 +199,8 @@ void dfcc_contract_clauses_codegent::encode_freeable_target_group(
     new_vars = cleaner.clean(condition, dest, language_mode);
 
   // Jump target if condition is false
-  auto goto_instruction = dest.add(
-    goto_programt::make_incomplete_goto(not_exprt{condition}, source_location));
+  auto goto_instruction = dest.add(goto_programt::make_incomplete_goto(
+    boolean_negate(condition), source_location));
 
   for(const auto &target : group.targets())
     encode_freeable_target(language_mode, target, dest);

src/goto-instrument/contracts/havoc_assigns_clause_targets.cpp

@@ -68,7 +68,7 @@ void havoc_assigns_clause_targetst::havoc_if_valid(
     skip_program.add(goto_programt::make_skip(source_location_no_checks));
 
   dest.add(goto_programt::make_goto(
-    skip_target, not_exprt{car.valid_var()}, source_location_no_checks));
+    skip_target, boolean_negate(car.valid_var()), source_location_no_checks));
 
   if(car.havoc_method == car_havoc_methodt::HAVOC_OBJECT)
   {
@@ -142,7 +142,7 @@ void havoc_assigns_clause_targetst::havoc_static_local(
     skip_program.add(goto_programt::make_skip(source_location_no_checks));
 
   dest.add(goto_programt::make_goto(
-    skip_target, not_exprt{car.valid_var()}, source_location_no_checks));
+    skip_target, boolean_negate(car.valid_var()), source_location_no_checks));
 
   const auto &target_type = car.target().type();
   side_effect_expr_nondett nondet(target_type, source_location);

src/goto-instrument/contracts/instrument_spec_assigns.cpp

@@ -656,9 +656,9 @@ exprt instrument_spec_assignst::target_validity_expr(
   // (or is NULL if we allow it explicitly).
   // This assertion will be falsified whenever `start_address` is invalid or
   // not of the right size (or is NULL if we do not allow it explicitly).
-  auto result =
-    or_exprt{not_exprt{car.condition()},
-             w_ok_exprt{car.target_start_address(), car.target_size()}};
+  auto result = or_exprt{
+    boolean_negate(car.condition()),
+    w_ok_exprt{car.target_start_address(), car.target_size()}};
 
   if(allow_null_target)
     result.add_to_operands(null_object(car.target_start_address()));

src/goto-instrument/contracts/utils.cpp

@@ -41,7 +41,9 @@ static void append_safe_havoc_code_for_expr(
   // skip havocing only if all pointer derefs in the expression are valid
   // (to avoid spurious pointer deref errors)
   dest.add(goto_programt::make_goto(
-    skip_target, not_exprt{all_dereferences_are_valid(expr, ns)}, location));
+    skip_target,
+    boolean_negate(all_dereferences_are_valid(expr, ns)),
+    location));
 
   havoc_code_impl();
 
@@ -433,8 +435,8 @@ static void replace_history_parameter_rec(
 
     // 2.2. Skip storing the history if the expression is invalid
     auto goto_instruction = history.add(goto_programt::make_incomplete_goto(
-      not_exprt{
-        all_dereferences_are_valid(parameter, namespacet(symbol_table))},
+      boolean_negate(
+        all_dereferences_are_valid(parameter, namespacet(symbol_table))),
       location));
 
     // 2.3. Add an assignment such that the value pointed to by the new

src/goto-symex/goto_state.cpp

@@ -145,11 +145,7 @@ void goto_statet::apply_condition(
     if(!is_ssa_expr(lhs) || !goto_symex_can_forward_propagatet(ns)(rhs))
       return;
 
-    if(rhs.is_true())
-      apply_condition(equal_exprt{lhs, false_exprt{}}, previous_state, ns);
-    else if(rhs.is_false())
-      apply_condition(equal_exprt{lhs, true_exprt{}}, previous_state, ns);
-    else
-      UNREACHABLE;
+    PRECONDITION(rhs.is_constant());
+    apply_condition(equal_exprt{lhs, boolean_negate(rhs)}, previous_state, ns);
   }
 }

src/goto-symex/symex_goto.cpp

@@ -279,7 +279,7 @@ void goto_symext::symex_goto(statet &state)
     {
       // generate assume(false) or a suitable negation if this
       // instruction is a conditional goto
-      exprt negated_guard = not_exprt{new_guard};
+      exprt negated_guard = boolean_negate(new_guard);
       do_simplify(negated_guard);
       log.statistics() << "replacing self-loop at "
                        << state.source.pc->source_location() << " by assume("
@@ -929,12 +929,7 @@ void goto_symext::loop_bound_exceeded(
 {
   const std::string loop_number = std::to_string(state.source.pc->loop_number);
 
-  exprt negated_cond;
-
-  if(guard.is_true())
-    negated_cond=false_exprt();
-  else
-    negated_cond=not_exprt(guard);
+  exprt negated_cond = boolean_negate(guard);
 
   if(symex_config.unwinding_assertions)
   {