Starting symbolic execution implementation

1 files changed, 314 insertions, 0 deletions

diff --git a/scheduling/BTL_SEimpl.v b/scheduling/BTL_SEimpl.v
new file mode 100644
index 00000000..5c974efd
--- /dev/null
+++ b/scheduling/BTL_SEimpl.v
@@ -0,0 +1,314 @@
+Require Import AST Maps.
+Require Import Op Registers.
+Require Import RTL BTL.
+Require Import BTL_SEsimuref BTL_SEtheory OptionMonad.
+
+Require Import Impure.ImpHCons.
+Import Notations.
+Import HConsing.
+
+Local Open Scope option_monad_scope.
+Local Open Scope impure.
+
+Import ListNotations.
+Local Open Scope list_scope.
+
+(** Notations to make lemmas more readable *)
+Notation "'sval_refines' ctx sv1 sv2" := (eval_sval ctx sv1 = eval_sval ctx sv2)
+  (only parsing, at level 0, ctx at next level, sv1 at next level, sv2 at next level): hse.
+
+Local Open Scope hse.
+
+Notation "'list_sval_refines' ctx lsv1 lsv2" := (eval_list_sval ctx lsv1 = eval_list_sval ctx lsv2)
+  (only parsing, at level 0, ctx at next level, lsv1 at next level, lsv2 at next level): hse.
+
+Notation "'smem_refines' ctx sm1 sm2" := (eval_smem ctx sm1 = eval_smem ctx sm2)
+  (only parsing, at level 0, ctx at next level, sm1 at next level, sm2 at next level): hse.
+
+(** Debug printer *)
+Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := RET tt. (* TO REMOVE DEBUG INFO *)
+(*Definition XDEBUG {A} (x:A) (k: A -> ?? pstring): ?? unit := DO s <~ k x;; println ("DEBUG simu_check:" +; s). (* TO INSERT DEBUG INFO *)*)
+
+Definition DEBUG (s: pstring): ?? unit := XDEBUG tt (fun _ => RET s).
+
+(** * Implementation of Data-structure use in Hash-consing *)
+
+Definition sval_get_hid (sv: sval): hashcode :=
+  match sv with
+  | Sundef hid => hid
+  | Sinput _ hid => hid
+  | Sop _ _ hid => hid
+  | Sload _ _ _ _ _ hid => hid
+  end.
+
+Definition list_sval_get_hid (lsv: list_sval): hashcode :=
+  match lsv with
+  | Snil hid => hid
+  | Scons _ _ hid => hid
+  end.
+
+Definition smem_get_hid (sm: smem): hashcode :=
+  match sm with
+  | Sinit hid => hid
+  | Sstore _ _ _ _ _ hid => hid
+  end.
+
+Definition sval_set_hid (sv: sval) (hid: hashcode): sval :=
+  match sv with
+  | Sundef _ => Sundef hid
+  | Sinput r _ => Sinput r hid
+  | Sop o lsv _ => Sop o lsv hid
+  | Sload sm trap chunk addr lsv _ => Sload sm trap chunk addr lsv hid
+  end.
+
+Definition list_sval_set_hid (lsv: list_sval) (hid: hashcode): list_sval :=
+  match lsv with
+  | Snil _ => Snil hid
+  | Scons sv lsv _ => Scons sv lsv hid
+  end.
+
+Definition smem_set_hid (sm: smem) (hid: hashcode): smem :=
+  match sm with
+  | Sinit _ => Sinit hid
+  | Sstore sm chunk addr lsv srce _ => Sstore sm chunk addr lsv srce hid
+  end.
+
+(** * Implementation of symbolic execution *)
+Section CanonBuilding.
+
+Variable hC_sval: hashinfo sval -> ?? sval.
+
+Hypothesis hC_sval_correct: forall s,
+  WHEN hC_sval s ~> s' THEN forall ctx,
+    sval_refines ctx (hdata s) s'.
+
+Variable hC_list_sval: hashinfo list_sval -> ?? list_sval.
+Hypothesis hC_list_sval_correct: forall lh,
+  WHEN hC_list_sval lh ~> lh' THEN forall ctx,
+    list_sval_refines ctx (hdata lh) lh'.
+
+Variable hC_smem: hashinfo smem -> ?? smem.
+Hypothesis hC_smem_correct: forall hm,
+  WHEN hC_smem hm ~> hm' THEN forall ctx,
+    smem_refines ctx (hdata hm) hm'.
+
+(* First, we wrap constructors for hashed values !*)
+
+Definition reg_hcode := 1.
+Definition op_hcode := 2.
+Definition load_hcode := 3.
+Definition undef_code := 4.
+
+Definition hSinput_hcodes (r: reg) :=
+   DO hc <~ hash reg_hcode;;
+   DO hv <~ hash r;;
+   RET [hc;hv].
+Extraction Inline hSinput_hcodes.
+
+Definition hSinput (r:reg): ?? sval :=
+   DO hv <~ hSinput_hcodes r;;
+   hC_sval {| hdata:=Sinput r unknown_hid; hcodes :=hv; |}.
+
+Lemma hSinput_correct r:
+  WHEN hSinput r ~> hv THEN forall ctx,
+    sval_refines ctx hv (Sinput r unknown_hid).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hSinput.
+Local Hint Resolve hSinput_correct: wlp.
+
+Definition hSop_hcodes (op:operation) (lsv: list_sval) :=
+   DO hc <~ hash op_hcode;;
+   DO hv <~ hash op;;
+   RET [hc;hv;list_sval_get_hid lsv].
+Extraction Inline hSop_hcodes.
+
+Definition hSop (op:operation) (lsv: list_sval): ?? sval :=
+   DO hv <~ hSop_hcodes op lsv;;
+   hC_sval {| hdata:=Sop op lsv unknown_hid; hcodes :=hv |}.
+
+Lemma hSop_fSop_correct op lsv:
+  WHEN hSop op lsv ~> hv THEN forall ctx,
+    sval_refines ctx hv (fSop op lsv).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hSop.
+Local Hint Resolve hSop_fSop_correct: wlp_raw.
+
+Lemma hSop_correct op lsv1:
+  WHEN hSop op lsv1 ~> hv THEN forall ctx lsv2
+   (LR: list_sval_refines ctx lsv1 lsv2),
+   sval_refines ctx hv (Sop op lsv2 unknown_hid).
+Proof.
+  wlp_xsimplify ltac:(intuition eauto with wlp wlp_raw).
+  rewrite <- LR. erewrite H; eauto.
+Qed.
+Local Hint Resolve hSop_correct: wlp.
+
+Definition hSload_hcodes (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval):=
+   DO hc <~ hash load_hcode;;
+   DO hv1 <~ hash trap;;
+   DO hv2 <~ hash chunk;;
+   DO hv3 <~ hash addr;;
+   RET [hc; smem_get_hid sm; hv1; hv2; hv3; list_sval_get_hid lsv].
+Extraction Inline hSload_hcodes.
+
+Definition hSload (sm: smem) (trap: trapping_mode) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval): ?? sval :=
+   DO hv <~ hSload_hcodes sm trap chunk addr lsv;;
+   hC_sval {| hdata := Sload sm trap chunk addr lsv unknown_hid; hcodes := hv |}.
+
+Lemma hSload_correct sm1 trap chunk addr lsv1:
+  WHEN hSload sm1 trap chunk addr lsv1 ~> hv THEN forall ctx lsv2 sm2 hid
+    (LR: list_sval_refines ctx lsv1 lsv2)
+    (MR: smem_refines ctx sm1 sm2),
+    sval_refines ctx hv (Sload sm2 trap chunk addr lsv2 hid).
+Proof.
+  wlp_simplify.
+  rewrite <- LR, <- MR.
+  auto.
+Qed.
+Global Opaque hSload.
+Local Hint Resolve hSload_correct: wlp.
+
+Definition hSundef_hcodes :=
+   DO hc <~ hash undef_code;;
+   RET [hc].
+Extraction Inline hSundef_hcodes.
+
+Definition hSundef : ?? sval :=
+   DO hv <~ hSundef_hcodes;;
+   hC_sval {| hdata:=Sundef unknown_hid; hcodes :=hv; |}.
+
+Lemma hSundef_correct:
+  WHEN hSundef ~> hv THEN forall ctx,
+    sval_refines ctx hv (Sundef unknown_hid).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hSundef.
+Local Hint Resolve hSundef_correct: wlp.
+
+Definition hSnil (_: unit): ?? list_sval :=
+   hC_list_sval {| hdata := Snil unknown_hid; hcodes := nil |}.
+
+Lemma hSnil_correct:
+  WHEN hSnil() ~> hv THEN forall ctx,
+    list_sval_refines ctx hv (Snil unknown_hid).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hSnil.
+Local Hint Resolve hSnil_correct: wlp.
+
+Definition hScons (sv: sval) (lsv: list_sval): ?? list_sval :=
+   hC_list_sval {| hdata := Scons sv lsv unknown_hid; hcodes := [sval_get_hid sv; list_sval_get_hid lsv] |}.
+
+Lemma hScons_correct sv1 lsv1:
+  WHEN hScons sv1 lsv1 ~> lsv1' THEN forall ctx sv2 lsv2
+    (VR: sval_refines ctx sv1 sv2)
+    (LR: list_sval_refines ctx lsv1 lsv2),
+    list_sval_refines ctx lsv1' (Scons sv2 lsv2 unknown_hid).
+Proof.
+  wlp_simplify.
+  rewrite <- VR, <- LR.
+  auto.
+Qed.
+Global Opaque hScons.
+Local Hint Resolve hScons_correct: wlp.
+
+Definition hSinit (_: unit): ?? smem :=
+   hC_smem {| hdata := Sinit unknown_hid; hcodes := nil |}.
+
+Lemma hSinit_correct:
+  WHEN hSinit() ~> hm THEN forall ctx,
+    smem_refines ctx hm (Sinit unknown_hid).
+Proof.
+  wlp_simplify.
+Qed.
+Global Opaque hSinit.
+Local Hint Resolve hSinit_correct: wlp.
+
+Definition hSstore_hcodes (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval):=
+   DO hv1 <~ hash chunk;;
+   DO hv2 <~ hash addr;;
+   RET [smem_get_hid sm; hv1; hv2; list_sval_get_hid lsv; sval_get_hid srce].
+Extraction Inline hSstore_hcodes.
+
+Definition hSstore (sm: smem) (chunk: memory_chunk) (addr: addressing) (lsv: list_sval) (srce: sval): ?? smem :=
+   DO hv <~ hSstore_hcodes sm chunk addr lsv srce;;
+   hC_smem {| hdata := Sstore sm chunk addr lsv srce unknown_hid; hcodes := hv |}.
+
+Lemma hSstore_correct sm1 chunk addr lsv1 sv1:
+  WHEN hSstore sm1 chunk addr lsv1 sv1 ~> sm1' THEN forall ctx lsv2 sm2 sv2
+    (LR: list_sval_refines ctx lsv1 lsv2)
+    (MR: smem_refines ctx sm1 sm2)
+    (VR: sval_refines ctx sv1 sv2),
+    smem_refines ctx sm1' (Sstore sm2 chunk addr lsv2 sv2 unknown_hid).
+Proof.
+  wlp_simplify.
+  rewrite <- LR, <- MR, <- VR.
+  auto.
+Qed.
+Global Opaque hSstore.
+Local Hint Resolve hSstore_correct: wlp.
+
+Definition hris_sreg_eval ctx hris r := eval_sval ctx (ris_sreg_get hris r).
+
+Definition hris_sreg_get (hris: ristate) r: ?? sval :=
+   match PTree.get r hris with
+   | None => if ris_input_init hris then hSinput r else hSundef
+   | Some sv => RET sv
+   end.
+Coercion hris_sreg_get: ristate >-> Funclass.
+
+Lemma hris_sreg_get_correct hris r:
+  WHEN hris_sreg_get hris r ~> sv THEN forall ctx (f: reg -> sval)
+  (RR: forall r, hris_sreg_eval ctx hris r = eval_sval ctx (f r)),
+  sval_refines ctx sv (f r).
+Proof.
+  unfold hris_sreg_eval, ris_sreg_get. wlp_simplify; rewrite <- RR; rewrite H; auto;
+  rewrite H0, H1; simpl; auto.
+Qed.
+Global Opaque hris_sreg_get.
+Local Hint Resolve hris_sreg_get_correct: wlp.
+
+Definition some_or_fail {A} (o: option A) (msg: pstring): ?? A :=
+  match o with
+  | Some x => RET x
+  | None => FAILWITH msg
+  end.
+
+Definition hris_init: ?? ristate
+  := DO hm <~ hSinit ();;
+     RET {| ris_smem := hm; ris_input_init := true; ok_rsval := nil; ris_sreg := PTree.empty _ |}.
+
+Lemma ris_init_correct:
+  WHEN hris_init ~> hris THEN
+  forall ctx, ris_refines ctx hris sis_init.
+Proof.
+  unfold hris_init, sis_init; wlp_simplify.
+  econstructor; simpl in *; eauto.
+  + split; destruct 1; econstructor; simpl in *;
+    try rewrite H; try congruence; trivial.
+  + destruct 1; simpl in *. unfold ris_sreg_get; simpl.
+    intros; rewrite PTree.gempty; eauto.
+Qed.
+
+(*
+Definition hrexec f ib := hrexec_rec f ib hris_init (fun _ => Rabort).
+
+Definition hsexec (f: function) (pc:node): ?? ristate :=
+  DO path <~ some_or_fail ((fn_code f)!pc) "hsexec.internal_error.1";;
+  DO hinit <~ init_ristate;;
+  DO hst <~ hsiexec_path path.(psize) f hinit;;
+  DO i <~ some_or_fail ((fn_code f)!(hst.(hsi_pc))) "hsexec.internal_error.2";;
+  DO ohst <~ hsiexec_inst i hst;;
+  match ohst with
+  | Some hst' => RET {| hinternal := hst'; hfinal := HSnone |}
+  | None => DO hsvf <~ hsexec_final i hst.(hsi_local);;
+            RET {| hinternal := hst; hfinal := hsvf |}
+   end.*)
+
+End CanonBuilding.