Well-formedness check for assume and assert instructions

Check that the guard evaluates to a Boolean value.

Author: Petr Bauch

src/goto-programs/goto_program.cpp

@@ -685,8 +685,16 @@ void goto_programt::instructiont::validate(
   case GOTO:
     break;
   case ASSUME:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      targets.empty(),
+      "assume instruction should not have a target",
+      source_location);
     break;
   case ASSERT:
+    DATA_CHECK_WITH_DIAGNOSTICS(
+      targets.empty(),
+      "assert instruction should not have a target",
+      source_location);
     break;
   case OTHER:
     break;

src/util/std_code.h

@@ -536,6 +536,11 @@ inline code_assumet &to_code_assume(codet &code)
   return static_cast<code_assumet &>(code);
 }
 
+inline void validate_expr(const code_assumet &x)
+{
+  validate_operands(x, 1, "assume must have one operand");
+}
+
 /// A non-fatal assertion, which checks a condition then permits execution to
 /// continue.
 class code_assertt:public codet
@@ -583,6 +588,11 @@ inline code_assertt &to_code_assert(codet &code)
   return static_cast<code_assertt &>(code);
 }
 
+inline void validate_expr(const code_assertt &x)
+{
+  validate_operands(x, 1, "assert must have one operand");
+}
+
 /// Create a fatal assertion, which checks a condition and then halts if it does
 /// not hold. Equivalent to `ASSERT(condition); ASSUME(condition)`.
 ///

src/util/std_expr.cpp

@@ -211,3 +211,47 @@ const exprt &object_descriptor_exprt::root_object() const
 
   return *p;
 }
+
+bool evaluates_to_boolean(const exprt &e)
+{
+  if(e.type().id() != ID_bool)
+    return false;
+  if(e.id() == ID_typecast)
+    return e.type().id() == ID_bool;
+
+  //Boolean constants
+  if(e.id() == ID_true || e.id() == ID_false)
+    return true;
+  if(e.id() == ID_constant)
+    return true;
+
+  //Symbols
+  if(e.id() == ID_symbol)
+    return true;
+
+  //arithmetic relations
+  if(e.id() == ID_equal || e.id() == ID_notequal)
+    return true;
+  if(e.id() == ID_ieee_float_equal || e.id() == ID_ieee_float_notequal)
+    return true;
+  if(e.id() == ID_ge || e.id() == ID_gt)
+    return true;
+  if(e.id() == ID_le || e.id() == ID_lt)
+    return true;
+
+  //propositional operators
+  if(
+    e.id() == ID_not || e.id() == ID_and || e.id() == ID_or ||
+    e.id() == ID_implies)
+    return true;
+  if(e.id() == ID_exists || e.id() == ID_forall)
+    return true;
+
+  //weird
+  if(
+    e.id() == ID_isfinite || e.id() == ID_isnormal || e.id() == ID_isinf ||
+    e.id() == ID_isnan)
+    return true;
+
+  return false;
+}

unit/Makefile

@@ -17,6 +17,7 @@ SRC += analyses/ai/ai.cpp \
        compound_block_locations.cpp \
        goto-programs/goto_trace_output.cpp \
        goto-programs/goto_program_declaration.cpp \
+       goto-programs/goto_program_assume.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \

unit/goto-programs/goto_program_assume.cpp

@@ -0,0 +1,64 @@
+/*******************************************************************\
+
+  Module: Unit tests for goto_program::validate
+
+  Author: Diffblue Ltd.
+
+ \*******************************************************************/
+
+#include <goto-programs/goto_function.h>
+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO(
+  "Validation of well-formed assert/assume codes",
+  "[core][goto-programs][validate]")
+{
+  GIVEN("A program with one assumption")
+  {
+    symbol_tablet symbol_table;
+    const typet type1 = signedbv_typet(32);
+    symbolt symbol;
+    irep_idt symbol_name = "a";
+    symbol.name = symbol_name;
+    symbol_exprt varx(symbol_name, type1);
+    exprt val10 = from_integer(10, type1);
+    binary_relation_exprt x_le_10(varx, ID_le, val10);
+
+    goto_functiont goto_function;
+    auto &instructions = goto_function.body.instructions;
+    instructions.emplace_back(goto_program_instruction_typet::ASSUME);
+
+    symbol.type = type1;
+    symbol_table.insert(symbol);
+    namespacet ns(symbol_table);
+    instructions.back().make_assertion(x_le_10);
+
+    WHEN("Instruction has no targets")
+    {
+      THEN("The consistency check succeeds")
+      {
+        goto_function.body.validate(ns, validation_modet::INVARIANT);
+        REQUIRE(true);
+      }
+    }
+
+    WHEN("Instruction has a target")
+    {
+      instructions.back().targets.push_back(instructions.begin());
+      THEN("The consistency check fails")
+      {
+        bool caught = false;
+        try
+        {
+          goto_function.body.validate(ns, validation_modet::EXCEPTION);
+        }
+        catch(incorrect_goto_program_exceptiont &e)
+        {
+          caught = true;
+        }
+        REQUIRE(caught);
+      }
+    }
+  }
+}