introduce __CPROVER_map type

This introduces C syntax for a type __CPROVER_map(domain, codomain) where domain is a list of types and codomain is a type. The type is internal, for modeling purposes within our own library only, and hence not added to user-facing documentation. It replaces arrays with size __CPROVER_infinity, which are now deprecated.
diffblue · Jan 9, 2025 · 76d5fe0 · 76d5fe0
1 parent 36b2335
commit 76d5fe0
Show file tree

Hide file tree

Showing 18 changed files with 152 additions and 7 deletions.
diff --git a/regression/cbmc/map-type/basic1.c b/regression/cbmc/map-type/basic1.c
@@ -0,0 +1,19 @@
+int main()
+{
+  __CPROVER_map(int, int) my_map;
+
+  my_map = __CPROVER_lambda
+  {
+    int i;
+    i == 1 ? 10 : 20
+  };
+
+  // should pass
+  __CPROVER_assert(my_map(1) == 10, "(1)");
+  __CPROVER_assert(my_map(2) == 20, "(2)");
+
+  // should fail
+  __CPROVER_assert(my_map(0) == 10, "(0)");
+
+  return 0;
+}
diff --git a/regression/cbmc/map-type/basic1.desc b/regression/cbmc/map-type/basic1.desc
@@ -0,0 +1,11 @@
+CORE
+basic1.c
+
+^\[.*\] line \d+ \(1\): FAILURE$
+^\[.*\] line \d+ \(2\): FAILURE$
+^\[.*\] line \d+ \(0\): FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc/map-type/basic2.c b/regression/cbmc/map-type/basic2.c
@@ -0,0 +1,18 @@
+__CPROVER_map(int, int) nondet_map();
+
+int main()
+{
+  __CPROVER_map(int, int) my_map = nondet_map();
+
+  __CPROVER_assume(my_map(1) == 10);
+  __CPROVER_assume(my_map(2) == 20);
+
+  // should pass
+  __CPROVER_assert(my_map(1) == 10, "(1)");
+  __CPROVER_assert(my_map(2) == 20, "(2)");
+
+  // should fail
+  __CPROVER_assert(my_map(0) == 10, "(0)");
+
+  return 0;
+}
diff --git a/regression/cbmc/map-type/basic2.desc b/regression/cbmc/map-type/basic2.desc
@@ -0,0 +1,11 @@
+CORE
+basic2.c
+
+^\[.*\] line \d+ \(1\): SUCCESS$
+^\[.*\] line \d+ \(2\): SUCCESS$
+^\[.*\] line \d+ \(0\): FAILURE$
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 
 class ansi_c_declarationt;
 class c_bit_field_typet;
+class mathematical_function_typet;
 class shift_exprt;
 
 class c_typecheck_baset:
@@ -261,6 +262,7 @@ class c_typecheck_baset:
   virtual void typecheck_code_type(code_typet &type);
   virtual void typecheck_typedef_type(typet &type);
   virtual void typecheck_c_bit_field_type(c_bit_field_typet &type);
+  virtual void typecheck_map_type(mathematical_function_typet &);
   virtual void typecheck_typeof_type(typet &type);
   virtual void typecheck_array_type(array_typet &type);
   virtual void typecheck_vector_type(typet &type);

diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
@@ -2534,6 +2534,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
     function_application_exprt function_application(f_op, expr.arguments());
 
     function_application.add_source_location() = expr.source_location();
+    function_application.type() = mathematical_function_type.codomain();
 
     expr.swap(function_application);
     return;

diff --git a/src/ansi-c/c_typecheck_type.cpp b/src/ansi-c/c_typecheck_type.cpp
@@ -111,6 +111,10 @@ void c_typecheck_baset::typecheck_type(typet &type)
   {
     typecheck_vector_type(type);
   }
+  else if(type.id() == ID_mathematical_function)
+  {
+    typecheck_map_type(to_mathematical_function_type(type));
+  }
   else if(type.id()==ID_custom_unsignedbv ||
           type.id()==ID_custom_signedbv ||
           type.id()==ID_custom_floatbv ||
@@ -726,6 +730,14 @@ void c_typecheck_baset::typecheck_vector_type(typet &type)
   type = new_type.with_source_location(source_location);
 }
 
+void c_typecheck_baset::typecheck_map_type(mathematical_function_typet &type)
+{
+  for(auto &t : type.domain())
+    typecheck_type(t);
+
+  typecheck_type(type.codomain());
+}
+
 void c_typecheck_baset::typecheck_compound_type(struct_union_typet &type)
 {
   // These get replaced by symbol types later.

diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
@@ -612,6 +612,28 @@ std::string expr2ct::convert_rec(
 
     return q+dest+d;
   }
+  else if(src.id() == ID_mathematical_function)
+  {
+    const mathematical_function_typet &function_type =
+      to_mathematical_function_type(src);
+    std::string dest = CPROVER_PREFIX "map(";
+    bool first = true;
+    for(auto &t : function_type.domain())
+    {
+      if(first)
+        first = false;
+      else
+        dest += ", ";
+
+      dest += convert(t);
+    }
+
+    dest += ", ";
+    dest += convert(function_type.codomain());
+    dest += ")";
+
+    return q + dest + d;
+  }
   else if(src.id()==ID_constructor ||
           src.id()==ID_destructor)
   {

diff --git a/src/ansi-c/parser.y b/src/ansi-c/parser.y
@@ -198,6 +198,7 @@ int yyansi_cerror(const std::string &error);
 %token TOK_CLRCALL     "__clrcall"
 %token TOK_FORALL      "forall"
 %token TOK_EXISTS      "exists"
+%token TOK_LAMBDA      "lambda"
 %token TOK_ACSL_FORALL "\\forall"
 %token TOK_ACSL_EXISTS "\\exists"
 %token TOK_ACSL_LAMBDA "\\lambda"
@@ -206,6 +207,7 @@ int yyansi_cerror(const std::string &error);
 %token TOK_CPROVER_BITVECTOR "__CPROVER_bitvector"
 %token TOK_CPROVER_FLOATBV "__CPROVER_floatbv"
 %token TOK_CPROVER_FIXEDBV "__CPROVER_fixedbv"
+%token TOK_CPROVER_MAP "__CPROVER_map"
 %token TOK_CPROVER_ATOMIC "__CPROVER_atomic"
 %token TOK_CPROVER_BOOL "__CPROVER_bool"
 %token TOK_CPROVER_THROW "__CPROVER_throw"
@@ -506,6 +508,14 @@ quantifier_expression:
           mto($$, $5);
           PARSER.pop_scope();
         }
+        | TOK_LAMBDA compound_scope '{' declaration comma_expression '}'
+        {
+          $$=$1;
+          set($$, ID_lambda);
+          parser_stack($$).add_to_operands(tuple_exprt( { std::move(parser_stack($4)) } ));
+          mto($$, $5);
+          PARSER.pop_scope();
+        }
         ;
 
 cprover_contract_loop_invariant:
@@ -1111,6 +1121,7 @@ type_specifier:
         | typedef_type_specifier
         | typeof_type_specifier
         | atomic_type_specifier
+        | map_type_specifier
         ;
 
 declaration_qualifier_list:
@@ -1554,6 +1565,18 @@ array_of_construct:
         { $$=$1; stack_type($$).add_subtype().swap(parser_stack($2)); }
         ;
 
+map_type_specifier:
+          TOK_CPROVER_MAP '(' type_specifier ',' type_specifier ')'
+        {
+          $$=$1;
+          parser_stack($$).id(ID_mathematical_function);
+          irept domain{ID_tuple};
+          domain.move_to_sub(parser_stack($3));
+          parser_stack($$).move_to_sub(domain);
+          mts($$, $5);
+        }
+        ;
+
 pragma_packed:
         {
           init($$);

diff --git a/src/ansi-c/scanner.l b/src/ansi-c/scanner.l
@@ -1319,11 +1319,13 @@ __decltype          { if(PARSER.cpp98 &&
 {CPROVER_PREFIX}"atomic"       { loc(); return TOK_CPROVER_ATOMIC; }
 {CPROVER_PREFIX}"forall"       { loc(); return TOK_FORALL; }
 {CPROVER_PREFIX}"exists"       { loc(); return TOK_EXISTS; }
+{CPROVER_PREFIX}"lambda"       { loc(); return TOK_LAMBDA; }
 {CPROVER_PREFIX}"array_of"     { loc(); return TOK_ARRAY_OF; }
 {CPROVER_PREFIX}"thread_local" { loc(); return TOK_THREAD_LOCAL; }
 {CPROVER_PREFIX}"bitvector"    { loc(); return TOK_CPROVER_BITVECTOR; }
 {CPROVER_PREFIX}"floatbv"      { loc(); return TOK_CPROVER_FLOATBV; }
 {CPROVER_PREFIX}"fixedbv"      { loc(); return TOK_CPROVER_FIXEDBV; }
+{CPROVER_PREFIX}"map"          { loc(); return TOK_CPROVER_MAP; }
 {CPROVER_PREFIX}"bool"         { loc(); return TOK_CPROVER_BOOL; }
 {CPROVER_PREFIX}"throw"        { loc(); return TOK_CPROVER_THROW; }
 {CPROVER_PREFIX}"catch"        { loc(); return TOK_CPROVER_CATCH; }

diff --git a/src/goto-symex/build_goto_trace.cpp b/src/goto-symex/build_goto_trace.cpp
@@ -124,7 +124,7 @@ static void set_internal_dynamic_object(
   if(expr.id()==ID_symbol)
   {
     const auto &type = expr.type();
-    if(type.id() != ID_code && type.id() != ID_mathematical_function)
+    if(type.id() != ID_code)
     {
       const irep_idt &id = to_ssa_expr(expr).get_original_name();
       const symbolt *symbol;

diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
@@ -234,7 +234,7 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
     const auto &type = as_const(expr).type();
 
     // we never rename function symbols
-    if(type.id() == ID_code || type.id() == ID_mathematical_function)
+    if(type.id() == ID_code)
     {
       rename<level>(expr.type(), to_symbol_expr(expr).get_identifier(), ns);
       return renamedt<exprt, level>{std::move(expr)};

diff --git a/src/goto-symex/renaming_level.cpp b/src/goto-symex/renaming_level.cpp
@@ -221,7 +221,7 @@ bool check_renaming_l1(const exprt &expr)
   {
     const auto &type = expr.type();
     if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
+      return type.id() != ID_code;
     if(!to_ssa_expr(expr).get_level_2().empty())
       return true;
     if(to_ssa_expr(expr).get_original_expr().type() != type)
@@ -262,7 +262,7 @@ bool check_renaming(const exprt &expr)
   {
     const auto &type = expr.type();
     if(!expr.get_bool(ID_C_SSA_symbol))
-      return type.id() != ID_code && type.id() != ID_mathematical_function;
+      return type.id() != ID_code;
     if(to_ssa_expr(expr).get_level_2().empty())
       return true;
     if(to_ssa_expr(expr).get_original_expr().type() != type)

diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
@@ -506,6 +506,10 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
     if(is_unbounded_array(type))
       return true;
 
+    // see if it's a function
+    if(type.id() == ID_mathematical_function)
+      return true;
+
     const bvt &bv1=convert_bv(expr.rhs());
 
     const irep_idt &identifier=

diff --git a/src/solvers/flattening/boolbv_equality.cpp b/src/solvers/flattening/boolbv_equality.cpp
@@ -35,6 +35,13 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
     return record_array_equality(expr);
   }
 
+  // see if it is a function
+  if(expr.lhs().type().id() == ID_mathematical_function)
+  {
+    functions.record(expr);
+    return prop.new_variable();
+  }
+
   const bvt &lhs_bv = convert_bv(expr.lhs());
   const bvt &rhs_bv = convert_bv(expr.rhs());
 

diff --git a/src/solvers/lowering/functions.cpp b/src/solvers/lowering/functions.cpp
@@ -18,6 +18,10 @@ void functionst::record(const function_application_exprt &function_application)
     function_application);
 }
 
+void functionst::record(const equal_exprt &function_equality)
+{
+}
+
 void functionst::add_function_constraints()
 {
   for(const auto &function : function_map)

diff --git a/src/solvers/lowering/functions.h b/src/solvers/lowering/functions.h
@@ -31,7 +31,8 @@ class functionst
   {
   }
 
-  void record(const function_application_exprt &function_application);
+  void record(const function_application_exprt &);
+  void record(const equal_exprt &);
 
   virtual void finish_eager_conversion()
   {

diff --git a/src/util/mathematical_types.h b/src/util/mathematical_types.h
@@ -73,13 +73,21 @@ class mathematical_function_typet : public type_with_subtypest
 {
 public:
   // the domain of the function is composed of zero, one, or
-  // many variables, given by their type
+  // many arguments, given by their type
   using domaint = std::vector<typet>;
 
   mathematical_function_typet(const domaint &_domain, const typet &_codomain)
     : type_with_subtypest(
         ID_mathematical_function,
-        {type_with_subtypest(irep_idt(), _domain), _codomain})
+        {type_with_subtypest(irep_idt{ID_tuple}, _domain), _codomain})
+  {
+  }
+
+  // short-hand for the 1-tuple domain
+  mathematical_function_typet(const typet &_domain, const typet &_codomain)
+    : type_with_subtypest(
+        ID_mathematical_function,
+        {type_with_subtypest(irep_idt{ID_tuple}, {_domain}), _codomain})
   {
   }