Commit 6af319ea authored by MARCHE Claude's avatar MARCHE Claude

group consecutive invariants together

parent 019647ce
......@@ -42,6 +42,7 @@ why3.conf
/why3regtests.out
/src/jessie/.merlin
/_build
/public
# /bench/
/bench/programs/good/booleans/
......@@ -231,6 +232,12 @@ pvsbin/
/plugins/microc/test/
/plugins/microc/mc_parser.conflicts
# /plugins/cfg/
/plugins/cfg/cfg_lexer.ml
/plugins/cfg/cfg_parser.ml
/plugins/cfg/cfg_parser.mli
/plugins/cfg/cfg_parser.conflicts
# /drivers
/drivers/coq-realizations.aux
/drivers/pvs-realizations.aux
......@@ -249,6 +256,7 @@ pvsbin/
/tests/microc/*/why3shapes.gz
# /examples/
/examples/use_api/results
/examples/in_progress/course/
/examples/in_progress/wcet_hull/
/examples/in_progress/binary_search2/
......
......@@ -366,7 +366,7 @@ The extension of syntax is formally described by the following rules.
file: `module`*
module: "module" `ident` `decl`* "end"
decl: "let" "cfg" `cfg_fundef` ("with" `cfg_fundef`)*
cfg_fundef: `ident` `binders` : `type` `spec` "=" `vardecl`* "{" `block` "}" `labelblock`*
cfg_fundef: `ident` `binder`+ : `type` `spec` "=" `vardecl`* "{" `block` "}" `labelblock`*
vardecl: "var" `ident`* ":" `type` ";" | "ghost" "var" `ident`* ":" `type` ";"
block: `instruction` (";" `instruction`)*
labelblock: `ident` "{" `block` "}"
......@@ -428,10 +428,11 @@ to node X, label L1 to node 'inv', label L2 to node YY.
goto L1
}
L1 {
invariant I { 0 <= i < a.length /\
0 <= ind < a.length /\
m = a[ind] /\
forall j. 0 <= j <= i -> a[ind] >= a[j] };
invariant i_bounds { 0 <= i < a.length };
invariant ind_bounds { 0 <= ind < a.length };
invariant m_and_ind { m = a[ind] };
invariant m_is_max { forall j. 0 <= j <= i -> m >= a[j] };
(* (yes, j <= i, not j < i !) *)
i <- i+1;
switch (i < a.length)
| True -> goto L2
......@@ -455,4 +456,5 @@ Limitations
- New keywords "cfg", "goto", "switch" and "var" cannot be used as regular identifiers anymore
- consecutive invariants are not seen as a conjunction of invariants
- Trailing code after "switch" is not supported: switch branches must
return a value or end with a goto
......@@ -25,8 +25,8 @@ and cfg_instr_desc =
(** goto a label "goto L" *)
| CFGswitch of Ptree.expr * switch_branch list
(** pattern-matching *)
| CFGinvariant of ident * Ptree.term
(** named invariant *)
| CFGinvariant of (ident * Ptree.term) list
(** named invariants *)
| CFGexpr of Ptree.expr
(** any other regular WhyML expressions *)
......
......@@ -84,6 +84,12 @@ let rec pp_pty fmt t =
let divergent_attr = ATstr (Ident.create_attribute "vc:divergent")
exception CFGError of string
let () = Exn_printer.register (fun fmt exn -> match exn with
| CFGError msg -> Format.fprintf fmt "CFG translation error: %s" msg
| _ -> raise exn)
let translate_cfg preconds block blocks =
let blocks =
List.fold_left
......@@ -99,29 +105,46 @@ let translate_cfg preconds block blocks =
| [] -> mk_unit ~loc:Loc.dummy_position
| i :: rem ->
let loc = i.cfg_instr_loc in
match i.cfg_instr_desc with
| CFGgoto l ->
match i.cfg_instr_desc, rem with
| CFGgoto l, [] ->
let bl =
try
Wstdlib.Mstr.find l.id_str blocks
with Not_found -> Format.eprintf "Label %a not found for goto@." pp_id l; exit 1
with Not_found ->
raise (Loc.Located(l.id_loc,CFGError ("Label " ^ l.id_str ^ " not found for goto")))
in
traverse_block bl
| CFGinvariant(id,t) ->
(* TODO: if next instruction is also an invariant, groupe them together *)
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ id.id_str)) in
(* TODO : add also an "expl:" *)
let t = { t with term_desc = Tattr(attr,t) } in
let e = mk_check ~loc t in
let k = mk_expr ~loc (Eidapp(Qident (mk_id ~loc ("_from_" ^ id.id_str)),[mk_unit ~loc])) in
let e = mk_seq ~loc e k in
| CFGgoto _,_ -> raise (Loc.Located(loc,CFGError "Unreachable code after goto"))
| CFGinvariant l1, { cfg_instr_desc = CFGinvariant l2 } :: rem ->
traverse_block ({ i with cfg_instr_desc = CFGinvariant (l1 @ l2)}:: rem)
| CFGinvariant l, _ ->
let id =
match l with
| [] -> assert false
| (id,_)::_ -> id
in
let l = List.map
(fun (id,t) ->
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ id.id_str)) in
(* TODO : add also an "expl:" *)
{ t with term_desc = Tattr(attr,t) })
l
in
if not (List.mem id.id_str !visited) then
begin
visited := id.id_str :: !visited;
traverse_from_entry_point id.id_str [t] rem
traverse_from_entry_point id.id_str l rem
end;
e
| CFGswitch(e,cases) ->
let k =
mk_expr ~loc (Eidapp(Qident (mk_id ~loc ("_from_" ^ id.id_str)),[mk_unit ~loc]))
in
List.fold_right
(fun t acc ->
let e = mk_check ~loc:t.term_loc t in
mk_seq ~loc e acc)
l
k
| CFGswitch(e,cases), [] ->
let branches =
List.map
(fun (pat,bl) ->
......@@ -130,8 +153,10 @@ let translate_cfg preconds block blocks =
cases
in
mk_expr ~loc (Ematch(e,branches,[]))
| CFGexpr e when rem=[] -> e
| CFGexpr e1 ->
| CFGswitch _,_ ->
raise (Loc.Located(loc,CFGError "unsupported: trailing code after switch"))
| CFGexpr e, [] -> e
| CFGexpr e1,_ ->
let e2 = traverse_block rem in
mk_seq ~loc e1 e2
......
......@@ -85,15 +85,7 @@ instr:
| SWITCH LEFTPAR contract_expr RIGHTPAR cases END
{ mk_cfginstr (CFGswitch ($3,$5)) $startpos $endpos }
| INVARIANT ident LEFTBRC term RIGHTBRC
{ mk_cfginstr (CFGinvariant($2,$4)) $startpos $endpos }
(*
| lident LARROW cfgexpr
{ mk_cfginstr (CFGassign ($1,$3)) $startpos $endpos }
| k=assertion_kind id=option(ident_nq) LEFTBRC t=term RIGHTBRC
{ let (n,k)=k in
mk_cfginstr (CFGassert(k, name_term id n t)) $startpos $endpos }
*)
{ mk_cfginstr (CFGinvariant [$2,$4]) $startpos $endpos }
;
cases:
......@@ -102,14 +94,3 @@ cases:
| BAR match_case(sequence) cases
{ $2 :: $3 }
;
(*
cfgexpr:
| TRUE
{ mk_cfgexpr CFGtrue $startpos $endpos }
| FALSE
{ mk_cfgexpr CFGfalse $startpos $endpos }
| numeral
{ mk_cfgexpr (CFGconst $1) $startpos $endpos }
;
*)
......@@ -37,11 +37,11 @@ module MaxArray
goto L1
}
L1 {
invariant I { 0 <= i < a.length /\
0 <= ind < a.length /\
m = a[ind] /\
forall j. 0 <= j <= i -> a[ind] >= a[j] };
(* (yes, j <= i, not j < i !) *)
invariant i_bounds { 0 <= i < a.length };
invariant ind_bounds { 0 <= ind < a.length };
invariant m_and_ind { m = a[ind] };
invariant m_is_max { forall j. 0 <= j <= i -> m >= a[j] };
(* (yes, j <= i, not j < i !) *)
i <- i+1;
switch (i < a.length)
| True -> goto L2
......
......@@ -12,33 +12,60 @@
<proof prover="2"><result status="valid" time="0.03" steps="2638"/></proof>
</goal>
<goal name="compute_max&#39;vc.1" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3086"/></proof>
<proof prover="2"><result status="valid" time="0.03" steps="2702"/></proof>
</goal>
<goal name="compute_max&#39;vc.2" expl="postcondition" proved="true">
<goal name="compute_max&#39;vc.2" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="2702"/></proof>
</goal>
<goal name="compute_max&#39;vc.3" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2320"/></proof>
</goal>
<goal name="compute_max&#39;vc.4" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2653"/></proof>
</goal>
<goal name="compute_max&#39;vc.5" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3038"/></proof>
</goal>
<goal name="compute_max&#39;vc.3" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3001"/></proof>
<goal name="compute_max&#39;vc.6" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3018"/></proof>
</goal>
<goal name="compute_max&#39;vc.7" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3061"/></proof>
</goal>
<goal name="compute_max&#39;vc.8" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3097"/></proof>
</goal>
<goal name="compute_max&#39;vc.9" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3098"/></proof>
</goal>
<goal name="compute_max&#39;vc.10" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="2549"/></proof>
</goal>
<goal name="compute_max&#39;vc.11" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3448"/></proof>
</goal>
<goal name="compute_max&#39;vc.12" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3692"/></proof>
</goal>
<goal name="compute_max&#39;vc.4" expl="index in array bounds" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3044"/></proof>
<goal name="compute_max&#39;vc.13" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3072"/></proof>
</goal>
<goal name="compute_max&#39;vc.5" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3758"/></proof>
<goal name="compute_max&#39;vc.14" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="2611"/></proof>
</goal>
<goal name="compute_max&#39;vc.6" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.04" steps="3643"/></proof>
<goal name="compute_max&#39;vc.15" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2482"/></proof>
</goal>
<goal name="compute_max&#39;vc.7" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3654"/></proof>
<goal name="compute_max&#39;vc.16" expl="check" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3386"/></proof>
</goal>
<goal name="compute_max&#39;vc.8" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3596"/></proof>
<goal name="compute_max&#39;vc.17" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3648"/></proof>
</goal>
<goal name="compute_max&#39;vc.9" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="3237"/></proof>
<goal name="compute_max&#39;vc.18" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="3273"/></proof>
</goal>
<goal name="compute_max&#39;vc.10" expl="postcondition" proved="true">
<goal name="compute_max&#39;vc.19" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02" steps="2965"/></proof>
</goal>
</transf>
......
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