Add nondet_padding expression

This data structure will be used to allow encoding/lowering passes
to insert padding bitvectors with non deteriministic values. Unlike the
SAT decision procedures, generating an SMT formula for nondet padding
will require a corresponding parameter-less function to be defined.
This placeholder expression is intended to be inserted in lowering
passes and then substituted at the point of term generation. Note that
it doesn't quite make sense to use symbols for this as the decision
procedure doesn't have mutable symbol table access and adding an extra
decision procedure symbol table would have other complications.

Author: thomasspriggs

src/solvers/smt2_incremental/encoding/nondet_padding.h

@@ -0,0 +1,41 @@
+// Author: Diffblue Ltd.
+
+/// \file
+/// Expressions for use in incremental SMT2 decision procedure
+
+#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H
+#define CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H
+
+#include <util/bitvector_types.h>
+#include <util/expr.h>
+#include <util/invariant.h>
+
+class nondet_padding_exprt;
+void validate_expr(const nondet_padding_exprt &padding);
+
+const irep_idt ID_nondet_padding = "nondet_padding";
+
+class nondet_padding_exprt : public expr_protectedt
+{
+public:
+  explicit nondet_padding_exprt(typet type)
+    : expr_protectedt{ID_nondet_padding, std::move(type)}
+  {
+    validate_expr(*this);
+  }
+};
+
+template <>
+inline bool can_cast_expr<nondet_padding_exprt>(const exprt &base)
+{
+  return base.id() == ID_nondet_padding;
+}
+
+inline void validate_expr(const nondet_padding_exprt &padding)
+{
+  INVARIANT(
+    can_cast_type<bv_typet>(padding.type()),
+    "Nondet padding is expected to pad a bit vector type.");
+}
+
+#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_ENCODING_NONDET_PADDING_H

unit/Makefile

@@ -117,6 +117,7 @@ SRC += analyses/ai/ai.cpp \
        solvers/smt2_incremental/smt_to_smt2_string.cpp \
        solvers/smt2_incremental/encoding/struct_encoding.cpp \
        solvers/smt2_incremental/encoding/enum_encoding.cpp \
+       solvers/smt2_incremental/encoding/nondet_padding.cpp \
        solvers/smt2_incremental/theories/smt_array_theory.cpp \
        solvers/smt2_incremental/theories/smt_bit_vector_theory.cpp \
        solvers/smt2_incremental/theories/smt_core_theory.cpp \

unit/solvers/smt2_incremental/encoding/nondet_padding.cpp

@@ -0,0 +1,43 @@
+// Author: Diffblue Ltd.
+
+#include <util/expr_cast.h>
+#include <util/std_expr.h>
+
+#include <solvers/smt2_incremental/encoding/nondet_padding.h>
+#include <testing-utils/invariant.h>
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("Nondet padding expression", "[core][smt2_incremental]")
+{
+  const bv_typet type{8};
+  const exprt padding = nondet_padding_exprt{type};
+  SECTION("Valid usage")
+  {
+    REQUIRE(padding.type() == type);
+    REQUIRE(nullptr != expr_try_dynamic_cast<nondet_padding_exprt>(padding));
+  }
+  const auto type_error = invariant_failure_containing(
+    "Nondet padding is expected to pad a bit vector type.");
+  SECTION("Failed downcasts")
+  {
+    const exprt not_padding = symbol_exprt{"foo", empty_typet{}};
+    REQUIRE(
+      nullptr == expr_try_dynamic_cast<nondet_padding_exprt>(not_padding));
+    const exprt wrong_type = [&]() {
+      exprt padding = nondet_padding_exprt{type};
+      padding.type() = empty_typet{};
+      return padding;
+    }();
+    cbmc_invariants_should_throwt invariants_throw;
+    CHECK_THROWS_MATCHES(
+      expr_checked_cast<nondet_padding_exprt>(wrong_type),
+      invariant_failedt,
+      type_error);
+  }
+  SECTION("Construction with incorrect type")
+  {
+    cbmc_invariants_should_throwt invariants_throw;
+    CHECK_THROWS_MATCHES(
+      nondet_padding_exprt{empty_typet{}}, invariant_failedt, type_error);
+  }
+}