Merge pull request #3233 from diffblue/cprover-smt2-2

SMT2 backend testing

Author: forejtv

.travis.yml

@@ -354,6 +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
   - 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

@@ -24,6 +24,8 @@ phases:
     commands:
       - make -C unit test
       - make -C regression test
+      - scripts/delete_failing_smt2_solver_tests
+      - make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test
       - make -C jbmc/regression test
       - echo Build completed on `date`

regression/cbmc/Makefile

@@ -3,6 +3,9 @@ default: tests.log
 test:
 	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
 
+test-cprover-smt2:
+	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
+
 tests.log: ../test.pl
 	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
 

scripts/delete_failing_smt2_solver_tests

@@ -0,0 +1,317 @@
+#!/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
+rm Float-div3/test.desc
+rm Float-flags-no-simp1/test.desc
+rm Float-flags-simp1/test.desc
+rm Float-no-simp1/test.desc
+rm Float-no-simp2/test.desc
+rm Float-no-simp3/test.desc
+rm Float-no-simp4/test.desc
+rm Float-no-simp5/test.desc
+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
+rm Float-to-int1/test.desc
+rm Float-to-int2/test.desc
+rm Float-to-int3/test.desc
+rm Float-zero-sum1/test.desc
+rm Float12/test.desc
+rm Float13/test.desc
+rm Float19/test.desc
+rm Float20/test.desc
+rm Float21/test.desc
+rm Float22/test.desc
+rm Float23/test.desc
+rm Float24/test.desc
+rm Float3/test.desc
+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
+rm Pointer_byte_extract5/no-simplify.desc
+rm Pointer_byte_extract5/test.desc
+rm Pointer_byte_extract7/test.desc
+rm Pointer_byte_extract9/test.desc
+rm Pointer_difference1/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 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
+rm byte_update2/test.desc
+rm byte_update3/test.desc
+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
+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_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 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_show_function_calls/test.desc
+rm uncaught_exceptions_analysis1/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/cbmc/cbmc_parse_options.cpp

@@ -327,6 +327,12 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("smt2", true);
   }
 
+  if(cmdline.isset("cprover-smt2"))
+  {
+    options.set_option("cprover-smt2", true), solver_set = true;
+    options.set_option("smt2", true);
+  }
+
   if(cmdline.isset("mathsat"))
   {
     options.set_option("mathsat", true), solver_set=true;
@@ -955,8 +961,9 @@ void cbmc_parse_optionst::help()
     " --localize-faults            localize faults (experimental)\n"
     " --smt2                       use default SMT2 solver (Z3)\n"
     " --boolector                  use Boolector\n"
-    " --mathsat                    use MathSAT\n"
+    " --cprover-smt2               use CPROVER SMT2 solver\n"
     " --cvc4                       use CVC4\n"
+    " --mathsat                    use MathSAT\n"
     " --yices                      use Yices\n"
     " --z3                         use Z3\n"
     " --refine                     use refinement procedure (experimental)\n"

src/cbmc/cbmc_parse_options.h

@@ -47,6 +47,7 @@ class optionst;
   "(no-assertions)(no-assumptions)" \
   "(xml-ui)(xml-interface)(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(opensmt)(mathsat)" \
+  "(cprover-smt2)" \
   "(no-sat-preprocessor)" \
   "(beautify)" \
   "(dimacs)(refine)(max-node-refinement):(refine-arrays)(refine-arithmetic)"\

src/cbmc/cbmc_solvers.cpp

@@ -41,6 +41,8 @@ smt2_dect::solvert cbmc_solverst::get_smt2_solver_type() const
 
   if(options.get_bool_option("boolector"))
     s=smt2_dect::solvert::BOOLECTOR;
+  else if(options.get_bool_option("cprover-smt2"))
+    s = smt2_dect::solvert::CPROVER_SMT2;
   else if(options.get_bool_option("mathsat"))
     s=smt2_dect::solvert::MATHSAT;
   else if(options.get_bool_option("cvc3"))