goto-model validation: Validate constant_exprt

We silently accept, and sometimes handle correctly, bitvector constants
that are encoded as -[absolute value] instead of two's complement. The
simplifier, however, will not handle this ambiguity as equalities over
constants are evaluated by comparing the value strings. Therefore, use
goto-model validation to ensure we do not process bitvector constants
that don't use two's complement encoding.

Fixes: #6759

Author: tautschnig

regression/cbmc/link_json_symtabs/two.json_symtab

@@ -1077,7 +1077,7 @@
                     }
                   },
                   "value": {
-                    "id": "00000000000000000000000000000000",
+                    "id": "0",
                     "sub": [
                     ],
                     "namedSub": {

src/util/std_expr.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "std_expr.h"
 
 #include "namespace.h"
+#include "pointer_expr.h"
 #include "range.h"
 
 #include <map>
@@ -19,6 +20,33 @@ bool constant_exprt::value_is_zero_string() const
   return val.find_first_not_of('0')==std::string::npos;
 }
 
+void constant_exprt::check(const exprt &expr, const validation_modet vm)
+{
+  DATA_CHECK(
+    vm, !expr.has_operands(), "constant expression must not have operands");
+
+  DATA_CHECK(
+    vm,
+    !can_cast_type<bitvector_typet>(expr.type()) ||
+      !id2string(to_constant_expr(expr).get_value()).empty(),
+    "bitvector constant must have a non-empty value");
+
+  DATA_CHECK(
+    vm,
+    !can_cast_type<bitvector_typet>(expr.type()) ||
+      can_cast_type<pointer_typet>(expr.type()) ||
+      id2string(to_constant_expr(expr).get_value())
+          .find_first_not_of("0123456789ABCDEF") == std::string::npos,
+    "negative bitvector constant must use two's complement");
+
+  DATA_CHECK(
+    vm,
+    !can_cast_type<bitvector_typet>(expr.type()) ||
+      to_constant_expr(expr).get_value() == ID_0 ||
+      id2string(to_constant_expr(expr).get_value())[0] != '0',
+    "bitvector constant must not have leading zeros");
+}
+
 exprt disjunction(const exprt::operandst &op)
 {
   if(op.empty())

src/util/std_expr.h

@@ -2848,6 +2848,18 @@ class constant_exprt : public nullary_exprt
   }
 
   bool value_is_zero_string() const;
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT);
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
 };
 
 template <>

src/util/validate_expressions.cpp

@@ -42,6 +42,10 @@ void call_on_expr(const exprt &expr, Args &&... args)
   {
     CALL_ON_EXPR(dereference_exprt);
   }
+  else if(expr.id() == ID_constant)
+  {
+    CALL_ON_EXPR(constant_exprt);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS