smart constructors with hash-consing

1 files changed, 144 insertions, 1 deletions

diff --git a/kvx/lib/RTLpathSE_impl_junk.v b/kvx/lib/RTLpathSE_impl_junk.v
index 8ae21a2d..dd8e80d7 100644
--- a/kvx/lib/RTLpathSE_impl_junk.v
+++ b/kvx/lib/RTLpathSE_impl_junk.v
@@ -19,9 +19,146 @@ Require Export Impure.ImpHCons.
 Export Notations.
 Import HConsing.
 
+Local Open Scope impure.
+
+Import ListNotations.
+Local Open Scope list_scope.
+
+(** * Refinement 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 *)
+with hsmem :=
+  | HSinit (hid:hashcode)
+  | HSstore (hsm: hsmem) (chunk:memory_chunk) (addr:addressing) (hlsv:hlist_sval) (srce: hsval) (hid:hashcode).
+
+Scheme hsval_mut := Induction for hsval Sort Prop
+with hlist_sval_mut := Induction for hlist_sval Sort Prop
+with hsmem_mut := Induction for hsmem Sort Prop.
+
+Definition hsval_get_hid (hsv: hsval): hashcode :=
+  match hsv with
+  | HSinput _ hid => hid
+  | HSop _ _ _ hid => hid
+  | HSload _ _ _ _ _ hid => hid
+  end.
+
+Definition hlist_sval_get_hid (hlsv: hlist_sval): hashcode :=
+  match hlsv with
+  | HSnil hid => hid
+  | HScons _ _ hid => hid
+  end.
+
+Definition hsmem_get_hid (hsm: hsmem ): hashcode :=
+  match hsm with
+  | HSinit hid => hid
+  | HSstore _ _ _ _ _ hid => hid
+  end.
+
+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
+  end.
+
+Definition hlist_sval_set_hid (hlsv: hlist_sval) (hid: hashcode): hlist_sval :=
+  match hlsv with
+  | HSnil _ => HSnil hid
+  | HScons hsv hlsv _ => HScons hsv hlsv hid
+  end.
+
+Definition hsmem_get_sid (hsm: hsmem ) (hid: hashcode): hsmem :=
+  match hsm with
+  | HSinit _ => HSinit hid
+  | HSstore hsm chunk addr hlsv srce _ => HSstore hsm chunk addr hlsv srce hid
+  end.
+
+
+Section CanonBuilding.
+
+Variable hC_hsval: hashinfo hsval -> ?? hsval.
+(*Hypothesis hC_hsval_correct: TODO *)
+
+Variable hC_hlist_sval: hashinfo hlist_sval -> ?? hlist_sval.
+(*Hypothesis hC_hlist_sval_correct: TODO *)
+
+Variable hC_hsmem: hashinfo hsmem -> ?? hsmem.
+(*Hypothesis hC_hsval_correct: TODO *)
+
+(* First, we wrap constructors for hashed values !*)
+
+Definition hSinput_hcodes (r: reg) :=
+   DO hc <~ hash 1;;
+   DO hv <~ hash r;;
+   RET [hc;hv].
+Extraction Inline hSinput_hcodes.
+
+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) :=
+   DO hc <~ hash 2;;
+   DO hv <~ hash op;;
+   RET [hc;hv;hlist_sval_get_hid hlsv; 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 hSload_hcodes (hsm: hsmem) (trap: trapping_mode) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval):=
+   DO hc <~ hash 3;;
+   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].
+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 hSTnil (_: unit): ?? hlist_sval :=
+   hC_hlist_sval {| hdata:=HSnil unknown_hid; hcodes := nil |}.
+
+Definition hSTcons (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 hSinit (_: unit): ?? hsmem :=
+   hC_hsmem {| hdata:=HSinit unknown_hid; hcodes := nil |}.
+
+Definition hSstore_hcodes (hsm: hsmem) (chunk: memory_chunk) (addr:addressing) (hlsv:hlist_sval) (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].
+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 |}.
+
+
+
 
 (*
-(** * TODO: refine symbolic values/symbolic memories with hash-consed symbolic values *)
+
+Fixpoint list_sval_inj (l: list sval): list_sval :=
+  match l with
+  | nil => Snil
+  | v::l => Scons v (list_sval_inj l)
+  end.
+
 
 (** * Implementation of local symbolic internal states 
 TODO: use refined symbolic values instead of those from RTLpathSE_theory.
@@ -211,6 +348,12 @@ Definition hsexec (f: function) (pc:node): option hsstate :=
        | None => {| hinternal := hst; hfinal := hsexec_final i hst.(hsi_local) |}
        end).
 
+
+*)
+
+End CanonBuilding.
+
+(*
 (** * The simulation test of concrete symbolic execution *)
 
 (* TODO - generalize it with a list of registers to test ? *)