Initial attempt at introducing well-formedness checking for SSA

Follows the #3123 skeleton with additional checks in SSA_stept.

Author: Petr Bauch

src/cbmc/bmc.cpp

@@ -638,6 +638,10 @@ void bmct::perform_symbolic_execution(
   goto_symext::get_goto_functiont get_goto_function)
 {
   symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+  if(options.get_bool_option("validate-ssa-equation"))
+  {
+    symex.validate(ns, validation_modet::INVARIANT);
+  }
   INVARIANT(
     options.get_bool_option("paths") || path_storage.empty(),
     "Branch points were saved even though we should have been "

src/cbmc/cbmc_parse_options.cpp

@@ -536,6 +536,11 @@ int cbmc_parse_optionst::doit()
     goto_model.validate(ns, validation_modet::INVARIANT);
   }
 
+  if(cmdline.isset("validate-ssa-equation"))
+  {
+    options.set_option("validate-ssa-equation", true);
+  }
+
   return bmct::do_language_agnostic_bmc(
     path_strategy_chooser, options, goto_model, ui_message_handler);
 }
@@ -986,6 +991,9 @@ void cbmc_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     " --validate-goto-model        enable additional well-formedness checks on the\n"
     "                              goto program\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --validate-ssa-equation      enable additional well-formedness checks on the\n"
+    "                              SSA equation\n"
     HELP_GOTO_TRACE
     HELP_FLUSH
     " --verbosity #                verbosity level\n"

src/cbmc/cbmc_parse_options.h

@@ -74,6 +74,7 @@ class optionst;
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
   "(validate-goto-model)" \
+  "(validate-ssa-equation)" \
   "(claim):(show-claims)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 

src/goto-symex/goto_symex.h

@@ -512,6 +512,11 @@ class goto_symext
       "attempting to read remaining_vccs");
     return _remaining_vccs;
   }
+
+  void validate(const namespacet &ns, const validation_modet vm) const
+  {
+    target.validate(ns, vm);
+  }
 };
 
 #endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_H

src/goto-symex/symex_target_equation.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_target_equation.h"
 
+#include <util/base_type.h>
 #include <util/format_expr.h>
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
@@ -976,3 +977,56 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
 
   out << "Guard: " << format(guard) << '\n';
 }
+
+/// Check that the SSA step is well-formed
+/// \param ns namespace to lookup identifiers
+/// \param vm validation mode to be used for reporting failures
+void symex_target_equationt::SSA_stept::validate(
+  const namespacet &ns,
+  const validation_modet vm) const
+{
+  validate_expr_full_pick(guard, ns, vm);
+
+  switch(type)
+  {
+  case goto_trace_stept::typet::ASSERT:
+  case goto_trace_stept::typet::ASSUME:
+  case goto_trace_stept::typet::GOTO:
+  case goto_trace_stept::typet::CONSTRAINT:
+    validate_expr_full_pick(cond_expr, ns, vm);
+    break;
+  case goto_trace_stept::typet::ASSIGNMENT:
+  case goto_trace_stept::typet::DECL:
+    validate_expr_full_pick(ssa_lhs, ns, vm);
+    validate_expr_full_pick(ssa_full_lhs, ns, vm);
+    validate_expr_full_pick(original_full_lhs, ns, vm);
+    validate_expr_full_pick(ssa_rhs, ns, vm);
+    base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns);
+    break;
+  case goto_trace_stept::typet::INPUT:
+  case goto_trace_stept::typet::OUTPUT:
+    for(const auto &expr : io_args)
+      validate_expr_full_pick(expr, ns, vm);
+    break;
+  case goto_trace_stept::typet::FUNCTION_CALL:
+    for(const auto &expr : ssa_function_arguments)
+      validate_expr_full_pick(expr, ns, vm);
+  case goto_trace_stept::typet::FUNCTION_RETURN:
+  {
+    const symbolt *symbol;
+    DATA_CHECK(
+      !ns.lookup(function_identifier, symbol), "unknown function identifier");
+  }
+  break;
+  case goto_trace_stept::typet::NONE:
+  case goto_trace_stept::typet::LOCATION:
+  case goto_trace_stept::typet::DEAD:
+  case goto_trace_stept::typet::SHARED_READ:
+  case goto_trace_stept::typet::SHARED_WRITE:
+  case goto_trace_stept::typet::SPAWN:
+  case goto_trace_stept::typet::MEMORY_BARRIER:
+  case goto_trace_stept::typet::ATOMIC_BEGIN:
+  case goto_trace_stept::typet::ATOMIC_END:
+    break;
+  }
+}

src/goto-symex/symex_target_equation.h

@@ -15,8 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <list>
 #include <iosfwd>
 
-#include <util/invariant.h>
 #include <util/merge_irep.h>
+#include <util/validate.h>
 
 #include <goto-programs/goto_program.h>
 #include <goto-programs/goto_trace.h>
@@ -268,6 +268,8 @@ class symex_target_equationt:public symex_targett
       std::ostream &out) const;
 
     void output(std::ostream &out) const;
+
+    void validate(const namespacet &ns, const validation_modet vm) const;
   };
 
   std::size_t count_assertions() const
@@ -324,6 +326,12 @@ class symex_target_equationt:public symex_targett
     return false;
   }
 
+  void validate(const namespacet &ns, const validation_modet vm) const
+  {
+    for(const SSA_stept &step : SSA_steps)
+      step.validate(ns, vm);
+  }
+
 protected:
   // for enforcing sharing in the expressions stored
   merge_irept merge_irep;

src/util/ssa_expr.h

@@ -139,6 +139,21 @@ class ssa_exprt:public symbol_exprt
   /* Used to determine whether or not an identifier can be built
    * before trying and getting an exception */
   static bool can_build_identifier(const exprt &src);
+
+  void check(const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    DATA_CHECK(!has_operands(), "SSA expression should not have operands");
+    DATA_CHECK(id() == ID_symbol, "SSA expression symbols are symbols");
+    DATA_CHECK(get_bool(ID_C_SSA_symbol), "wrong SSA expression ID");
+  }
+
+  void validate(
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT) const
+  {
+    check(vm);
+    validate_expr_full_pick(get_original_expr(), ns, vm);
+  }
 };
 
 /*! \brief Cast a generic exprt to an \ref ssa_exprt

src/util/validate_expressions.cpp

@@ -14,7 +14,7 @@ Author: Daniel Poetzl
 
 #include "expr.h"
 #include "namespace.h"
-#include "std_expr.h"
+#include "ssa_expr.h"
 #include "validate.h"
 
 #define CALL_ON_EXPR(expr_type)                                                \
@@ -31,6 +31,10 @@ void call_on_expr(const exprt &expr, Args &&... args)
   {
     CALL_ON_EXPR(plus_exprt);
   }
+  else if(expr.get_bool(ID_C_SSA_symbol))
+  {
+    CALL_ON_EXPR(ssa_exprt);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS