Commit d3d2595d authored by Andrei Paskevich's avatar Andrei Paskevich

Vc: Eassign (to be cont.)

parent b939cb83
......@@ -272,13 +272,6 @@ let ity_affected wr ity = Util.any ity_rch_fold (Mreg.contains wr) ity
let pv_affected wr v = ity_affected wr v.pv_ity
let rec reg_aff_regs wr s reg =
let q = reg_exp_fold (reg_aff_regs wr) Sreg.empty reg in
let affect = not (Sreg.is_empty q) || Mreg.mem reg wr in
Sreg.union s (if affect then Sreg.add reg q else q)
let ity_aff_regs wr s ity = ity_exp_fold (reg_aff_regs wr) s ity
(* a "destination map" maps program variables (pre-effect state)
to fresh vsymbols (post-effect state) *)
......@@ -382,7 +375,14 @@ and explore_its kn aff regs t s tl rl =
List.fold_left follow regs (find_its_defn kn s).itd_fields
let name_regions kn wr dst =
let collect o _ aff = ity_aff_regs wr aff o.pv_ity in
(* for every write collect the regions affected by it or
reachable from it (needed for multi-staged assignment) *)
let rec regs_to_name s r =
let q = if Mreg.mem r wr
then reg_rch_fold Sreg.add_left Sreg.empty r
else reg_exp_fold regs_to_name Sreg.empty r in
if Sreg.is_empty q then s else Sreg.union s (Sreg.add r q) in
let collect o _ aff = ity_exp_fold regs_to_name aff o.pv_ity in
let aff = Mpv.fold collect dst Sreg.empty in
let fill o n regs = explore_paths kn aff regs (t_var n) o.pv_ity in
let regs = Mpv.fold fill dst Mreg.empty in
......@@ -396,23 +396,12 @@ let name_regions kn wr dst =
let cons_t_simp nt t fl =
if t_equal nt t then fl else t_equ nt t :: fl
let rec havoc kn wr regs t ity fl =
let rec havoc kn reg_havoc wr regs t ity fl =
if not (ity_affected wr ity) then t, fl else
match ity.ity_node with
| Ityvar _ -> assert false
| Ityreg ({reg_its = s} as r) when s.its_nonfree || Mreg.mem r wr ->
let itd = find_its_defn kn s in
let isb = its_match_regs s r.reg_args r.reg_regs in
let wfs = Mreg.find_def Mpv.empty r wr in
let nt = Mreg.find r regs in
let field rs fl =
if Mpv.mem (Opt.get rs.rs_field) wfs then fl else
let ity = ity_full_inst isb rs.rs_cty.cty_result in
let ls = ls_of_rs rs and ty = Some (ty_of_ity ity) in
let t = t_app ls [t] ty and nt = t_app ls [nt] ty in
let t, fl = havoc kn wr regs t ity fl in
cons_t_simp nt t fl in
nt, List.fold_right field itd.itd_fields fl
reg_havoc kn wr regs t r fl
| Ityreg {reg_its = s; reg_args = tl; reg_regs = rl}
| Ityapp (s,tl,rl) ->
let itd = find_its_defn kn s in
......@@ -423,7 +412,7 @@ let rec havoc kn wr regs t ity fl =
let field rs (tl, fl) =
let ity = ity_full_inst isb rs.rs_cty.cty_result in
let t = t_app_infer (ls_of_rs rs) [t] in
let t, fl = havoc kn wr regs t ity fl in
let t, fl = havoc kn reg_havoc wr regs t ity fl in
t::tl, fl in
let tl, fl = List.fold_right field itd.itd_fields ([],fl) in
let t0 = match tl with
......@@ -445,7 +434,7 @@ let rec havoc kn wr regs t ity fl =
let vl = List.map2 get_pjv cty.cty_args ityl in
let p = pat_app cs (List.map pat_var vl) ty in
let field v ity (tl, fl) =
let t, fl = havoc kn wr regs (t_var v) ity fl in
let t, fl = havoc kn reg_havoc wr regs (t_var v) ity fl in
t::tl, fl in
let tl, fl = List.fold_right2 field vl ityl ([],[]) in
(p, fs_app cs tl ty), (p, t_and_l fl) in
......@@ -454,6 +443,51 @@ let rec havoc kn wr regs t ity fl =
t, begin match f.t_node with Ttrue -> fl | _ -> f::fl end
end
let rec havoc_effect kn wr regs t ({reg_its = s} as r) fl =
let itd = find_its_defn kn s in
let isb = its_match_regs s r.reg_args r.reg_regs in
let wfs = Mreg.find_def Spv.empty r wr in
let nt = Mreg.find r regs in
let field rs fl =
if Spv.mem (Opt.get rs.rs_field) wfs then fl else
let ity = ity_full_inst isb rs.rs_cty.cty_result in
let ls = ls_of_rs rs and ty = Some (ty_of_ity ity) in
let t = t_app ls [t] ty and nt = t_app ls [nt] ty in
let t, fl = havoc kn havoc_effect wr regs t ity fl in
cons_t_simp nt t fl in
nt, List.fold_right field itd.itd_fields fl
let rec havoc_assign kn wr regs t ({reg_its = s} as r) fl =
let itd = find_its_defn kn s in
let isb = its_match_regs s r.reg_args r.reg_regs in
let wfs = Mreg.find_def Mrs.empty r wr in
let nt = Mreg.find r regs in
let field rs fl =
let ity = ity_full_inst isb rs.rs_cty.cty_result in
let ls = ls_of_rs rs and ty = Some (ty_of_ity ity) in
let t = t_app ls [t] ty and nt = t_app ls [nt] ty in
let t, fl = match Mrs.find_opt rs wfs with
| Some v ->
let lrl = ity_rch_fold (fun l r -> r::l) [] ity in
let rrl = ity_rch_fold (fun l r -> r::l) [] v.pv_ity in
(* we start from a surviving variable, so lrl <-> rrl *)
let update rg l r = Mreg.add r (Mreg.find l regs) rg in
let regs = List.fold_left2 update Mreg.empty lrl rrl in
havoc kn havoc_assign wr regs (t_var v.pv_vs) v.pv_ity fl
| None ->
havoc kn havoc_assign wr regs t ity fl in
cons_t_simp nt t fl in
nt, List.fold_right field itd.itd_fields fl
let writes_of_assign asl =
let add wr (r,f,v) =
let r = match r.pv_ity.ity_node with
| Ityreg r -> r | _ -> assert false in
Mreg.change (function
| None -> Some (Mrs.singleton f v)
| Some s -> Some (Mrs.add f v s)) r wr in
List.fold_left add Mreg.empty asl
let print_dst dst = if Debug.test_flag debug then
Format.printf "@[vars = %a@]@." (Pp.print_list Pp.space
(fun fmt (o,n) -> Format.fprintf fmt "(%a -> %a)"
......@@ -464,7 +498,7 @@ let print_regs regs = if Debug.test_flag debug then
(fun fmt (r,t) -> Format.fprintf fmt "(%a -> %a)"
Ity.print_reg r Pretty.print_term t)) (Mreg.bindings regs)
let wp_havoc {known_map = kn} {eff_writes = wr; eff_covers = cv} wp =
let wp_havoc_raw {known_map = kn} reg_havoc wr cv wp =
let dst = dst_of_wp cv wp in
if Mpv.is_empty dst then wp else
let regs = name_regions kn cv dst in
......@@ -472,7 +506,7 @@ let wp_havoc {known_map = kn} {eff_writes = wr; eff_covers = cv} wp =
let add _ t fvs = t_freevars fvs t in
let fvs = Mreg.fold add regs Mvs.empty in
let update {pv_vs = o; pv_ity = ity} n wp =
let t, fl = havoc kn wr regs (t_var o) ity [] in
let t, fl = havoc kn reg_havoc wr regs (t_var o) ity [] in
if Mvs.mem n fvs then
sp_implies (t_and_l (cons_t_simp (t_var n) t fl)) wp
else wp_let n t (sp_implies (t_and_l fl) wp) in
......@@ -480,7 +514,10 @@ let wp_havoc {known_map = kn} {eff_writes = wr; eff_covers = cv} wp =
let wp = Mpv.fold update dst wp in
wp_forall (Mvs.keys fvs) wp
let sp_havoc {known_map = kn} {eff_writes = wr; eff_covers = cv} res sp dst =
let wp_havoc env {eff_writes = wr; eff_covers = cv} wp =
wp_havoc_raw env havoc_effect wr cv wp
let sp_havoc_raw {known_map = kn} reg_havoc wr cv res sp dst =
if Sreg.is_empty cv then sp else
let rd = vc_freepvs Spv.empty res sp in
let dst = dst_step_back_raw cv rd Mreg.empty dst in
......@@ -488,11 +525,14 @@ let sp_havoc {known_map = kn} {eff_writes = wr; eff_covers = cv} res sp dst =
let regs = name_regions kn cv dst in
let () = print_dst dst; print_regs regs in
let update {pv_vs = o; pv_ity = ity} n sp =
let t, fl = havoc kn wr regs (t_var o) ity [] in
let t, fl = havoc kn reg_havoc wr regs (t_var o) ity [] in
sp_and (t_and_l (cons_t_simp (t_var n) t fl)) sp in
let sp = t_subst (advancement dst) sp in
sp_and sp (Mpv.fold update dst t_true)
let sp_havoc env {eff_writes = wr; eff_covers = cv} res sp dst =
sp_havoc_raw env havoc_effect wr cv res sp dst
let sp_complete {eff_covers = cv} sp dst =
let check o n sp =
if pv_affected cv o then sp else
......@@ -656,9 +696,10 @@ let rec wp_expr env e res q xq = match e.e_node with
end
| Eabsurd ->
vc_label e (vc_expl expl_absurd t_false)
| Eassign _ ->
let _q = t_subst_single res t_void q in
assert false (* TODO *)
| Eassign asl ->
let q = t_subst_single res t_void q in
let wr = writes_of_assign asl in
vc_label e (wp_havoc_raw env havoc_assign wr e.e_effect.eff_covers q)
| Ewhile (e0, invl, varl, e1) ->
(* wp(while e0 inv I var V do e1 done, Q, R) =
I and forall S. I ->
......@@ -808,7 +849,10 @@ and sp_expr env e res xres dst = match e.e_node with
| Eabsurd ->
let ok = vc_label e (vc_expl expl_absurd t_false) in
ok, ok, Mexn.empty
| Eassign _ -> assert false (* TODO *)
| Eassign asl ->
let sp = sp_havoc_raw env havoc_assign
(writes_of_assign asl) e.e_effect.eff_covers res t_true dst in
t_true, vc_label e sp, Mexn.empty
| Ewhile (e0, invl, varl, e1) ->
(* ok: I /\ !! I -> (ok0 /\ (ne0 -> test -> ok1 /\ (ne1 -> I /\ V)))
ne: !! I /\ (ne0 /\ !test)
......
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