From 49279228f8a37f84c73c1416bb36475fb97a394d Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Fri, 18 Sep 2020 11:47:49 +0200 Subject: Some renaming --- kvx/lib/RTLpathSE_impl_junk.v | 359 +++++++++++++++++++++++++++--------------- 1 file changed, 230 insertions(+), 129 deletions(-) (limited to 'kvx') diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v index bd6fafa4..3963326a 100644 --- a/kvx/lib/RTLpathSE_impl_junk.v +++ b/kvx/lib/RTLpathSE_impl_junk.v @@ -20,8 +20,8 @@ Local Open Scope impure. Import ListNotations. Local Open Scope list_scope. -Ltac wlp_intros varname hname := apply wlp_unfold; intros varname hname. -Ltac wlp_step_bind varname hname := apply wlp_bind; wlp_intros varname hname. +Ltac wlp_intro varname hname := apply wlp_unfold; intros varname hname. +Ltac wlp_bind varname hname := apply wlp_bind; wlp_intro varname hname. Ltac wlp_absurd := match goal with | [ H : FAILWITH ?msg |- _ ] => eapply (_FAILWITH_correct _ _ (fun _ => False)) in H; inv H @@ -33,19 +33,18 @@ end. (** ** Implementation of symbolic values/symbolic memories with hash-consing data *) Inductive hsval := - | HSinput (r: reg) (hid:hashcode) - | HSop (op:operation) (hlsv: hlist_sval) (hsm: hsmem) (hid:hashcode) - | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (hid:hashcode) -with hlist_sval := - | HSnil (hid:hashcode) - | HScons (hsv: hsval) (hlsv: hlist_sval) (hid:hashcode) -(* symbolic memory *) + | HSinput (r: reg) (hid: hashcode) + | HSop (op: operation) (lhsv: list_hsval) (hsm: hsmem) (hid: hashcode) + | HSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (hid: hashcode) +with list_hsval := + | HSnil (hid: hashcode) + | HScons (hsv: hsval) (lhsv: list_hsval) (hid: hashcode) with hsmem := - | HSinit (hid:hashcode) - | HSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval) (hid:hashcode). + | HSinit (hid: hashcode) + | HSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval) (hid:hashcode). Scheme hsval_mut := Induction for hsval Sort Prop -with hlist_sval_mut := Induction for hlist_sval Sort Prop +with list_hsval_mut := Induction for list_hsval Sort Prop with hsmem_mut := Induction for hsmem Sort Prop. Definition hsval_get_hid (hsv: hsval): hashcode := @@ -55,13 +54,13 @@ Definition hsval_get_hid (hsv: hsval): hashcode := | HSload _ _ _ _ _ hid => hid end. -Definition hlist_sval_get_hid (hlsv: hlist_sval): hashcode := - match hlsv with +Definition list_hsval_get_hid (lhsv: list_hsval): hashcode := + match lhsv with | HSnil hid => hid | HScons _ _ hid => hid end. -Definition hsmem_get_hid (hsm: hsmem ): hashcode := +Definition hsmem_get_hid (hsm: hsmem): hashcode := match hsm with | HSinit hid => hid | HSstore _ _ _ _ _ hid => hid @@ -70,30 +69,29 @@ Definition hsmem_get_hid (hsm: hsmem ): hashcode := Definition hsval_set_hid (hsv: hsval) (hid: hashcode): hsval := match hsv with | HSinput r _ => HSinput r hid - | HSop o hlsv hsm _ => HSop o hlsv hsm hid - | HSload hsm trap chunk addr hlsv _ => HSload hsm trap chunk addr hlsv hid + | HSop o lhsv hsm _ => HSop o lhsv hsm hid + | HSload hsm trap chunk addr lhsv _ => HSload hsm trap chunk addr lhsv hid end. -Definition hlist_sval_set_hid (hlsv: hlist_sval) (hid: hashcode): hlist_sval := - match hlsv with +Definition list_hsval_set_hid (lhsv: list_hsval) (hid: hashcode): list_hsval := + match lhsv with | HSnil _ => HSnil hid - | HScons hsv hlsv _ => HScons hsv hlsv hid + | HScons hsv lhsv _ => HScons hsv lhsv hid end. -Definition hsmem_set_hid (hsm: hsmem ) (hid: hashcode): hsmem := +Definition hsmem_set_hid (hsm: hsmem) (hid: hashcode): hsmem := match hsm with | HSinit _ => HSinit hid - | HSstore hsm chunk addr hlsv srce _ => HSstore hsm chunk addr hlsv srce hid + | HSstore hsm chunk addr lhsv srce _ => HSstore hsm chunk addr lhsv srce hid end. -(* Now, we build the hash-Cons value from a "hash_eq". +(** Now, we build the hash-Cons value from a "hash_eq". -Informal specification: - [hash_eq] must be consistent with the "hashed" constructors defined above. + Informal specification: + [hash_eq] must be consistent with the "hashed" constructors defined above. -We expect that hashinfo values in the code of these "hashed" constructors verify: - - (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y) + We expect that hashinfo values in the code of these "hashed" constructors verify: + (hash_eq (hdata x) (hdata y) ~> true) <-> (hcodes x)=(hcodes y) *) Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool := @@ -116,7 +114,7 @@ Definition hsval_hash_eq (sv1 sv2: hsval): ?? bool := | _,_ => RET false end. -Definition hlist_sval_hash_eq (lsv1 lsv2: hlist_sval): ?? bool := +Definition list_hsval_hash_eq (lsv1 lsv2: list_hsval): ?? bool := match lsv1, lsv2 with | HSnil _, HSnil _ => RET true | HScons sv1 lsv1' _, HScons sv2 lsv2' _ => @@ -142,7 +140,7 @@ Definition hsmem_hash_eq (sm1 sm2: hsmem): ?? bool := end. Definition hSVAL: hashP hsval := {| hash_eq := hsval_hash_eq; get_hid:=hsval_get_hid; set_hid:=hsval_set_hid |}. -Definition hLSVAL: hashP hlist_sval := {| hash_eq := hlist_sval_hash_eq; get_hid:= hlist_sval_get_hid; set_hid:= hlist_sval_set_hid |}. +Definition hLSVAL: hashP list_hsval := {| hash_eq := list_hsval_hash_eq; get_hid:= list_hsval_get_hid; set_hid:= list_hsval_set_hid |}. Definition hSMEM: hashP hsmem := {| hash_eq := hsmem_hash_eq; get_hid:= hsmem_get_hid; set_hid:= hsmem_set_hid |}. Program Definition mk_hash_params: Dict.hash_params hsval := @@ -155,16 +153,16 @@ Obligation 1. Qed. -(* Symbolic final value -- from hash-consed values -It does not seem useful to hash-consed these final values (because they are final). +(** Symbolic final value -- from hash-consed values + It does not seem useful to hash-consed these final values (because they are final). *) Inductive hsfval := | HSnone - | HScall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval) (res:reg) (pc:node) - | HStailcall (sig:signature) (svos: hsval + ident) (lsv:hlist_sval) - | HSbuiltin (ef:external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc:node) + | HScall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) (res: reg) (pc: node) + | HStailcall (sig: signature) (svos: hsval + ident) (lsv: list_hsval) + | HSbuiltin (ef: external_function) (sargs: list (builtin_arg hsval)) (res: builtin_res reg) (pc: node) | HSjumptable (sv: hsval) (tbl: list node) - | HSreturn (res:option hsval) + | HSreturn (res: option hsval) . (** ** Implementation of symbolic states @@ -185,7 +183,7 @@ Record hsistate_local := (* Syntax and semantics of symbolic exit states *) Record hsistate_exit := mk_hsistate_exit - { hsi_cond: condition; hsi_scondargs: hlist_sval; hsi_elocal: hsistate_local; hsi_ifso: node }. + { hsi_cond: condition; hsi_scondargs: list_hsval; hsi_elocal: hsistate_local; hsi_ifso: node }. (** ** Syntax and Semantics of symbolic internal state *) @@ -222,12 +220,12 @@ Hypothesis hC_hsval_correct: forall hs rhsv, (hsval_proj (hdata hs)) = (hsval_proj rhsv). Local Hint Resolve hC_hsval_correct: wlp. -Variable hC_hlist_sval: hashinfo hlist_sval -> ?? hlist_sval. +Variable hC_list_hsval: hashinfo list_hsval -> ?? list_hsval. -Hypothesis hC_hlist_sval_correct: forall hs rhsv, - hC_hlist_sval hs ~~> rhsv -> +Hypothesis hC_list_hsval_correct: forall hs rhsv, + hC_list_hsval hs ~~> rhsv -> (hsval_list_proj (hdata hs)) = (hsval_list_proj rhsv). -Local Hint Resolve hC_hlist_sval_correct: wlp. +Local Hint Resolve hC_list_hsval_correct: wlp. Variable hC_hsmem: hashinfo hsmem -> ?? hsmem. @@ -252,48 +250,46 @@ Definition hSinput (r:reg): ?? hsval := DO hv <~ hSinput_hcodes r;; hC_hsval {| hdata:=HSinput r unknown_hid; hcodes :=hv; |}. - -Definition hSop_hcodes (op:operation) (hlsv: hlist_sval) (hsm: hsmem) := +Definition hSop_hcodes (op:operation) (lhsv: list_hsval) (hsm: hsmem) := DO hc <~ hash op_hcode;; DO hv <~ hash op;; - RET [hc;hv;hlist_sval_get_hid hlsv; hsmem_get_hid hsm]. + RET [hc;hv;list_hsval_get_hid lhsv; hsmem_get_hid hsm]. Extraction Inline hSop_hcodes. -Definition hSop (op:operation) (hlsv: hlist_sval) (hsm: hsmem): ?? hsval := - DO hv <~ hSop_hcodes op hlsv hsm;; - hC_hsval {| hdata:=HSop op hlsv hsm unknown_hid; hcodes :=hv |}. - +Definition hSop (op:operation) (lhsv: list_hsval) (hsm: hsmem): ?? hsval := + DO hv <~ hSop_hcodes op lhsv hsm;; + hC_hsval {| hdata:=HSop op lhsv hsm unknown_hid; hcodes :=hv |}. -Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval):= +Definition hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval):= DO hc <~ hash load_hcode;; DO hv1 <~ hash trap;; DO hv2 <~ hash chunk;; DO hv3 <~ hash addr;; - RET [hc;hsmem_get_hid hsm;hv1;hv2;hv3;hlist_sval_get_hid hlsv]. + RET [hc; hsmem_get_hid hsm; hv1; hv2; hv3; list_hsval_get_hid lhsv]. Extraction Inline hSload_hcodes. -Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval): ?? hsval := - DO hv <~ hSload_hcodes hsm trap chunk addr hlsv;; - hC_hsval {| hdata:=HSload hsm trap chunk addr hlsv unknown_hid; hcodes :=hv |}. +Definition hSload (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval): ?? hsval := + DO hv <~ hSload_hcodes hsm trap chunk addr lhsv;; + hC_hsval {| hdata := HSload hsm trap chunk addr lhsv unknown_hid; hcodes := hv |}. -Definition hSnil (_: unit): ?? hlist_sval := - hC_hlist_sval {| hdata:=HSnil unknown_hid; hcodes := nil |}. +Definition hSnil (_: unit): ?? list_hsval := + hC_list_hsval {| hdata := HSnil unknown_hid; hcodes := nil |}. -Definition hScons (hsv: hsval) (hlsv: hlist_sval): ?? hlist_sval := - hC_hlist_sval {| hdata:=HScons hsv hlsv unknown_hid; hcodes := [hsval_get_hid hsv; hlist_sval_get_hid hlsv] |}. +Definition hScons (hsv: hsval) (lhsv: list_hsval): ?? list_hsval := + hC_list_hsval {| hdata := HScons hsv lhsv unknown_hid; hcodes := [hsval_get_hid hsv; list_hsval_get_hid lhsv] |}. Definition hSinit (_: unit): ?? hsmem := - hC_hsmem {| hdata:=HSinit unknown_hid; hcodes := nil |}. + hC_hsmem {| hdata := HSinit unknown_hid; hcodes := nil |}. -Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval):= +Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval):= DO hv1 <~ hash chunk;; DO hv2 <~ hash addr;; - RET [hsmem_get_hid hsm;hv1;hv2;hlist_sval_get_hid hlsv;hsval_get_hid srce]. + RET [hsmem_get_hid hsm; hv1; hv2; list_hsval_get_hid lhsv; hsval_get_hid srce]. Extraction Inline hSstore_hcodes. -Definition hSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval): ?? hsmem := - DO hv <~ hSstore_hcodes hsm chunk addr hlsv srce;; - hC_hsmem {| hdata:=HSstore hsm chunk addr hlsv srce unknown_hid; hcodes := hv |}. +Definition hSstore (hsm: hsmem) (chunk: memory_chunk) (addr: addressing) (lhsv: list_hsval) (srce: hsval): ?? hsmem := + DO hv <~ hSstore_hcodes hsm chunk addr lhsv srce;; + hC_hsmem {| hdata := HSstore hsm chunk addr lhsv srce unknown_hid; hcodes := hv |}. Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval := @@ -302,17 +298,17 @@ Definition hsi_sreg_get (hst: PTree.t hsval) r: ?? hsval := | Some sv => RET sv end. -Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? hlist_sval := +Fixpoint hlist_args (hst: PTree.t hsval) (l: list reg): ?? list_hsval := match l with | nil => hSnil() | r::l => DO v <~ hsi_sreg_get hst r;; - DO hlsv <~ hlist_args hst l;; - hScons v hlsv + DO lhsv <~ hlist_args hst l;; + hScons v lhsv end. (** ** Assignment of memory *) -Definition hslocal_store (hst:hsistate_local) chunk addr args src: ?? hsistate_local := +Definition hslocal_store (hst: hsistate_local) chunk addr args src: ?? hsistate_local := let pt := hst.(hsi_sreg) in DO hargs <~ hlist_args pt args;; DO hsrc <~ hsi_sreg_get pt src;; @@ -329,56 +325,56 @@ Definition hsist_set_local (hst: hsistate) (pc: node) (hnxt: hsistate_local): hs (** ** Assignment of registers *) -(* locally new symbolic values during symbolic execution *) +(** locally new symbolic values during symbolic execution *) Inductive root_sval: Type := -| Rop (op:operation) -| Rload (trap: trapping_mode) (chunk:memory_chunk) (addr:addressing) +| Rop (op: operation) +| Rload (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) . -Definition root_apply (rsv: root_sval) (lsv: list reg) (hst: hsistate_local) : ?? hsval := - DO hlsv <~ hlist_args hst lsv;; +Definition root_apply (rsv: root_sval) (lr: list reg) (hst: hsistate_local) : ?? hsval := + DO lhsv <~ hlist_args hst lr;; match rsv with - | Rop op => hSop op hlsv hst - | Rload trap chunk addr => hSload hst trap chunk addr hlsv + | Rop op => hSop op lhsv hst + | Rload trap chunk addr => hSload hst trap chunk addr lhsv end. Local Open Scope lazy_bool_scope. (* NB: return [false] if the rsv cannot fail *) -Definition may_trap (rsv: root_sval) (lsv: list reg): bool := +Definition may_trap (rsv: root_sval) (lr: list reg): bool := match rsv with - | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lsv) (args_of_operation op)) (* cf. lemma is_trapping_op_sound *) + | Rop op => is_trapping_op op ||| negb (Nat.eqb (length lr) (args_of_operation op)) (* cf. lemma is_trapping_op_sound *) | Rload TRAP _ _ => true | _ => false end. -(* simplify a symbolic value before assignment to a register *) -Definition simplify (rsv: root_sval) (lsv: list reg) (hst: hsistate_local): ?? hsval := +(** simplify a symbolic value before assignment to a register *) +Definition simplify (rsv: root_sval) (lr: list reg) (hst: hsistate_local): ?? hsval := match rsv with | Rop op => - match is_move_operation op lsv with - | Some arg => hsi_sreg_get hst arg (* optimization of Omove *) + match is_move_operation op lr with + | Some arg => hsi_sreg_get hst arg (** optimization of Omove *) | None => DO hsi <~ hSinit ();; - DO hlsv <~ hlist_args hst lsv;; - hSop op hlsv hsi (* magically remove the dependency on sm ! *) + DO lhsv <~ hlist_args hst lr;; + hSop op lhsv hsi (** magically remove the dependency on sm ! *) end | Rload _ chunk addr => - DO hlsv <~ hlist_args hst lsv;; - hSload hst NOTRAP chunk addr hlsv + DO lhsv <~ hlist_args hst lr;; + hSload hst NOTRAP chunk addr lhsv end. -Definition red_PTree_set (r:reg) (sv: hsval) (hst: PTree.t hsval): PTree.t hsval := - match sv with +Definition red_PTree_set (r: reg) (hsv: hsval) (hst: PTree.t hsval): PTree.t hsval := + match hsv with | HSinput r' _ => if Pos.eq_dec r r' then PTree.remove r' hst - else PTree.set r sv hst - | _ => PTree.set r sv hst + else PTree.set r hsv hst + | _ => PTree.set r hsv hst end. -Definition hslocal_set_sreg (hst:hsistate_local) (r:reg) (rsv:root_sval) lsv: ?? hsistate_local := - DO hsiok <~ +Definition hslocal_set_sreg (hst: hsistate_local) (r: reg) (rsv: root_sval) lsv: ?? hsistate_local := + DO hsiok <~ (if may_trap rsv lsv then DO hv <~ root_apply rsv lsv hst;; RET (hv::(hsi_ok_lsval hst)) else RET (hsi_ok_lsval hst));; @@ -465,7 +461,6 @@ Definition hsum_left (hst: PTree.t hsval) (ros: reg + ident): ?? (hsval + ident) end. - (** * The simulation test of concrete hash-consed symbolic execution *) Definition phys_check {A} (x y:A) (msg: pstring): ?? unit := @@ -482,7 +477,7 @@ Qed. Global Opaque phys_check. Hint Resolve phys_check_correct: wlp. -Definition struct_check {A} (x y:A) (msg: pstring): ?? unit := +Definition struct_check {A} (x y: A) (msg: pstring): ?? unit := DO b <~ struct_eq x y;; assert_b b msg;; RET tt. @@ -1052,7 +1047,7 @@ Remark init_hsistate_correct_dyn ge sp rs0 m0 pc: WHEN init_hsistate pc ~> hst THEN hsistate_refines_dyn ge sp rs0 m0 hst (init_sistate pc). Proof. - unfold init_hsistate. wlp_step_bind hst HST. + unfold init_hsistate. wlp_bind hst HST. wlp_simplify. constructor; simpl; auto; [|constructor]. - apply list_forall2_nil. @@ -1266,7 +1261,7 @@ Definition sum_refines (hsi: hsval + ident) (si: sval + ident) := | _, _ => False end. -Inductive list_refines: hlist_sval -> list_sval -> Prop := +Inductive list_refines: list_hsval -> list_sval -> Prop := | hsnil_ref: forall h, list_refines (HSnil h) Snil | hscons_ref: forall lhv lsv hv sv h, list_refines lhv lsv -> @@ -1320,18 +1315,18 @@ Proof. constructor. Qed. End HFINAL_REFINES. -Lemma list_proj_refines_eq ge ge' sp rs0 m0: forall lsv hlsv, +Lemma list_proj_refines_eq ge ge' sp rs0 m0: forall lsv lhsv, (forall s, Genv.find_symbol ge s = Genv.find_symbol ge' s) -> - list_refines ge sp rs0 m0 hlsv lsv -> - forall hlsv' lsv', - list_refines ge' sp rs0 m0 hlsv' lsv' -> - hsval_list_proj hlsv = hsval_list_proj hlsv' -> + list_refines ge sp rs0 m0 lhsv lsv -> + forall lhsv' lsv', + list_refines ge' sp rs0 m0 lhsv' lsv' -> + hsval_list_proj lhsv = hsval_list_proj lhsv' -> seval_list_sval ge sp lsv rs0 m0 = seval_list_sval ge' sp lsv' rs0 m0. Proof. induction 2; rename H into GFS. - - simpl. intros. destruct hlsv'; try discriminate. clear H0. + - simpl. intros. destruct lhsv'; try discriminate. clear H0. inv H. simpl. reflexivity. - - simpl. intros. destruct hlsv'; try discriminate. + - simpl. intros. destruct lhsv'; try discriminate. simpl in H2. inv H2. destruct lsv'; [inv H|]. inv H. simpl. assert (SVALEQ: seval_sval ge sp sv rs0 m0 = seval_sval ge' sp sv0 rs0 m0). { @@ -1534,7 +1529,7 @@ Lemma sval_refines_local_get ge sp rs0 m0 hsl sl r: WHEN hsi_sreg_get hsl r ~> hsv THEN sval_refines ge sp rs0 m0 hsv (si_sreg sl r). Proof. - intros HOK HREF. wlp_intros hsv HSV. unfold sval_refines. + intros HOK HREF. wlp_intro hsv HSV. unfold sval_refines. erewrite <- hsi_sreg_eval_correct; eauto. destruct HREF as (_ & _ & A & _). rewrite <- A; [| assumption]. reflexivity. @@ -1547,14 +1542,14 @@ Lemma hsum_left_correct ge sp rs0 m0 hsl sl ros: sum_refines ge sp rs0 m0 svos (sum_left_map (si_sreg sl) ros). Proof. intros HOK HREF. destruct ros; [| wlp_simplify]. - wlp_step_bind hr HGET. wlp_simplify. unfold sval_refines. + wlp_bind hr HGET. wlp_simplify. unfold sval_refines. rewrite sval_refines_local_get; eauto. Qed. Lemma hSnil_correct: WHEN hSnil () ~> shv THEN hsval_list_proj shv = Snil. Proof. - wlp_simplify. unfold hSnil in Hexta. apply hC_hlist_sval_correct in Hexta. + wlp_simplify. unfold hSnil in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. symmetry. assumption. Qed. Global Opaque hSnil. @@ -1565,9 +1560,9 @@ Lemma hScons_correct: forall lhsv hsv, hsval_list_proj lhsv' = Scons (hsval_proj hsv) (hsval_list_proj lhsv). Proof. destruct lhsv; wlp_simplify. - - unfold hScons in Hexta. apply hC_hlist_sval_correct in Hexta. + - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. congruence. - - unfold hScons in Hexta. apply hC_hlist_sval_correct in Hexta. simpl in *. congruence. + - unfold hScons in Hexta. apply hC_list_hsval_correct in Hexta. simpl in *. congruence. Qed. Global Opaque hScons. Hint Resolve hScons_correct: wlp. @@ -1578,7 +1573,7 @@ Lemma hsi_sreg_get_refines ge sp rs0 m0 hsl sl r: WHEN hsi_sreg_get hsl r ~> hsv THEN sval_refines ge sp rs0 m0 hsv (si_sreg sl r). Proof. - intros HOK HREF. wlp_intros hsv HGET. destruct HREF as (_ & _ & A & _). + intros HOK HREF. wlp_intro hsv HGET. destruct HREF as (_ & _ & A & _). unfold sval_refines. erewrite <- hsi_sreg_eval_correct by eassumption. rewrite A by assumption. reflexivity. Qed. @@ -1604,7 +1599,7 @@ Lemma hsval_proj_correct ge sp rs0 m0 hsl sl hsv r: hsval_proj hsv = hsval_proj hsv' -> sval_refines ge sp rs0 m0 hsv (si_sreg sl r). Proof. - intros HOK HREF. wlp_intros hsv' HGET. intros PROJ. + intros HOK HREF. wlp_intro hsv' HGET. intros PROJ. unfold sval_refines. unfold seval_hsval. rewrite PROJ. enough (seval_sval ge sp (hsval_proj hsv') rs0 m0 = seval_hsval ge sp hsv' rs0 m0) as ->; [|reflexivity]. erewrite hsi_sreg_get_refines; eauto. @@ -1620,7 +1615,7 @@ Lemma hlist_args_correct ge sp rs0 m0 hsl sl: Proof. intros HOK HREF. induction lr. - simpl. wlp_simplify. destruct exta; try discriminate. constructor. - - simpl. wlp_step_bind v V. wlp_step_bind hlsv HLSV. wlp_simplify. + - simpl. wlp_bind v V. wlp_bind lhsv HLSV. wlp_simplify. apply IHlr in HLSV. clear IHlr. destruct exta; try discriminate. simpl in H. inv H. constructor. + eapply hsval_list_proj_correct; eauto. @@ -1641,7 +1636,7 @@ Proof. induction br. all: try (wlp_simplify; constructor; auto; fail). (* BA *) - - simpl. wlp_step_bind hsv HGET. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto. + - simpl. wlp_bind hsv HGET. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto. Qed. Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl: @@ -1653,7 +1648,7 @@ Lemma hbuiltin_args_correct ge sp rs0 m0 hsl sl: Proof. intros HOK HREF. induction lbr; [wlp_simplify; constructor|]. - simpl. wlp_step_bind ha HA. wlp_step_bind hl HL. wlp_simplify. + simpl. wlp_bind ha HA. wlp_bind hl HL. wlp_simplify. constructor; [|auto]. eapply hbuiltin_arg_correct; eauto. Qed. @@ -1666,20 +1661,20 @@ Proof. intro HOK. destruct i; simpl; intros HLREF; try (wlp_simplify; apply hfinal_refines_snone). (* Scall *) - - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_simplify. constructor. + - wlp_bind svos SVOS. wlp_bind sargs SARGS. wlp_simplify. constructor. + eapply hsum_left_correct; eauto. + eapply hlist_args_correct; eauto. (* Stailcall *) - - wlp_step_bind svos SVOS. wlp_step_bind sargs SARGS. wlp_simplify. constructor. + - wlp_bind svos SVOS. wlp_bind sargs SARGS. wlp_simplify. constructor. + eapply hsum_left_correct; eauto. + eapply hlist_args_correct; eauto. (* Sbuiltin *) - wlp_simplify. constructor. eapply hbuiltin_args_correct; eauto. (* Sjumptable *) - - wlp_step_bind sv SV. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto. + - wlp_bind sv SV. wlp_simplify. constructor. eapply hsi_sreg_get_refines; eauto. (* Sreturn *) - destruct o. - -- wlp_step_bind sv HGET. wlp_simplify. constructor. simpl. + -- wlp_bind sv HGET. wlp_simplify. constructor. simpl. eapply hsi_sreg_get_refines; eauto. -- wlp_simplify. repeat constructor. Qed. @@ -1755,12 +1750,12 @@ Proof. - destruct bs2; wlp_simplify; try wlp_absurd. congruence. (* BA_splitlong *) - destruct bs2; try (wlp_simplify; wlp_absurd). simpl. - wlp_step_bind b1 B1. wlp_intros b2 B2. + wlp_bind b1 B1. wlp_intro b2 B2. rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption. reflexivity. (* BA_addptr *) - destruct bs2; try (wlp_simplify; wlp_absurd). simpl. - wlp_step_bind b1 B1. wlp_intros b2 B2. + wlp_bind b1 B1. wlp_intro b2 B2. rewrite IHbs1_1 by eassumption. rewrite IHbs1_2 by eassumption. reflexivity. Qed. @@ -1822,18 +1817,18 @@ Theorem sfval_simu_check_correct dm f opc1 opc2 fv1 fv2: Proof. destruct fv1; destruct fv2; try (wlp_simplify; simpl in Hexta; wlp_absurd). (* HScall *) - - simpl. wlp_step_bind u1 REVMAP. wlp_step_bind u2 SIG. wlp_step_bind u3 RES. - wlp_step_bind u4 SVOS. wlp_intros u5 LSV. + - simpl. wlp_bind u1 REVMAP. wlp_bind u2 SIG. wlp_bind u3 RES. + wlp_bind u4 SVOS. wlp_intro u5 LSV. apply phys_check_correct in SIG. apply phys_check_correct in RES. apply revmap_check_single_correct in REVMAP. apply phys_check_correct in LSV. apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto). (* HStailcall *) - - simpl. wlp_step_bind u1 SIG. wlp_step_bind u2 SVOS. wlp_intros u3 LSV. + - simpl. wlp_bind u1 SIG. wlp_bind u2 SVOS. wlp_intro u3 LSV. apply phys_check_correct in SIG. apply phys_check_correct in LSV. apply svos_simu_check_correct in SVOS. subst. repeat (constructor; auto). (* HSbuiltin *) - - simpl. wlp_step_bind u1 RMAP. wlp_step_bind u2 EF. wlp_step_bind u3 RES. - wlp_intros u4 SARGS. + - simpl. wlp_bind u1 RMAP. wlp_bind u2 EF. wlp_bind u3 RES. + wlp_intro u4 SARGS. apply phys_check_correct in EF. apply phys_check_correct in RES. apply list_builtin_arg_simu_check_correct in SARGS. apply revmap_check_single_correct in RMAP. subst. repeat (constructor; auto). @@ -1885,7 +1880,104 @@ Proof. wlp_simplify. constructor. 1-2: assumption. Qed. Hint Resolve hsstate_simu_check_correct: wlp. -Global Opaque hsstate_simu_core. +Global Opaque hsstate_simu_core. + +Definition seval_list_hsval ge sp lhsv rs m := seval_list_sval ge sp (hsval_list_proj lhsv) rs m. + +Definition hok_args ge sp rs0 m0 hst lhsv := + hsok_local ge sp rs0 m0 hst -> + (seval_list_hsval ge sp lhsv rs0 m0 <> None). + +(* Lemma hslocal_set_sreg_correct ge sp rs0 m0 hst st r (rsv:root_sval) lhsv sv': + hsilocal_refines ge sp rs0 m0 hst st -> + hok_args ge sp rs0 m0 hst lhsv -> + (hsok_local ge sp rs0 m0 hst -> seval_hsval ge sp hsv' rs0 m0 = seval_hsval ge sp (rsv lhsv (hsi_smem hst)) rs0 m0) -> + hsilocal_refines ge sp rs0 m0 (hslocal_set_sreg hst r rsv lsv) (slocal_set_sreg st r sv'). +Proof. + intros (ROK & RMEM & RVAL) OKA RSV. + unfold hsilocal_refines; simpl. rewrite! hsok_local_set_sreg; eauto. split. + + rewrite <- ROK in RSV; rewrite sok_local_set_sreg; eauto. + intuition congruence. + + split; try tauto. + intros (HOKL & RSV2) r0. + rewrite red_PTree_set_correct. + rewrite hsi_sreg_eval_correct. unfold hsi_sreg_get. + destruct (Pos.eq_dec r r0). + * subst. rewrite PTree.gss, RSV; auto. + destruct (seval_sval ge sp (rsv lsv (hsi_smem hst))) eqn: RSV3; simpl; try congruence. + eapply simplify_correct; eauto. + * intros; rewrite PTree.gso; auto. + rewrite <- RVAL, hsi_sreg_eval_correct; auto. +Qed. *) + +(* Lemma refines_hokargs ge sp rs0 m0 hst st l: + hsistate_refines_dyn ge sp rs0 m0 hst st -> + WHEN hlist_args (hsi_local hst) l ~> lhsv THEN + hok_args ge sp rs0 m0 (hsi_local hst) lhsv. +Proof. + unfold hok_args. intros (_ & HLREF & _). + wlp_intro lhsv LHSV. intros HOK. + eapply hlist_args_correct in LHSV; eauto. + + + intros (_ & HLREF & _) OK. + erewrite seval_list_sval_refines; eauto. + destruct HLREF as (OKEQ & _ & _). + rewrite <- OKEQ in OK. + destruct OK as (_ & _ & OK). + clear OKEQ; induction l as [|r l]; simpl; try congruence. + simplify_SOME x. congruence. +Qed. *) + +(* Local Hint Resolve refines_okargs: core. +Lemma hsiexec_inst_correct_dyn ge sp rs0 m0 i hst st hst' st': + hsiexec_inst i hst = Some hst' -> + siexec_inst i st = Some st' -> + hsistate_refines_dyn ge sp rs0 m0 hst st -> hsistate_refines_dyn ge sp rs0 m0 hst' st'. +Proof. + destruct i; simpl; intros STEP1 STEP2; inversion_clear STEP1; + inversion_clear STEP2; discriminate || (intro REF; eauto). + - (* Iop *) + eapply hsist_set_local_correct_dyn; eauto. + + eapply hslocal_set_sreg_correct; eauto. + simpl; intros. + erewrite seval_list_sval_refines; eauto. + erewrite seval_smem_refines; eauto. + + unfold sok_local; simpl; intros (PRE & MEM & REG). + intuition. + generalize (REG r0); clear REG. + destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). + - (* Iload *) + eapply hsist_set_local_correct_dyn; eauto. + + eapply hslocal_set_sreg_correct; eauto. + simpl; intros. + erewrite seval_list_sval_refines; eauto. + erewrite seval_smem_refines; eauto. + + unfold sok_local; simpl; intros (PRE & MEM & REG). + intuition. + generalize (REG r0); clear REG. + destruct (Pos.eq_dec r r0); simpl; intuition (subst; eauto). + - (* Istore *) + eapply hsist_set_local_correct_dyn; eauto. + + eapply hslocal_set_mem_correct; eauto. + * simpl. simplify_SOME x. + * intros. simpl. + erewrite seval_list_sval_refines; eauto. + erewrite seval_smem_refines; eauto. + erewrite seval_sval_refines; eauto. + + unfold sok_local; simpl; intuition. + - (* Icond *) + destruct REF as (EXREF & LREF & NEST). + split. + + constructor; simpl; auto. + constructor; simpl; auto. + intros; erewrite seval_condition_refines; eauto. + unfold seval_condition. + erewrite seval_list_sval_refines; eauto. + + split; simpl; auto. + destruct NEST as [|st0 se lse TOP NEST]; + econstructor; simpl; auto; constructor; auto. +Qed. *) Definition hsexec (f: function) (pc:node): ?? hsstate := DO path <~ some_or_fail ((fn_path f)!pc) "hsexec.internal_error.1";; @@ -1899,6 +1991,15 @@ Definition hsexec (f: function) (pc:node): ?? hsstate := RET {| hinternal := hst; hfinal := hsvf |} end. +(** + * init_hsistate_correct_stat : OK + * init_hsistate_correct_dyn : OK + * hsexec_final_correct : OK + * hsiexec_inst_correct_dyn : TODO + * hsiexec_path_correct_dyn : TODO + * hfinal_refines_snone : OK + *) + (* Local Hint Resolve init_hsistate_correct_stat init_hsistate_correct_dyn hsexec_final_correct hsiexec_inst_correct_dyn hsiexec_path_correct_dyn hfinal_refines_snone: core. *) @@ -1930,9 +2031,9 @@ Definition simu_check_single (dm: PTree.t node) (f: RTLpath.function) (tf: RTLpa let (pc2, pc1) := m in (* creating the hash-consing tables *) DO hC_sval <~ hCons hSVAL;; - DO hC_hlist_sval <~ hCons hLSVAL;; + DO hC_list_hsval <~ hCons hLSVAL;; DO hC_hsmem <~ hCons hSMEM;; - let hsexec := hsexec hC_sval.(hC) hC_hlist_sval.(hC) hC_hsmem.(hC) in + let hsexec := hsexec hC_sval.(hC) hC_list_hsval.(hC) hC_hsmem.(hC) in (* performing the hash-consed executions *) DO hst1 <~ hsexec f pc1;; DO hst2 <~ hsexec tf pc2;; @@ -1944,13 +2045,13 @@ Lemma simu_check_single_correct dm tf f pc1 pc2: sexec_simu dm f tf pc1 pc2. Proof. unfold simu_check_single. - wlp_step_bind hC_sval HSVAL. wlp_step_bind hC_hlist_sval HLSVAL. - wlp_step_bind hC_hsmem HSMEM. wlp_step_bind hst1 HSEXEC1. wlp_step_bind hst2 HSEXEC2. - wlp_intros u HSIMU. + wlp_bind hC_sval HSVAL. wlp_bind hC_list_hsval HLSVAL. + wlp_bind hC_hsmem HSMEM. wlp_bind hst1 HSEXEC1. wlp_bind hst2 HSEXEC2. + wlp_intro u HSIMU. unfold sexec_simu. intros st1 SEXEC. explore. assert (TODO1: forall hs rhsv, hC hC_sval hs ~~> rhsv -> hsval_proj (hdata hs) = hsval_proj rhsv) by admit. - assert (TODO2: forall hs rhsv, hC hC_hlist_sval hs ~~> rhsv -> hsval_list_proj (hdata hs) = hsval_list_proj rhsv) + assert (TODO2: forall hs rhsv, hC hC_list_hsval hs ~~> rhsv -> hsval_list_proj (hdata hs) = hsval_list_proj rhsv) by admit. assert (TODO3: forall hs rhsv, hC hC_hsmem hs ~~> rhsv -> hsmem_proj (hdata hs) = hsmem_proj rhsv) by admit. -- cgit