ce: fix parser for z3's bitvectors

CHANGES.md

@@ -37,6 +37,7 @@ IDE
 Counterexamples
   * Field names now use ident names instead of smt generated ones:
     int32qtint -> int32'int
+  * Fix parsing of bitvector counterexamples orignated from Z3
 
 Provers
   * support for Z3 4.8.1 (released Oct 16, 2018)

bench/ce/oracles/bv32_Z3,4.6.0_SP.oracle

 Strongest Postcondition
 bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
+Counter-example model:File bv32.mlw:
+Line 7:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000022" } }] } }
+Line 9:
+r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+[@model_trace:r]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000084" } }] } }
+Line 10:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000042" } }] } }
+Line 11:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000084" } }] } }
+
 bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
+Counter-example model:File bv32.mlw:
+Line 13:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000022" } }] } }
+Line 15:
+r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+[@model_trace:r]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000084" } }] } }
+Line 16:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000042" } }] } }
+Line 17:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000084" } }] } }
+

bench/ce/oracles/bv32_Z3,4.6.0_WP.oracle

 Weakest Precondition
 bench/ce/bv32.mlw Ce_int32bv VC dummy_update: Timeout or Unknown
+Counter-example model:File bv32.mlw:
+Line 7:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000022" } }] } }
+Line 9:
+r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+[@model_trace:r]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000084" } }] } }
+Line 10:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000042" } }] } }
+Line 11:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000084" } }] } }
+
 bench/ce/bv32.mlw Ce_int32bv VC dummy_update_with_int: Timeout or Unknown
+Counter-example model:File bv32.mlw:
+Line 13:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000022" } }] } }
+Line 15:
+r, [[@mlw:reference_var], [@introduced], [@field:0:contents],
+[@model_trace:r]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000084" } }] } }
+Line 16:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000042" } }] } }
+Line 17:
+r, [[@mlw:reference_var], [@introduced],
+[@field:0:contents]] = {"type" : "Record" ,
+"val" : {"Field" : [{"field" : "contents" , "value" : {"type" : "Bv" ,
+"val" : "#x00000084" } }] } }
+

src/driver/collect_data_model.ml

@@ -672,7 +672,8 @@ let create_list (projections_list: Ident.ident Mstr.t)
   Mstr.fold
     (fun key value list_acc ->
       try (convert_to_model_element ~set_str key value :: list_acc)
-      with Not_value when not (Debug.test_flag Debug.stack_trace) -> list_acc
+      with Not_value when not (Debug.test_flag Debug.stack_trace) ->
+        Debug.dprintf debug_cntex "Element creation failed: %s@." key; list_acc
       | e -> raise e)
     table
     []

src/driver/parse_smtv2_model_lexer.mll

@@ -24,7 +24,7 @@ let dec_num = num"."num
 let name = (['a'-'z']*'_'*['0'-'9']*)*
 let dummy = ('_''_''_')?
 let float_num = '#'('b' | 'x') hexa_num
-
+let bv_num = '#'('b' | 'x') hexa_num
 
 rule token = parse
   | '\n'
@@ -73,6 +73,7 @@ rule token = parse
   | "(_" space+ "NaN" space+ num space+ num ")" { FLOAT_VALUE Model_parser.Not_a_number }
   | "(fp" space+ (float_num as b) space+ (float_num as eb) space+ (float_num as sb) ")"
       { FLOAT_VALUE (Model_parser.interp_float b eb sb) }
+  | bv_num as bv_value { BITVECTOR_VALUE bv_value }
 
   | num as integer
       { INT_STR (integer) }