Commit 4a62dea0 authored by Sylvain Dailler's avatar Sylvain Dailler

Automatically add model labels for ce generation

Changed the parser to automatically add model_trace labels during parsing.
Removed model labels in bench for counterexamples.
parent d80f0499
module M
use import ref.Ref
use import list.List
use import int.Int
type int_type = Integer int
goal G : forall x : int_type. match x with Integer y -> y > 0 end
let test_post (x : int) (y : ref int): unit
ensures { "model_vc_post" old !y >= x }
=
y := x - 1 + !y
end
ce/algebraic_type.mlw M G : Unknown (other)
ce/algebraic_type.mlw M WP_parameter test_post : Unknown (other)
Counter-example model:File algebraic_type.mlw:
Line 10:
x = {"type" : "Integer" , "val" : "1" }
y = {"type" : "Integer" ,
"val" : "0" }
Line 11:
old x = {"type" : "Integer" , "val" : "1" }
old y = {"type" : "Integer" ,
"val" : "0" }
Line 13:
y = {"type" : "Integer" ,
"val" : "0" }
ce/algebraic_type.mlw M G : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/algebraic_type.mlw M WP_parameter test_post : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/algebraic_type.mlw M G : Timeout
ce/algebraic_type.mlw M WP_parameter test_post : Timeout
......@@ -3,59 +3,59 @@ theory ModelInt
use import int.Int
(* PASS *)
goal test0 : forall x "model":int. not (0 < x < 1)
goal test0 : forall x:int. not (0 < x < 1)
(* CE *)
goal test1 : forall x "model":int. not (0 <= x <= 1)
goal test1 : forall x:int. not (0 <= x <= 1)
use import int.EuclideanDivision
(* CE *)
goal test2 : forall x "model":int. div x x = 1
goal test2 : forall x:int. div x x = 1
(* CE *)
goal test_overflow:
forall x "model" y "model" : int.
forall x y : int.
0 <= x <= 65535 /\ 0 <= y <= 65535 -> 0 <= x + y <= 65535
(* CE *)
goal test_overflow2:
forall x "model" y "model" : int.
forall x y : int.
-2 <= x <= 65535 /\ -2 <= y <= 65535 -> -2 <= x + y <= 65535
predicate is_int16 (x:int) = -65536 <= x <= 65535
(* CE *)
goal test_overflow_int16:
forall x "model" y "model" : int.
forall x y : int.
is_int16 x /\ is_int16 y -> is_int16 (x + y)
(* CE *)
goal test_overflow_int16_alt:
forall x "model" y "model" : int.
forall x y : int.
-65536 <= x <= 65535 /\ -65536 <= y <= 65535 -> -65536 <= x+y <= 65535
(* CE *)
goal test_overflow_int16_bis:
forall x "model" y "model" : int.
forall x y : int.
is_int16 x /\ is_int16 y /\
("model" 0 <= x) /\ (x <= y) -> is_int16 (x + y)
(0 <= x) /\ (x <= y) -> is_int16 (x + y)
predicate is_int32 (x:int) = -2147483648 <= x <= 2147483647
(* CE *)
goal test_overflow_int32:
forall x "model" y "model" : int.
forall x y : int.
is_int32 x /\ is_int32 y -> is_int32 (x + y)
(* CE *)
goal test_overflow_int32_bis:
forall x "model" y "model" : int.
forall x y : int.
is_int32 x /\ is_int32 y /\ 0 <= x <= y -> is_int32 (x + y)
(* CE *)
goal test_overflow_int32_bis_inline:
forall x "model" y "model" : int.
forall x y : int.
-2147483648 <= x <= 2147483647 /\ -2147483648 <= y <= 2147483647 /\ 0 <= x <= y -> -2147483648 <= x + y <= 2147483647
end
......@@ -3,21 +3,21 @@ theory T
use import int.Int
goal g0 : forall x "model":int. ("model" x >= 42) -> ("model" x + 3 <= 50)
goal g0 : forall x :int. (x >= 42) -> (x + 3 <= 50)
constant g : int
goal g1 : forall x "model":int. ("model" g >= x)
goal g1 : forall x:int. (g >= x)
goal g2 : forall x1 "model" "model_trace:X" x2 "model" x3 "model" x4 "model" x5 "model" x6 "model" x7 "model" x8 "model".
goal g2 : forall x1 "model" "model_trace:X" x2 x3 x4 x5 x6 x7 x8 .
("model" "model_trace: X1 + 1 = 2" x1 + 1 = 2) ->
("model" x2 + 1 = 2) ->
("model" x3 + 1 = 2) ->
("model" x4 + 1 = 2) ->
("model" x5 + 1 = 2) ->
("model" x6 + 1 = 2) ->
("model" x7 + 1 = 2) ->
("model" x8 + 1 = 2) ->
("model" x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
(x2 + 1 = 2) ->
(x3 + 1 = 2) ->
(x4 + 1 = 2) ->
(x5 + 1 = 2) ->
(x6 + 1 = 2) ->
(x7 + 1 = 2) ->
(x8 + 1 = 2) ->
(x1 + x2 + x3 + x4 + x5 + x6 + x7 + x8 = 2)
end
......@@ -7,9 +7,9 @@ module M
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
val y "model" "model_trace:y" :ref int
val y :ref int
let incr ( x23 "model" "model_trace:x23" : ref int ): unit
let incr ( x23 : ref int ): unit
ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
=
(*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
......@@ -17,7 +17,7 @@ module M
x23 := !x23 + 1;
x23 := !x23 + 1
let test_loop ( x "model" "model_trace:x" : ref int ): unit
let test_loop ( x : ref int ): unit
ensures { "model_vc_post" !x < old !x }
=
'L: incr x;
......
......@@ -2,8 +2,8 @@ theory ModelReal
use import real.Real
goal test1 : forall x "model":real. not (0.0 < x < 1.0)
goal test1 : forall x:real. not (0.0 < x < 1.0)
goal test2 : forall x "model":real. x/x=1.0
goal test2 : forall x:real. x/x=1.0
end
......@@ -24,7 +24,7 @@ module M
meta "inline : no" function projf_r_g
meta "model_projection" function projf_r_g
let record_match_eval_test1 (x "model" "model_trace:x" : r) : int
let record_match_eval_test1 (x : r) : int
ensures { "model_vc_post" result = 1 }
=
if x.g then
......@@ -37,12 +37,12 @@ module M
=
x.f
let record_match_eval_test3 (x "model" "model_trace:x" : ref r) : unit
let record_match_eval_test3 (x : ref r) : unit
ensures { !x.g }
=
x := { !x with f = 6}
let record_match_eval_test4 (x "model" "model_trace:x" : ref r) : r
let record_match_eval_test4 (x : ref r) : r
ensures { "model_vc_post" result.g }
=
x := { !x with f = 6 };
......@@ -50,7 +50,7 @@ module M
val re "model_projected" : ref r
let test_record_match_eval_test5 (x "model" "model_trace:x" : ref r) : r
let test_record_match_eval_test5 (x : ref r) : r
ensures { "model_vc_post" result = !re }
=
x := { !x with f = 6 };
......
......@@ -3,11 +3,7 @@ module M
use import list.List
use import int.Int
type int_type = Integer int
goal G : forall x "model" : int_type. match x with Integer y -> y > 0 end
let test_post (x "model" "model_trace:x" : int) (y "model" "model_trace:y" : ref int): unit
let test_post (x: int) (y : ref int): unit
ensures { "model_vc_post" old !y >= x }
=
y := x - 1 + !y
......@@ -15,9 +11,9 @@ module M
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
val y "model" "model_trace:y" :ref int
val y :ref int
let incr ( x23 "model" "model_trace:x23" : ref int ): unit
let incr ( x23: ref int ): unit
ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
=
(*#"random_path.random" 62 27 32#*)
......@@ -25,7 +21,7 @@ module M
x23 := !x23 + 1;
x23 := !x23 + 1
let test_loop ( x "model" "model_trace:x" : ref int ): unit
let test_loop ( x: ref int ): unit
ensures { "model_vc_post" !x < old !x }
=
'L: incr x;
......
ce/ref.mlw M G : Unknown (other)
ce/ref.mlw M WP_parameter test_post : Unknown (other)
Counter-example model:File ref.mlw:
Line 10:
Line 6:
x = {"type" : "Integer" , "val" : "1" }
y = {"type" : "Integer" ,
"val" : "0" }
Line 11:
Line 7:
old x = {"type" : "Integer" , "val" : "1" }
old y = {"type" : "Integer" ,
"val" : "0" }
Line 13:
Line 9:
y = {"type" : "Integer" ,
"val" : "0" }
ce/ref.mlw M WP_parameter incr : Unknown (other)
Counter-example model:File ref.mlw:
Line 18:
Line 14:
y = {"type" : "Integer" , "val" : "-2" }
Line 20:
Line 16:
x23 = {"type" : "Integer" , "val" : "0" }
Line 21:
Line 17:
x23 = {"type" : "Integer" , "val" : "2" }
old x23 = {"type" : "Integer" ,
"val" : "0" }
y = {"type" : "Integer" ,
"val" : "-1" }
Line 24:
Line 20:
y = {"type" : "Integer" , "val" : "-1" }
Line 25:
Line 21:
x23 = {"type" : "Integer" , "val" : "1" }
Line 26:
Line 22:
x23 = {"type" : "Integer" ,
"val" : "2" }
ce/ref.mlw M WP_parameter test_loop : Unknown (other)
Counter-example model:File ref.mlw:
Line 28:
Line 24:
x = {"type" : "Integer" , "val" : "0" }
Line 29:
Line 25:
x = {"type" : "Integer" , "val" : "0" }
old x = {"type" : "Integer" ,
"val" : "0" }
Line 31:
Line 27:
x = {"type" : "Integer" , "val" : "-1" }
y = {"type" : "Integer" ,
"val" : "-3" }
Line 32:
Line 28:
x = {"type" : "Integer" , "val" : "0" }
Line 33:
Line 29:
x = {"type" : "Integer" , "val" : "0" }
x = {"type" : "Integer" ,
"val" : "-1" }
......
ce/ref.mlw M G : HighFailure
Prover exit status: exited with status 1
Prover output:
ce/ref.mlw M WP_parameter test_post : HighFailure
Prover exit status: exited with status 1
Prover output:
......
ce/ref.mlw M G : Timeout
ce/ref.mlw M WP_parameter test_post : Timeout
ce/ref.mlw M WP_parameter incr : Timeout
ce/ref.mlw M WP_parameter test_loop : Timeout
......@@ -2,7 +2,7 @@ theory ModelArray
use import map.Map
goal t1 : forall t "model" :map int int, i "model" : int.
goal t1 : forall t :map int int, i: int.
get (set t 0 42) i = get t i
end
......@@ -5,9 +5,9 @@ module M
type int_type = Integer int
goal G : forall x "model" : int_type. match x with Integer y -> y > 0 end
goal G : forall x : int_type. match x with Integer y -> y > 0 end
let test_post (x "model" "model_trace:x" : int) (y "model" "model_trace:y" : ref int): unit
let test_post (x : int) (y : ref int): unit
ensures { "model_vc_post" old !y >= x }
=
y := x - 1 + !y
......@@ -15,9 +15,9 @@ module M
(**********************************************************
** Getting counterexamples for terms of primitive types **
**********************************************************)
val y "model" "model_trace:y" :ref int
val y :ref int
let incr ( x23 "model" "model_trace:x23" : ref int ): unit
let incr ( x23 : ref int ): unit
ensures { "model_vc_post" !x23 = old !x23 + 2 + !y }
=
(*#"/home/cmarche/recherche/why/tests/c/binary_search.c" 62 27 32#*)
......@@ -25,7 +25,7 @@ module M
x23 := !x23 + 1;
x23 := !x23 + 1
let test_loop ( x "model" "model_trace:x" : ref int ): unit
let test_loop ( x : ref int ): unit
ensures { "model_vc_post" !x < old !x }
=
'L: incr x;
......@@ -39,18 +39,18 @@ module M
** Getting counterexamples for maps **
**************************************)
use import map.Map
let test_map (x "model" : ref (map int int)) : unit
let test_map (x : ref (map int int)) : unit
ensures { "model_vc" !x[0] <> !x[1] }
=
x := Map.set !x 0 3
(* Multi-dimensional maps *)
let test_map_multidim1 (x "model" : ref (map int (map int int))) : unit
let test_map_multidim1 (x : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }
=
x := Map.set !x 0 (Map.get !x 1)
let test_map_multidim2 (x "model" : ref (map int (map int int))) : unit
let test_map_multidim2 (x : ref (map int (map int int))) : unit
ensures { "model_vc" !x[0][0] <> !x[1][1] }
=
let x0 = Map.get !x 0 in
......@@ -78,7 +78,7 @@ module M
meta "inline : no" function projf_r_g
meta "model_projection" function projf_r_g
let record_match_eval_test1 (x "model" "model_trace:x" : r) : int
let record_match_eval_test1 (x : r) : int
ensures { "model_vc_post" result = 1 }
=
if x.g then
......@@ -91,12 +91,12 @@ module M
=
x.f
let record_match_eval_test3 (x "model" "model_trace:x" : ref r) : unit
let record_match_eval_test3 (x : ref r) : unit
ensures { !x.g }
=
x := { !x with f = 6}
let record_match_eval_test4 (x "model" "model_trace:x" : ref r) : r
let record_match_eval_test4 (x : ref r) : r
ensures { "model_vc_post" result.g }
=
x := { !x with f = 6 };
......@@ -104,7 +104,7 @@ module M
val re "model_projected" : ref r
let test_record_match_eval_test5 (x "model" "model_trace:x" : ref r) : r
let test_record_match_eval_test5 (x : ref r) : r
ensures { "model_vc_post" result = !re }
=
x := { !x with f = 6 };
......
......@@ -2,43 +2,80 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.5-prerelease" alternative="alt" timelimit="5" memlimit="1000"/>
<prover id="0" name="CVC4" version="1.5-prerelease" alternative="alt" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.5" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../cvc4-models.mlw">
<theory name="M">
<goal name="G">
</goal>
<goal name="WP_parameter test_post" expl="VC for test_post">
</goal>
<goal name="WP_parameter incr" expl="VC for incr">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00" steps="896"/></proof>
<transf name="split_goal_wp">
<goal name="WP_parameter incr.1" expl="1. postcondition">
<transf name="split_goal_wp" >
<goal name="WP_parameter incr.0" expl="postcondition">
</goal>
</transf>
</goal>
<goal name="WP_parameter test_loop" expl="VC for test_loop">
<transf name="split_goal_wp">
<goal name="WP_parameter test_loop.1" expl="1. loop invariant init">
<proof prover="0"><result status="unknown" time="0.00" steps="813"/></proof>
<transf name="split_goal_wp" >
<goal name="WP_parameter test_loop.0" expl="loop invariant init">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00" steps="813"/></proof>
</goal>
<goal name="WP_parameter test_loop.1" expl="loop invariant preservation">
<proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="866"/></proof>
</goal>
<goal name="WP_parameter test_loop.2" expl="2. loop invariant preservation">
<proof prover="0"><result status="valid" time="0.01" steps="866"/></proof>
<goal name="WP_parameter test_loop.2" expl="loop variant decrease">
<proof prover="0" obsolete="true"><result status="unknown" time="0.00" steps="916"/></proof>
</goal>
<goal name="WP_parameter test_loop.3" expl="3. postcondition">
<proof prover="0"><result status="unknown" time="0.00" steps="916"/></proof>
<goal name="WP_parameter test_loop.3" expl="postcondition">
</goal>
</transf>
</goal>
<goal name="WP_parameter test_map" expl="VC for test_map">
</goal>
<goal name="WP_parameter test_map_multidim1" expl="VC for test_map_multidim1">
</goal>
<goal name="WP_parameter test_map_multidim2" expl="VC for test_map_multidim2">
</goal>
<goal name="WP_parameter record_match_eval_test1" expl="VC for record_match_eval_test1">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="WP_parameter record_match_eval_test2" expl="VC for record_match_eval_test2">
</goal>
<goal name="WP_parameter record_match_eval_test3" expl="VC for record_match_eval_test3">
</goal>
<goal name="WP_parameter record_match_eval_test4" expl="VC for record_match_eval_test4">
</goal>
<goal name="WP_parameter test_record_match_eval_test5" expl="VC for test_record_match_eval_test5">
</goal>
<goal name="WP_parameter map_record_proj_test1" expl="VC for map_record_proj_test1">
</goal>
<goal name="WP_parameter record_map_proj_test2" expl="VC for record_map_proj_test2">
</goal>
<goal name="WP_parameter record_map_proj_test3" expl="VC for record_map_proj_test3">
</goal>
<goal name="WP_parameter proj_map_test1" expl="VC for proj_map_test1">
</goal>
<goal name="WP_parameter proj_map_test2" expl="VC for proj_map_test2">
</goal>
<goal name="WP_parameter proj_test" expl="VC for proj_test">
</goal>
</theory>
</file>
<file name="../cvc4-models.why">
<theory name="T">
<goal name="g_binop">
</goal>
<goal name="g_no_lab">
<proof prover="1"><result status="unknown" time="0.00"/></proof>
</goal>
<goal name="g_lab0">
</goal>
<goal name="g2_lab">
</goal>
<goal name="newgoal">
<proof prover="0"><result status="unknown" time="0.00" steps="549"/></proof>
<proof prover="0" obsolete="true"><result status="unknown" time="0.00" steps="549"/></proof>
</goal>
<goal name="g_binop">
</goal>
</theory>
<theory name="ModelInt">
......
......@@ -36,21 +36,18 @@ end
let floc s e = Loc.extract (s,e)
let model_label = Ident.create_label "model"
let model_projected = Ident.create_label "model_projected"
(* let model_projected = Ident.create_label "model_projected"*)
(*
let is_model_label l =
match l with
| Lpos _ -> false
| Lstr lab ->
(lab = model_label) || (lab = model_projected)
let model_lab_present labels =
try
ignore(List.find is_model_label labels);
true
with Not_found ->
false
List.exists is_model_label labels
*)
let model_trace_regexp = Str.regexp "model_trace:"
......@@ -64,22 +61,26 @@ end
with Not_found -> false
let model_trace_lab_present labels =
try
ignore(List.find is_model_trace_label labels);
true
with Not_found ->
false
let add_model_trace name labels =
if (model_lab_present labels) && (not (model_trace_lab_present labels)) then
(Lstr (Ident.create_label ("model_trace:" ^ name)))::labels
List.exists is_model_trace_label labels
let add_model_trace id =
if model_trace_lab_present id.id_lab then
id
else
labels
let l =
(Lstr (Ident.create_label ("model_trace:" ^ id.id_str)))
::(Lstr model_label) :: id.id_lab in
{ id with id_lab = l }
let add_lab id l =
let l = add_model_trace id.id_str l in
{ id with id_lab = l }
let add_model_labels (b : binder) =
match b with
| (loc, Some id, ghost, ty) ->
(loc, Some (add_model_trace id), ghost, ty)
| _ -> b
let id_anonymous loc = { id_str = "_"; id_lab = []; id_loc = loc }
let mk_int_const neg lit =
......@@ -483,7 +484,7 @@ binder:
{ match $1 with
| PTtyapp (Qident id, [])
| PTparen (PTtyapp (Qident id, [])) ->
[floc $startpos $endpos, Some id, false, None]
[floc $startpos $endpos, Some id, false, None]
| _ -> [floc $startpos $endpos, None, false, Some $1] }
| LEFTPAR GHOST ty RIGHTPAR
{ match $3 with
......@@ -584,7 +585,8 @@ term_:
| MATCH comma_list2(term) WITH match_cases(term) END
{ Tmatch (mk_term (Ttuple $2) $startpos($2) $endpos($2), $4) }
| quant comma_list1(quant_vars) triggers DOT term
{ Tquant ($1, List.concat $2, $3, $5) }
{ let l = List.map add_model_labels (List.concat $2) in
Tquant ($1, l, $3, $5) }
| EPSILON
{ Loc.errorm "Epsilon terms are currently not supported in WhyML" }
| label term %prec prec_named
......@@ -658,11 +660,11 @@ quant:
numeral:
| INTEGER { Number.ConstInt (mk_int_const false $1) }
| REAL { Number.ConstReal (mk_real_const false $1) }
(* Program declarations *)
pdecl:
| VAL top_ghost labels(lident_rich) type_v { Dval ($3, $2, $4) }
| VAL top_ghost labels(lident_rich) type_v { Dval (add_model_trace $3, $2, $4) }
| LET top_ghost labels(lident_rich) fun_defn { Dfun ($3, $2, $4) }
| LET top_ghost labels(lident_rich) EQUAL fun_expr { Dfun ($3, $2, $5) }
| LET REC with_list1(rec_defn) { Drec $3 }
......@@ -697,7 +699,8 @@ rec_defn:
{ $2, $1, ($3, $4, $8, spec_union $5 $7) }
fun_defn:
| binders cast? spec EQUAL spec seq_expr { ($1, $2, $6, spec_union $3 $5) }
| binders cast? spec EQUAL spec seq_expr {
(List.map add_model_labels $1, $2, $6, spec_union $3 $5) }
fun_expr:
| FUN binders spec ARROW spec seq_expr { ($2, None, $6, spec_union $3 $5) }
......
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