Commit e9bc3ea1 authored by Sylvain Dailler's avatar Sylvain Dailler

Automatic insertion of model_vc and model_vc_post labels.

Also update of ce/bench
parent 429c2197
......@@ -2,11 +2,11 @@ module Ce_int32
use import ref.Ref
use export mach.int.Int32
let dummy_update (r: ref int32)
let dummy_update (r: ref int32)
requires { to_int !r = 22}
ensures { "model_vc" to_int !r = 42} =
ensures {to_int !r = 42} =
r := of_int 42;
r := !r + !r;
end
ce/int32.mlw Ce_int32 WP_parameter dummy_update : Unknown (other)
Counter-example model:File int32.mlw:
Line 6:
r = {"type" : "Integer" ,
"val" : "22" }
Line 8:
the check fails with all inputs
r = {"type" : "Integer" , "val" : "22" }
Line 9:
r = {"type" : "Integer" ,
"val" : "42" }
......
......@@ -17,18 +17,18 @@ module M
**************************************)
use import map.Map
let test_map (x : ref (map int int)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let test_map_multidim1 (x : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }
ensures { !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
let test_map_multidim2 (x : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }
ensures { !x[0][0] <> !x[1][1] }
=
let x0 = Map.get !x 0 in
let x0 = Map.set x0 0 3 in
......@@ -62,14 +62,14 @@ module M
projfi, projf1, and projf2
Warning: cvc4 is not able to handle projections there *)
let proj_map_test1 (x "model_projected" : ref (map int int)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* No projection function for bool -> the array should be
present in counterexample as it is. *)
let proj_map_test2 (x "model_projected" : ref (map int bool)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
ensures { !x[0] <> !x[1] }
=
x := Map.set !x 0 true
......
......@@ -3,12 +3,20 @@ ce/record_map.mlw M WP_parameter record_map_proj_test2 : Unknown (other)
ce/record_map.mlw M WP_parameter record_map_proj_test3 : Unknown (other)
Counter-example model:File record_map.mlw:
Line 51:
re_rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 53:
rec_map.f_map = {"type" : "Array" ,
rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 54:
old re_rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
rec_map.g_bool = {"type" : "Boolean" ,
old re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
old rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
......@@ -5,6 +5,10 @@ Line 46:
rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
Line 47:
old rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test3 : Unknown (other)
Counter-example model:File record_map.mlw:
......@@ -12,8 +16,23 @@ Line 51:
re_rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 53:
rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 54:
old re_rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
old re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
old rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
old rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
......@@ -5,6 +5,10 @@ Line 46:
rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
Line 47:
old rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
ce/record_map.mlw M WP_parameter record_map_proj_test3 : Unknown (other)
Counter-example model:File record_map.mlw:
......@@ -12,8 +16,23 @@ Line 51:
re_rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 53:
rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
Line 54:
old re_rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "1" } }] }
old re_rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
old rec_map.f_map = {"type" : "Array" ,
"val" : [{"others" : {"type" : "Integer" ,
"val" : "0" } }] }
old rec_map.g_bool = {"type" : "Boolean" ,
"val" : false }
......@@ -25,7 +25,7 @@ module M
meta "model_projection" function projf_r_g
let record_match_eval_test1 (x : r) : int
ensures { "model_vc_post" result = 1 }
ensures { result = 1 }
=
if x.g then
x.f
......@@ -43,7 +43,7 @@ module M
x := { !x with f = 6}
let record_match_eval_test4 (x : ref r) : r
ensures { "model_vc_post" result.g }
ensures { result.g }
=
x := { !x with f = 6 };
!x
......@@ -51,7 +51,7 @@ module M
val re "model_projected" : ref r
let test_record_match_eval_test5 (x : ref r) : r
ensures { "model_vc_post" result = !re }
ensures { result = !re }
=
x := { !x with f = 6 };
!x
......
......@@ -15,6 +15,9 @@ Counter-example model:File records.mlw:
Line 35:
x.field_f = {"type" : "Integer" ,
"val" : "0" }
Line 36:
old x.field_f = {"type" : "Integer" ,
"val" : "0" }
ce/records.mlw M WP_parameter record_match_eval_test3 : Unknown (other)
Counter-example model:File records.mlw:
......
......@@ -4,17 +4,24 @@ module M
use import int.Int
let test_post (x: int) (y : ref int): unit
ensures { "model_vc_post" old !y >= x }
ensures {old !y >= x }
=
y := x - 1 + !y
let test_post2 (x: int) (y : ref int): unit
requires {x > 42}
ensures {old !y > !y + x}
=
y := x - 1 + !y
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
val y :ref int
let incr ( x23: ref int ): unit
ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
ensures { !x23 = old !x23 + 2 + !y }
=
(*#"random_path.random" 62 27 32#*)
y := !y + 1;
......@@ -22,11 +29,11 @@ module M
x23 := !x23 + 1
let test_loop ( x: ref int ): unit
ensures { "model_vc_post" !x < old !x }
ensures { !x < old !x }
=
'L: incr x;
'M: while !x > 0 do
invariant { "model_vc" !x > at !x 'L + at !x 'M }
invariant { !x > at !x 'L + at !x 'M }
variant { !x }
x := !x - 1
done
......
......@@ -12,41 +12,57 @@ Line 9:
y = {"type" : "Integer" ,
"val" : "0" }
ce/ref.mlw M WP_parameter test_post2 : Unknown (other)
Counter-example model:File ref.mlw:
Line 11:
x = {"type" : "Integer" , "val" : "43" }
y = {"type" : "Integer" ,
"val" : "0" }
Line 13:
old x = {"type" : "Integer" , "val" : "43" }
y = {"type" : "Integer" ,
"val" : "42" }
old y = {"type" : "Integer" ,
"val" : "0" }
Line 15:
y = {"type" : "Integer" ,
"val" : "42" }
ce/ref.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File ref.mlw:
Line 14:
Line 21:
y = {"type" : "Integer" , "val" : "-2" }
Line 16:
Line 23:
x23 = {"type" : "Integer" , "val" : "0" }
Line 17:
Line 24:
x23 = {"type" : "Integer" , "val" : "2" }
old x23 = {"type" : "Integer" ,
"val" : "0" }
y = {"type" : "Integer" ,
"val" : "-1" }
Line 20:
Line 27:
y = {"type" : "Integer" , "val" : "-1" }
Line 21:
Line 28:
x23 = {"type" : "Integer" , "val" : "1" }
Line 22:
Line 29:
x23 = {"type" : "Integer" ,
"val" : "2" }
ce/ref.mlw M WP_parameter test_loop : Unknown (other)
Counter-example model:File ref.mlw:
Line 24:
Line 31:
x = {"type" : "Integer" , "val" : "0" }
Line 25:
Line 32:
x = {"type" : "Integer" , "val" : "0" }
old x = {"type" : "Integer" ,
"val" : "0" }
Line 27:
Line 34:
x = {"type" : "Integer" , "val" : "-1" }
y = {"type" : "Integer" ,
"val" : "-3" }
Line 28:
Line 35:
x = {"type" : "Integer" , "val" : "0" }
Line 29:
Line 36:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" ,
"val" : "-1" }
......
......@@ -3,6 +3,11 @@ Prover exit status: exited with status 1
Prover output:
ce/ref.mlw M WP_parameter test_post2 : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/ref.mlw M WP_parameter incr : HighFailure
Prover exit status: exited with status 1
Prover output:
......
ce/ref.mlw M WP_parameter test_post : Timeout
ce/ref.mlw M WP_parameter test_post2 : Timeout
ce/ref.mlw M WP_parameter incr : Timeout
ce/ref.mlw M WP_parameter test_loop : Timeout
......@@ -81,6 +81,17 @@ end
(loc, Some (add_model_trace id), ghost, ty)
| _ -> b
let model_vc_label = Ident.create_label "model_vc"
let model_vc_post_label = Ident.create_label "model_vc_post"
let add_model_vc_label t =
{t with term_desc = Tnamed (Lstr model_vc_label, t)}
let add_model_vc_post_label t =
{t with term_desc = Tnamed (Lstr model_vc_post_label, t)}
let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
let mk_int_const neg lit =
......@@ -807,7 +818,8 @@ expr_:
| ABSTRACT spec seq_expr END
{ Eabstract($3, $2) }
| assertion_kind LEFTBRC term RIGHTBRC
{ Eassert ($1, $3) }
{ let t = add_model_vc_label $3 in
Eassert ($1, t) }
| label expr %prec prec_named
{ Enamed ($1, $2) }
| expr cast
......@@ -884,11 +896,13 @@ spec:
single_spec:
| REQUIRES LEFTBRC term RIGHTBRC
{ { empty_spec with sp_pre = [$3] } }
{ let t = add_model_vc_label $3 in
{ empty_spec with sp_pre = [t] } }
| ENSURES LEFTBRC ensures RIGHTBRC
{ { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
{ { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
{ let l = List.map (fun (x, t) -> x, add_model_vc_post_label t) $3 in
{ empty_spec with sp_post = [floc $startpos($3) $endpos($3), l] } }
| RAISES LEFTBRC bar_list1(raises) RIGHTBRC
{ { empty_spec with sp_xpost = [floc $startpos($3) $endpos($3), $3] } }
| READS LEFTBRC comma_list0(lqualid) RIGHTBRC
......@@ -905,20 +919,23 @@ single_spec:
ensures:
| term
{ let id = mk_id "result" $startpos $endpos in
[mk_pat (Pvar id) $startpos $endpos, $1] }
let t = add_model_vc_post_label $1 in
[mk_pat (Pvar id) $startpos $endpos, t] }
raises:
| uqualid ARROW term
{ $1, mk_pat (Ptuple []) $startpos($1) $endpos($1), $3 }
{ let t = add_model_vc_post_label $3 in
$1, mk_pat (Ptuple []) $startpos($1) $endpos($1), t }
| uqualid pat_arg ARROW term
{ $1, $2, $4 }
{ let t = add_model_vc_post_label $4 in
$1, $2, t }
xsymbol:
| uqualid
{ $1, mk_pat Pwild $startpos $endpos, mk_term Ttrue $startpos $endpos }
invariant:
| INVARIANT LEFTBRC term RIGHTBRC { $3 }
| INVARIANT LEFTBRC term RIGHTBRC { add_model_vc_label $3 }
variant:
| VARIANT LEFTBRC comma_list1(single_variant) RIGHTBRC { $3 }
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment