Merge pull request #6786 from tautschnig/feature/more-checks

goto-model validation: Validate constant_exprt

Author: kroening

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, [email protected]
 #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

@@ -79,6 +79,14 @@ class ternary_exprt : public expr_protectedt
       expr.operands().size() == 3,
       "ternary expression must have three operands");
   }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+  }
 };
 
 /// \brief Cast an exprt to a \ref ternary_exprt
@@ -2294,6 +2302,21 @@ class if_exprt : public ternary_exprt
   {
     return op2();
   }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    ternary_exprt::check(expr, vm);
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    ternary_exprt::validate(expr, ns, vm);
+  }
 };
 
 template <>
@@ -2563,6 +2586,21 @@ class update_exprt : public ternary_exprt
   {
     return op2();
   }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    ternary_exprt::check(expr, vm);
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    ternary_exprt::validate(expr, ns, vm);
+  }
 };
 
 template <>
@@ -2848,6 +2886,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

@@ -13,6 +13,7 @@ Author: Daniel Poetzl
 #include <iostream>
 #endif
 
+#include "bitvector_expr.h"
 #include "pointer_expr.h"
 #include "ssa_expr.h"
 
@@ -42,6 +43,26 @@ 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 if(expr.id() == ID_if)
+  {
+    CALL_ON_EXPR(if_exprt);
+  }
+  else if(expr.id() == ID_update)
+  {
+    CALL_ON_EXPR(update_exprt);
+  }
+  else if(expr.id() == ID_overflow_unary_minus)
+  {
+    CALL_ON_EXPR(unary_minus_overflow_exprt);
+  }
+  else if(expr.id() == ID_count_leading_zeros)
+  {
+    CALL_ON_EXPR(count_leading_zeros_exprt);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS