Merge pull request #3521 from diffblue/smt2_solver_arrays

smt2_solver: arrays

Author: Daniel Kroening

regression/smt2_solver/arrays/arrays1.desc

@@ -0,0 +1,8 @@
+CORE
+arrays1.smt2
+
+^EXIT=0$
+^SIGNAL=0$
+^sat$
+^\(\(array2 \(store .* \(_ bv1 16\) \(_ bv16 8\)\)\)\)$
+--

regression/smt2_solver/arrays/arrays1.smt2

@@ -0,0 +1,7 @@
+(set-logic QF_ABV)
+
+(declare-const array1 (Array (_ BitVec 16) (_ BitVec 8)))
+(define-const array2 (Array (_ BitVec 16) (_ BitVec 8)) (store array1 #x0001 #x10))
+
+(check-sat)
+(get-value (array2))

scripts/delete_failing_smt2_solver_tests

@@ -2,12 +2,9 @@
 
 cd regression/cbmc
 rm Anonymous_Struct3/test.desc
-rm Array_Initialization2/test.desc
 rm Array_operations1/test.desc
 rm Bitfields1/test.desc
 rm Bitfields3/test.desc
-rm Boolean_Guards1/test.desc
-rm Computed-Goto1/test.desc
 rm Empty_struct1/test.desc
 rm Endianness4/test.desc
 rm Endianness6/test.desc
@@ -39,35 +36,19 @@ rm Float4/test.desc
 rm Float5/test.desc
 rm Float6/test.desc
 rm Float8/test.desc
-rm Function1/test.desc
-rm Initialization6/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
-rm Local_out_of_scope3/test.desc
-rm Malloc17/test.desc
-rm Malloc18/test.desc
 rm Malloc19/test.desc
-rm Malloc21/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc
 rm Memory_leak2/test.desc
-rm Multi_Dimensional_Array1/test.desc
 rm Multi_Dimensional_Array2/test.desc
-rm Multi_Dimensional_Array3/test.desc
-rm Multi_Dimensional_Array4/test.desc
-rm Multi_Dimensional_Array6/test.desc
 rm Overflow_Leftshift1/test.desc
 rm Overflow_Multiplication1/test.desc
 rm Overflow_Subtraction1/test.desc
-rm Pointer_Arithmetic1/test.desc
 rm Pointer_Arithmetic10/test.desc
 rm Pointer_Arithmetic11/test.desc
 rm Pointer_Arithmetic12/test.desc
-rm Pointer_Arithmetic6/test.desc
-rm Pointer_array3/test.desc
-rm Pointer_array4/test.desc
-rm Pointer_array5/test.desc
-rm Pointer_array6/test.desc
 rm Pointer_byte_extract2/test.desc
 rm Pointer_byte_extract3/test.desc
 rm Pointer_byte_extract4/test.desc
@@ -76,34 +57,22 @@ rm Pointer_byte_extract5/test.desc
 rm Pointer_byte_extract7/test.desc
 rm Pointer_byte_extract9/test.desc
 rm Promotion3/test.desc
-rm Promotion4/test.desc
 rm Quantifiers-assertion/test.desc
 rm Quantifiers-assignment/test.desc
-rm Quantifiers-copy/test.desc
 rm Quantifiers-if/test.desc
-rm Quantifiers-initialisation/test.desc
 rm Quantifiers-initialisation2/test.desc
 rm Quantifiers-invalid-var-range/test.desc
 rm Quantifiers-not/test.desc
 rm Quantifiers-not-exists/test.desc
 rm Quantifiers-two-dimension-array/test.desc
 rm Quantifiers-type/test.desc
-rm Quantifiers1/test.desc
-rm String2/test.desc
-rm Struct_Bytewise1/test.desc
 rm Struct_Bytewise2/test.desc
-rm Struct_Initialization2/test.desc
-rm Struct_Padding1/test.desc
 rm Typecast1/test.desc
 rm Union_Initialization1/test.desc
-rm Unwinding_Locality1/test.desc
 rm address_space_size_limit1/test.desc
 rm address_space_size_limit3/test.desc
-rm argv1/test.desc
 rm array-tests/test.desc
-rm big-endian-array1/test.desc
 rm bounds_check1/test.desc
-rm byte_update1/test.desc
 rm byte_update2/test.desc
 rm byte_update3/test.desc
 rm byte_update4/test.desc
@@ -114,61 +83,35 @@ rm byte_update8/test.desc
 rm byte_update9/test.desc
 rm compact-trace/test.desc
 rm dynamic_size1/stack_object.desc
-rm equality_through_array1/test.desc
-rm equality_through_array2/test.desc
-rm equality_through_array3/test.desc
-rm equality_through_array4/test.desc
-rm equality_through_array5/test.desc
-rm equality_through_array6/test.desc
-rm equality_through_array_of_struct1/test.desc
-rm equality_through_array_of_struct2/test.desc
-rm equality_through_array_of_struct3/test.desc
-rm equality_through_array_of_struct4/test.desc
 rm equality_through_struct_containing_arrays1/test.desc
 rm equality_through_struct_containing_arrays2/test.desc
 rm equality_through_union1/test.desc
 rm equality_through_union2/test.desc
 rm equality_through_union3/test.desc
 rm gcc_bswap1/test.desc
-rm gcc_c99-bool-1/test.desc
-rm gcc_statement_expression4/test.desc
 rm gcc_vector1/test.desc
-rm gcc_vector2/test.desc
 rm graphml_witness1/test.desc
-rm havoc_object1/test.desc
-rm little-endian-array1/test.desc
-rm memcpy/memcpy4.desc
 rm memory_allocation1/test.desc
-rm memset1/test.desc
-rm mm_io1/test.desc
-rm no_nondet_static/test.desc
-rm null1/test.desc
 rm pointer-function-parameters-struct-mutual-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion/test.desc
 rm pointer-function-parameters-struct-simple-recursion-2/test.desc
 rm pointer-function-parameters-struct-simple-recursion-3/test.desc
 rm scanf1/test.desc
-rm simple_assert/test.desc
 rm stack-trace/test.desc
 rm struct10/test.desc
 rm struct6/test.desc
 rm struct7/test.desc
 rm struct9/test.desc
 rm trace-values/trace-values.desc
 rm trace_address_arithmetic1/test.desc
-rm trace_options_json_extended/extended.desc
-rm trace_options_json_extended/non-extended.desc
 rm trace_show_function_calls/test.desc
-rm uniform_array1/test.desc
 rm union11/union_list.desc
 rm union5/test.desc
 rm union6/test.desc
 rm union7/test.desc
 rm union8/test.desc
 rm union9/test.desc
-rm unsigned___int128/test.desc
 rm variable-access-to-constant-array/test.desc
 rm void_pointer2/test.desc
 rm void_pointer3/test.desc
 rm void_pointer4/test.desc
-rm while1/test.desc

src/solvers/smt2/smt2_format.cpp

@@ -22,6 +22,12 @@ std::ostream &smt2_format_rec(std::ostream &out, const typet &type)
     out << "Int";
   else if(type.id() == ID_real)
     out << "Real";
+  else if(type.id() == ID_array)
+  {
+    const auto &array_type = to_array_type(type);
+    out << "(Array " << smt2_format(array_type.size().type()) << ' '
+        << smt2_format(array_type.subtype()) << ')';
+  }
   else
     out << "? " << type.id();
 
@@ -87,6 +93,13 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
     else
       out << identifier;
   }
+  else if(expr.id() == ID_with && expr.type().id() == ID_array)
+  {
+    const auto &with_expr = to_with_expr(expr);
+    out << "(store " << smt2_format(with_expr.old()) << ' '
+        << smt2_format(with_expr.where()) << ' '
+        << smt2_format(with_expr.new_value()) << ')';
+  }
   else
     out << "? " << expr.id();
 

src/solvers/smt2/smt2_parser.cpp

@@ -644,6 +644,31 @@ exprt smt2_parsert::function_application()
       {
         return binary(ID_implies, op);
       }
+      else if(id == "select")
+      {
+        // array index
+        if(op.size() != 2)
+          throw error("select takes two operands");
+
+        if(op[0].type().id() != ID_array)
+          throw error("select expects array operand");
+
+        return index_exprt(op[0], op[1]);
+      }
+      else if(id == "store")
+      {
+        // array update
+        if(op.size() != 3)
+          throw error("store takes three operands");
+
+        if(op[0].type().id() != ID_array)
+          throw error("store expects array operand");
+
+        if(to_array_type(op[0].type()).subtype() != op[2].type())
+          throw error("store expects value that matches array element type");
+
+        return with_exprt(op[0], op[1], op[2]);
+      }
       else
       {
         // rummage through id_map
@@ -944,10 +969,7 @@ typet smt2_parsert::sort()
       // we can turn arrays that map an unsigned bitvector type
       // to something else into our 'array_typet'
       if(domain.id() == ID_unsignedbv)
-      {
-        const auto size = to_unsignedbv_type(domain).largest_expr();
-        return array_typet(range, size);
-      }
+        return array_typet(range, infinity_exprt(domain));
       else
         throw error("unsupported array sort");
     }
@@ -1089,6 +1111,38 @@ void smt2_parsert::command(const std::string &c)
     entry.type = type;
     entry.definition = nil_exprt();
   }
+  else if(c == "define-const")
+  {
+    if(next_token() != SYMBOL)
+      throw error("expected a symbol after define-const");
+
+    const irep_idt id = buffer;
+
+    if(id_map.find(id) != id_map.end())
+    {
+      std::ostringstream msg;
+      msg << "identifier `" << id << "' defined twice";
+      throw error(msg.str());
+    }
+
+    const auto type = sort();
+    const auto value = expression();
+
+    // check type of value
+    if(value.type() != type)
+    {
+      std::ostringstream msg;
+      msg << "type mismatch in constant definition: expected `"
+          << smt2_format(type) << "' but got `" << smt2_format(value.type())
+          << '\'';
+      throw error(msg.str());
+    }
+
+    // create the entry
+    auto &entry = id_map[id];
+    entry.type = type;
+    entry.definition = value;
+  }
   else if(c=="define-fun")
   {
     if(next_token()!=SYMBOL)

src/solvers/smt2/smt2_solver.cpp

@@ -401,6 +401,13 @@ int solver(std::istream &in)
       message.error().source_location.set_line(error.get_line_no());
       message.error() << error.what() << messaget::eom;
     }
+    catch(const analysis_exceptiont &error)
+    {
+      smt2_solver.skip_to_end_of_list();
+      error_found = true;
+      messaget message(message_handler);
+      message.error() << error.what() << messaget::eom;
+    }
   }
 
   if(error_found)