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.

Author: kroening

regression/cbmc/map-type/basic1.c

@@ -0,0 +1,10 @@
+int main()
+{
+  __CPROVER_map(int, int) my_map;
+
+  my_map[1] = 10;
+  my_map[2] = 20;
+
+  __CPROVER_assert(my_map[1] == 10, "[1]");
+  __CPROVER_assert(my_map[2] == 20, "[2]");
+}

regression/cbmc/map-type/basic1.desc

@@ -0,0 +1,8 @@
+CORE
+basic1.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

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);

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.

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)
   {

src/ansi-c/parser.y

@@ -206,6 +206,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"
@@ -1111,6 +1112,7 @@ type_specifier:
         | typedef_type_specifier
         | typeof_type_specifier
         | atomic_type_specifier
+        | map_type_specifier
         ;
 
 declaration_qualifier_list:
@@ -1554,6 +1556,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($$);

src/ansi-c/scanner.l

@@ -1324,6 +1324,7 @@ __decltype          { if(PARSER.cpp98 &&
 {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; }

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})
+  {
+  }
+
+  // sort-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})
   {
   }