Merge pull request #3284 from diffblue/smt2-bv-fix

smt2 bit vector fix [blocks: any PR adding CBMC tests]

Author: tautschnig

.travis.yml

@@ -354,7 +354,7 @@ install:
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
-  - scripts/delete_failing_smt2_solver_tests ; env UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
+  - scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2

buildspec.yml

@@ -25,7 +25,7 @@ phases:
       - make -C unit test
       - make -C regression test
       - scripts/delete_failing_smt2_solver_tests
-      - make -C regression/cbmc test-cprover-smt2
+      - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test
       - make -C jbmc/regression test
       - echo Build completed on `date`

scripts/delete_failing_smt2_solver_tests

@@ -1,43 +1,25 @@
 #!/bin/sh
 
 cd regression/cbmc
-rm ACSL/operators.desc
 rm Address_of2/test.desc
 rm Anonymous_Struct3/test.desc
 rm Array_Initialization2/test.desc
 rm Array_operations1/test.desc
-rm Assumption1/test.desc
-rm BV_Arithmetic1/test.desc
 rm BV_Arithmetic6/test.desc
 rm Bitfields1/test.desc
 rm Bitfields3/test.desc
-rm Bool1/test.desc
-rm Bool2/test.desc
-rm Bool3/test.desc
-rm Boolean_Guards1/test.desc
-rm Computed-Goto1/test.desc
 rm Division2/test.desc
 rm Double-to-float-no-simp1/test.desc
 rm Double-to-float-no-simp1-fix1/test.desc
 rm Double-to-float-no-simp1-fix2/test.desc
-rm Ellipsis2/test.desc
 rm Empty_struct1/test.desc
-rm Endianness1/test.desc
-rm Endianness2/test.desc
 rm Endianness3/test.desc
 rm Endianness4/test.desc
 rm Endianness6/test.desc
 rm Endianness7/test.desc
-rm Endianness8/test.desc
-rm Error_Label1/test.desc
-rm Error_Label2/test.desc
-rm Error_Label3/test.desc
-rm Eval_Order1/test.desc
-rm Failing_Assert1/test.desc
 rm Fixedbv3/test.desc
 rm Fixedbv5/test.desc
 rm Fixedbv6/test.desc
-rm Fixedbv8/test.desc
 rm Float-Rounding1/test.desc
 rm Float-div1/test.desc
 rm Float-div2/test.desc
@@ -53,7 +35,6 @@ rm Float-no-simp6/test.desc
 rm Float-no-simp7/test.desc
 rm Float-no-simp8/test.desc
 rm Float-no-simp9/test.desc
-rm Float-overflow2/test.desc
 rm Float-smt2-1/test.desc
 rm Float-to-double1/test.desc
 rm Float-to-double2/test.desc
@@ -74,68 +55,31 @@ rm Float4/test.desc
 rm Float5/test.desc
 rm Float6/test.desc
 rm Float8/test.desc
-rm Free1/test.desc
 rm Free2/test.desc
-rm Free3/test.desc
-rm Free4/test.desc
 rm Function1/test.desc
-rm Function2/test.desc
-rm Function5/test.desc
-rm Function8/test.desc
-rm Function9/test.desc
-rm Function_Eval_Order2/test.desc
-rm Function_Pointer15/test.desc
-rm Function_Pointer2/test.desc
 rm Function_Pointer3/test.desc
-rm Function_Pointer6/test.desc
-rm Function_Pointer8/test.desc
-rm Function_Pointer9/test.desc
-rm Initialization5/test.desc
-rm Initialization6/test.desc
 rm Linking4/test.desc
 rm Linking7/test.desc
-rm Linking8/test.desc
-rm Local_out_of_scope1/test.desc
-rm Local_out_of_scope2/test.desc
-rm Local_out_of_scope3/test.desc
-rm Malloc15/test.desc
 rm Malloc17/test.desc
 rm Malloc18/test.desc
 rm Malloc19/test.desc
 rm Malloc20/test.desc
-rm Malloc21/test.desc
 rm Malloc23/test.desc
 rm Malloc24/test.desc
 rm Memmove1/test.desc
 rm Memory_leak1/test.desc
 rm Memory_leak2/test.desc
-rm Mod1/test.desc
-rm Mod2/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 Multiple_Properties1/test.desc
-rm Negation2/test.desc
-rm Overflow_Addition1/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_Arithmetic5/test.desc
 rm Pointer_Arithmetic6/test.desc
-rm Pointer_Arithmetic8/test.desc
-rm Pointer_array1/test.desc
-rm Pointer_array2/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_extract1/test.desc
 rm Pointer_byte_extract2/test.desc
 rm Pointer_byte_extract3/test.desc
 rm Pointer_byte_extract4/test.desc
@@ -158,30 +102,19 @@ rm Quantifiers-not-exists/test.desc
 rm Quantifiers-two-dimension-array/test.desc
 rm Quantifiers-type/test.desc
 rm Quantifiers1/test.desc
-rm Recursion4/test.desc
 rm Recursion5/test.desc
-rm Sideeffects5/test.desc
-rm Sideeffects6/test.desc
-rm String2/test.desc
 rm String6/test.desc
 rm Struct_Bytewise1/test.desc
 rm Struct_Bytewise2/test.desc
 rm Struct_Initialization2/test.desc
-rm Struct_Initialization5/test.desc
 rm Struct_Padding1/test.desc
-rm Typecast1/test.desc
-rm Typecast2/test.desc
-rm Undefined_Function1/test.desc
-rm Undefined_Function2/test.desc
 rm Undefined_Shift1/test.desc
 rm Union_Initialization1/test.desc
 rm Unwinding_Locality1/test.desc
-rm abs1/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 atomic_section_seq1/test.desc
 rm big-endian-array1/test.desc
 rm bounds_check1/test.desc
 rm byte_update1/test.desc
@@ -191,16 +124,8 @@ rm byte_update4/test.desc
 rm byte_update5/test.desc
 rm byte_update6/test.desc
 rm byte_update7/test.desc
-rm byte_update8/test.desc
-rm byte_update9/test.desc
-rm c99_Bool/test.desc
-rm cprover_bool1/test.desc
-rm divide-by-one-simplify/test.desc
 rm dynamic_size1/stack_object.desc
 rm dynamic_size1/test.desc
-rm dynamic_sizeof1/test.desc
-rm enum3/test.desc
-rm enum5/test.desc
 rm equality_through_array1/test.desc
 rm equality_through_array2/test.desc
 rm equality_through_array3/test.desc
@@ -211,109 +136,60 @@ 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_struct1/test.desc
-rm equality_through_struct2/test.desc
-rm equality_through_struct3/test.desc
-rm equality_through_struct4/test.desc
-rm equality_through_struct5/test.desc
 rm equality_through_struct_containing_arrays1/test.desc
 rm equality_through_struct_containing_arrays2/test.desc
 rm equality_through_struct_containing_arrays3/test.desc
 rm equality_through_union1/test.desc
 rm equality_through_union2/test.desc
 rm equality_through_union3/test.desc
-rm exit1/test.desc
-rm extern_initialization1/test.desc
 rm fgets1/test.desc
-rm for2/test.desc
 rm full_slice1/test.desc
 rm full_slice2/test.desc
 rm gcc_bswap1/test.desc
-rm gcc_c99-bool-1/test.desc
-rm gcc_local_label1/test.desc
-rm gcc_popcount1/test.desc
 rm gcc_statement_expression4/test.desc
 rm gcc_switch_case_range1/test.desc
 rm gcc_switch_case_range2/test.desc
 rm gcc_vector1/test.desc
 rm gcc_vector2/test.desc
-rm getenv-overflow1/test.desc
-rm goto1/test.desc
-rm goto2/test.desc
-rm goto4/test.desc
-rm goto5/test.desc
 rm graphml_witness1/test.desc
 rm havoc_object1/test.desc
 rm hex_trace/test.desc
-rm if1/test.desc
 rm if2/test.desc
-rm if3/test.desc
-rm if4/test.desc
 rm inet_endian1/test.desc
 rm int-to-float2/test.desc
 rm integer-assignments1/test.desc
-rm json1/test.desc
 rm little-endian-array1/test.desc
-rm member1/test.desc
-rm memcpy1/test.desc
-rm memcpy2/test.desc
-rm memcpy3/test.desc
 rm memory_allocation1/test.desc
-rm memset1/test.desc
 rm memset3/test.desc
 rm mm_io1/test.desc
 rm nested_label1/test.desc
 rm no_nondet_static/test.desc
-rm null1/test.desc
-rm null2/test.desc
-rm path-per-path-vccs/test.desc
 rm pipe1/test.desc
-rm pointer-extra-checks/test.desc
 rm pointer-function-parameters/test.desc
 rm pointer-function-parameters-2/test.desc
-rm posix_memalign/test.desc
-rm printf1/test.desc
 rm read1/test.desc
 rm realloc1/test.desc
 rm realloc2/test.desc
-rm return2/test.desc
-rm return5/test.desc
 rm scanf1/test.desc
-rm self_loops_to_assumptions1/no-assume.desc
 rm simple_assert/test.desc
 rm stack-trace/test.desc
 rm strcat1/test.desc
-rm struct1/test.desc
 rm struct10/test.desc
-rm struct3/test.desc
 rm struct6/test.desc
 rm struct7/test.desc
-rm struct8/test.desc
 rm struct9/test.desc
-rm switch1/test.desc
-rm switch2/test.desc
-rm switch3/test.desc
-rm switch4/test.desc
-rm switch5/test.desc
-rm trace_address_arithmetic1/test.desc
 rm trace-values/trace-values.desc
-rm trace_options_json_extended/extended.desc
-rm trace_options_json_extended/non-extended.desc
-rm trace_show_code/test.desc
+rm trace_address_arithmetic1/test.desc
 rm trace_show_function_calls/test.desc
 rm uncaught_exceptions_analysis1/test.desc
 rm uniform_array1/test.desc
 rm union11/union_list.desc
-rm union3/test.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 unwind_counters2/test.desc
-rm unwind_counters3/test.desc
-rm variable-access-to-constant-array/test.desc
 rm void_pointer2/test.desc
 rm void_pointer3/test.desc
 rm while1/test.desc

src/solvers/smt2/smt2_conv.cpp

@@ -268,11 +268,11 @@ constant_exprt smt2_convt::parse_literal(
     if(type.id()==ID_floatbv)
     {
       const floatbv_typet &floatbv_type=to_floatbv_type(type);
-      constant_exprt s1=parse_literal(src.get_sub()[1], bv_typet(1));
-      constant_exprt s2=
-        parse_literal(src.get_sub()[2], bv_typet(floatbv_type.get_e()));
-      constant_exprt s3=
-        parse_literal(src.get_sub()[3], bv_typet(floatbv_type.get_f()));
+      constant_exprt s1 = parse_literal(src.get_sub()[1], unsignedbv_typet(1));
+      constant_exprt s2 =
+        parse_literal(src.get_sub()[2], unsignedbv_typet(floatbv_type.get_e()));
+      constant_exprt s3 =
+        parse_literal(src.get_sub()[3], unsignedbv_typet(floatbv_type.get_f()));
       // stitch the bits together
       std::string bits=id2string(s1.get_value())+
                        id2string(s2.get_value())+
@@ -309,7 +309,6 @@ constant_exprt smt2_convt::parse_literal(
 
   if(type.id()==ID_signedbv ||
      type.id()==ID_unsignedbv ||
-     type.id()==ID_bv ||
      type.id()==ID_c_enum ||
      type.id()==ID_c_bool)
   {
@@ -376,7 +375,7 @@ exprt smt2_convt::parse_union(
   PRECONDITION(!type.components().empty());
   const union_typet::componentt &first=type.components().front();
   std::size_t width=boolbv_width(type);
-  exprt value=parse_rec(src, bv_typet(width));
+  exprt value = parse_rec(src, unsignedbv_typet(width));
   if(value.is_nil())
     return nil_exprt();
   const typecast_exprt converted(value, first.type());
@@ -415,7 +414,7 @@ exprt smt2_convt::parse_struct(
   {
     // These are just flattened, i.e., we expect to see a monster bit vector.
     std::size_t total_width=boolbv_width(type);
-    exprt l=parse_literal(src, bv_typet(total_width));
+    exprt l = parse_literal(src, unsignedbv_typet(total_width));
     if(!l.is_constant())
       return nil_exprt();
 
@@ -456,7 +455,6 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
      type.id()==ID_integer ||
      type.id()==ID_rational ||
      type.id()==ID_real ||
-     type.id()==ID_bv ||
      type.id()==ID_fixedbv ||
      type.id()==ID_floatbv)
   {
@@ -473,7 +471,7 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &_type)
   {
     // these come in as bit-vector literals
     std::size_t width=boolbv_width(type);
-    constant_exprt bv_expr=parse_literal(src, bv_typet(width));
+    constant_exprt bv_expr = parse_literal(src, unsignedbv_typet(width));
 
     mp_integer v = numeric_cast_v<mp_integer>(bv_expr);