Commit b6b769e2 authored by MARCHE Claude's avatar MARCHE Claude

basic support for invariants

parent 4fcd288f
......@@ -46,17 +46,13 @@ type cfg_instr = {
and cfg_instr_desc =
| CFGgoto of label
(** goto a label "goto L" *)
(** goto a label "goto L" *)
| CFGswitch of Ptree.expr * switch_branch list
(** pattern-matching *)
(** pattern-matching *)
| CFGinvariant of ident * Ptree.term
(** named invariant *)
| CFGexpr of Ptree.expr
(*
| CFGassign of ident * cfg_expr
(** assignment "x <- e" *)
| CFGassert of Expr.assertion_kind * Ptree.term
(** assert or assume or check *)
(* TODO: expand -> branching, procedure call... or any Ptree.expr ! *)
*)
(** any other regular WhyML expressions *)
and switch_branch = Ptree.pattern * block
(** pattern -> regular WhyML expression ; goto ident *)
......
......@@ -366,46 +366,44 @@ let translate_instr e =
*)
| CFGgoto _id -> mk_expr ~loc (Etuple [])
| CFGswitch _ -> mk_expr ~loc (Etuple [])
| CFGinvariant (id,t) ->
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ id.id_str)) in
let t = { t with term_desc = Tattr(attr,t) } in
mk_expr ~loc (Eassert(Expr.Assert,t))
| CFGexpr e -> e
let build_return_function retty pat spec (startlabel, e, revbody) acc =
let body =
List.fold_left
(fun acc e -> mk_expr ~loc:e.expr_loc (Esequence (e, acc)))
e revbody
in
let f =
Efun([], Some retty, pat, Ity.MaskVisible, spec, body)
in
let loc = Loc.dummy_position in
let id = mk_id ~loc ("_" ^ startlabel ^ "_to_return") in
mk_expr ~loc (Elet (id,false,Expr.RKnone, mk_expr ~loc f, acc))
let translate_cfg block blocks =
let translate_cfg preconds block blocks =
let blocks =
List.fold_left
(fun acc (l,b) -> Wstdlib.Mstr.add l.id_str b acc)
Wstdlib.Mstr.empty
blocks
in
let rec traverse startlabel bl acc =
let visited = ref [] in
let rec traverse startlabel preconds bl acc (funs,ret_funs) =
match bl with
| [] -> assert false
| { cfg_instr_desc = 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
in
traverse startlabel bl acc
| { cfg_instr_desc = CFGswitch _} :: _ ->
failwith "switch not suported yet"
| [{ cfg_instr_desc = CFGexpr e}] ->
(startlabel, e, acc)
| { cfg_instr_desc = CFGexpr e} :: rem ->
traverse startlabel rem (e::acc)
| i :: rem ->
match i.cfg_instr_desc 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
in
traverse startlabel preconds bl acc (funs,ret_funs)
| CFGinvariant(id,t) ->
let funs = (startlabel, preconds, id, t, acc) :: funs in
traverse id.id_str [t] rem [] (funs,ret_funs)
| CFGswitch _ ->
failwith "switch not suported yet"
| CFGexpr e when rem=[] ->
let ret_funs = (startlabel, e, acc) :: ret_funs in
(funs, ret_funs)
| CFGexpr e ->
traverse startlabel preconds rem (e::acc) (funs,ret_funs)
in
traverse "start" block []
traverse "start" preconds block [] ([],[])
let e_ref = mk_expr ~loc:Loc.dummy_position Eref
......@@ -419,17 +417,61 @@ let declare_local (loc,idopt,ghost,tyopt) body =
mk_expr ~loc:id.id_loc (Elet(id,ghost,Expr.RKnone,e,body))
| _ -> failwith "invalid variable declaration"
let build_path_function (startlabel, preconds, id , t, revbody) acc =
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_expr ~loc:id.id_loc (Eassert(Expr.Assert,t)) in
let body =
List.fold_left
(fun acc e -> mk_expr ~loc:e.expr_loc (Esequence (e, acc)))
e revbody
in
let body =
List.fold_left
(fun acc t ->
let e = mk_expr ~loc:t.term_loc (Eassert(Expr.Assume,t)) in
mk_expr ~loc:acc.expr_loc (Esequence (e, acc)))
body preconds
in
let f =
Efun([], None, pat_wild ~loc:Loc.dummy_position, Ity.MaskVisible, empty_spec, body)
in
let loc = Loc.dummy_position in
let id = mk_id ~loc ("_" ^ startlabel ^ "_to_" ^ id.id_str) in
mk_expr ~loc (Elet (id,false,Expr.RKnone, mk_expr ~loc f, acc))
let build_return_function retty pat spec (startlabel, e, revbody) acc =
let body =
List.fold_left
(fun acc e -> mk_expr ~loc:e.expr_loc (Esequence (e, acc)))
e revbody
in
let f =
Efun([], Some retty, pat, Ity.MaskVisible, spec, body)
in
let loc = Loc.dummy_position in
let id = mk_id ~loc ("_" ^ startlabel ^ "_to_return") in
mk_expr ~loc (Elet (id,false,Expr.RKnone, mk_expr ~loc f, acc))
let translate_letcfg (id,args,retty,pat,spec,locals,block,blocks) =
Debug.dprintf debug "translating cfg function `%s`@." id.id_str;
Debug.dprintf debug "return type is `%a`@." pp_pty retty;
let fun_returning = translate_cfg block blocks in
let (funs,ret_funs) = translate_cfg spec.sp_pre block blocks in
let loc = Loc.dummy_position in
let body = Eany([],Expr.RKnone,Some retty,pat,Ity.MaskVisible,spec) in
let body =
build_return_function retty pat spec fun_returning
List.fold_right (build_return_function retty pat spec) ret_funs
(mk_expr ~loc body)
in
let body = List.fold_right declare_local locals body in
let body =
List.fold_right build_path_function funs body
in
let body =
List.fold_right declare_local locals body
in
let f =
Efun(args, Some retty, pat, Ity.MaskVisible, spec, body)
in
......
......@@ -83,6 +83,9 @@ instr:
{ mk_cfginstr (CFGexpr $1) $startpos $endpos }
| SWITCH contract_expr cases END
{ mk_cfginstr (CFGswitch ($2,$3)) $startpos $endpos }
| INVARIANT ident LEFTBRC term RIGHTBRC
{ mk_cfginstr (CFGinvariant($2,$4)) $startpos $endpos }
(*
| lident LARROW cfgexpr
{ mk_cfginstr (CFGassign ($1,$3)) $startpos $endpos }
......
......@@ -26,6 +26,26 @@ let cfg cfggoto (x:int) : int
y
}
let main () = cfgassert 42; cfggoto 43
let cfg cfg_inv (x:int) : int
requires { x >= 0 }
ensures { result >= 2 }
=
var (y:int);
{
y <- x;
invariant I { y >= 0} ;
y <- y + 1;
invariant J { y >= 1} ;
y <- y + 1;
y
}
let main () =
cfgassert 42;
let _ = cfggoto 43 in
cfg_inv 44
end
\ No newline at end of file
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