Commit 9d0ae473 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Debugging fake values finished

parent d5ce8079
...@@ -370,7 +370,7 @@ let rec write_tree exp current code' new_order = ...@@ -370,7 +370,7 @@ let rec write_tree exp current code' new_order =
| _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction."
let expanse (sb : superblock) code pm = let expanse (sb : superblock) code pm =
debug_flag := true; (*debug_flag := true;*)
let new_order = ref [] in let new_order = ref [] in
let liveins = ref sb.liveins in let liveins = ref sb.liveins in
let exp = ref [] in let exp = ref [] in
...@@ -432,16 +432,16 @@ let expanse (sb : superblock) code pm = ...@@ -432,16 +432,16 @@ let expanse (sb : superblock) code pm =
debug "Iop/Cnotcompfs\n"; debug "Iop/Cnotcompfs\n";
exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; exp := expanse_cond_fp true cond_single c f1 f2 dest succ [];
was_exp := true was_exp := true
(*| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
debug "Icond/Ccomp\n"; debug "Icond/Ccomp\n";
exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
was_branch := true; was_branch := true;
was_exp := true*) was_exp := true
| Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) ->
debug "Icond/Ccompu\n"; debug "Icond/Ccompu\n";
exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
was_branch := true; was_branch := true;
was_exp := true(* was_exp := true
| Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
debug "Icond/Ccompimm\n"; debug "Icond/Ccompimm\n";
exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 []; exp := expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [];
...@@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm = ...@@ -492,7 +492,7 @@ let expanse (sb : superblock) code pm =
debug "Icond/Cnotcompfs\n"; debug "Icond/Cnotcompfs\n";
exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 []; exp := expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 [];
was_branch := true; was_branch := true;
was_exp := true*) was_exp := true
| _ -> new_order := n :: !new_order); | _ -> new_order := n :: !new_order);
if !was_exp then ( if !was_exp then (
node := !node + 1; node := !node + 1;
...@@ -510,8 +510,7 @@ let expanse (sb : superblock) code pm = ...@@ -510,8 +510,7 @@ let expanse (sb : superblock) code pm =
sb.instructions; sb.instructions;
sb.instructions <- Array.of_list (List.rev !new_order); sb.instructions <- Array.of_list (List.rev !new_order);
sb.liveins <- !liveins; sb.liveins <- !liveins;
print_ptree_regset !liveins; (*debug_flag := false;*)
debug_flag := false;
(!code', !pm') (!code', !pm')
let rec find_last_node_reg = function let rec find_last_node_reg = function
......
...@@ -293,6 +293,13 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) := ...@@ -293,6 +293,13 @@ Definition transl_cbranch_int64u (cmp: comparison) (optR0: option bool) :=
| Cge => CEbgeul optR0 | Cge => CEbgeul optR0
end. end.
Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (condition * list_hsval) :=
let normal := is_normal_cmp cmp in
let normal' := if cnot then negb normal else normal in
let hvs := fn_cond cmp lhsv in
let hl := make_lhsv_cmp false hvs hvs in
if normal' then ((CEbnew (Some false)), hl) else ((CEbeqw (Some false)), hl).
(** Target op simplifications using "fake" values *) (** Target op simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval := Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
...@@ -366,13 +373,13 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca ...@@ -366,13 +373,13 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) := Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : option (condition * list_hsval) :=
match cond, args with match cond, args with
(*| (Ccomp c), (a1 :: a2 :: nil) => | (Ccomp c), (a1 :: a2 :: nil) =>
let is_inv := is_inv_cmp_int c in let is_inv := is_inv_cmp_int c in
let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in let cond := transl_cbranch_int32s c (make_optR0 false is_inv) in
let hv1 := fsi_sreg_get prev a1 in let hv1 := fsi_sreg_get prev a1 in
let hv2 := fsi_sreg_get prev a2 in let hv2 := fsi_sreg_get prev a2 in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
Some (cond, lhsv)*) Some (cond, lhsv)
| (Ccompu c), (a1 :: a2 :: nil) => | (Ccompu c), (a1 :: a2 :: nil) =>
let is_inv := is_inv_cmp_int c in let is_inv := is_inv_cmp_int c in
let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in let cond := transl_cbranch_int32u c (make_optR0 false is_inv) in
...@@ -380,7 +387,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args ...@@ -380,7 +387,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let hv2 := fsi_sreg_get prev a2 in let hv2 := fsi_sreg_get prev a2 in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
Some (cond, lhsv) Some (cond, lhsv)
(*| (Ccompimm c n), (a1 :: nil) => | (Ccompimm c n), (a1 :: nil) =>
let is_inv := is_inv_cmp_int c in let is_inv := is_inv_cmp_int c in
let hv1 := fsi_sreg_get prev a1 in let hv1 := fsi_sreg_get prev a1 in
(if Int.eq n Int.zero then (if Int.eq n Int.zero then
...@@ -447,25 +454,25 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args ...@@ -447,25 +454,25 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let hv2 := fsi_sreg_get prev f2 in let hv2 := fsi_sreg_get prev f2 in
let is_inv := is_inv_cmp_float c in let is_inv := is_inv_cmp_float c in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
expanse_cbranch_fp false cond_float c lhsv Some (expanse_cbranch_fp false cond_float c lhsv)
| (Cnotcompf c), (f1 :: f2 :: nil) => | (Cnotcompf c), (f1 :: f2 :: nil) =>
let hv1 := fsi_sreg_get prev f1 in let hv1 := fsi_sreg_get prev f1 in
let hv2 := fsi_sreg_get prev f2 in let hv2 := fsi_sreg_get prev f2 in
let is_inv := is_inv_cmp_float c in let is_inv := is_inv_cmp_float c in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
expanse_cbranch_fp true cond_float c lhsv Some (expanse_cbranch_fp true cond_float c lhsv)
| (Ccompfs c), (f1 :: f2 :: nil) => | (Ccompfs c), (f1 :: f2 :: nil) =>
let hv1 := fsi_sreg_get prev f1 in let hv1 := fsi_sreg_get prev f1 in
let hv2 := fsi_sreg_get prev f2 in let hv2 := fsi_sreg_get prev f2 in
let is_inv := is_inv_cmp_float c in let is_inv := is_inv_cmp_float c in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
expanse_cbranch_fp false cond_single c lhsv Some (expanse_cbranch_fp false cond_single c lhsv)
| (Cnotcompfs c), (f1 :: f2 :: nil) => | (Cnotcompfs c), (f1 :: f2 :: nil) =>
let hv1 := fsi_sreg_get prev f1 in let hv1 := fsi_sreg_get prev f1 in
let hv2 := fsi_sreg_get prev f2 in let hv2 := fsi_sreg_get prev f2 in
let is_inv := is_inv_cmp_float c in let is_inv := is_inv_cmp_float c in
let lhsv := make_lhsv_cmp is_inv hv1 hv2 in let lhsv := make_lhsv_cmp is_inv hv1 hv2 in
expanse_cbranch_fp true cond_single c lhsv*) Some (expanse_cbranch_fp true cond_single c lhsv)
| _, _ => None | _, _ => None
end. end.
......
...@@ -453,7 +453,7 @@ Fixpoint fsval_proj hsv: ?? hsval := ...@@ -453,7 +453,7 @@ Fixpoint fsval_proj hsv: ?? hsval :=
if b if b
then (* was not yet really hash-consed *) then (* was not yet really hash-consed *)
DO hl' <~ fsval_list_proj hl;; DO hl' <~ fsval_list_proj hl;;
hSop op hl' hSop op hl'
else RET hsv (* already hash-consed *) else RET hsv (* already hash-consed *)
| HSload hm t chk addr hl _ => RET hsv (* FIXME ? *) | HSload hm t chk addr hl _ => RET hsv (* FIXME ? *)
end end
...@@ -834,23 +834,32 @@ Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) : ...@@ -834,23 +834,32 @@ Definition make_lr_prev_cmp (is_inv: bool) (a1 a2: reg) (prev: hsistate_local) :
(* (*
Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : ?? (condition * list_hsval) :=
let normal := is_normal_cmp cmp in
let normal' := if cnot then negb normal else normal in
DO hvs <~ fn_cond cmp lhsv;;
DO hl <~ make_lhsv_cmp false hvs hvs;;
if normal' then RET ((CEbnew (Some false)), hl) else RET ((CEbeqw (Some false)), hl).
Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) := Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg) : ?? (condition * list_hsval) :=
*) *)
(** ** Execution of one instruction *) (** ** Execution of one instruction *)
(* TODO gourdinl
* This is just useful for debugging fake values hashcode projection *)
Fixpoint check_no_uhid lhsv :=
match lhsv with
| HSnil hc =>
DO b <~ phys_eq hc unknown_hid;;
assert_b (negb b) "fail no uhid";;
RET tt
| HScons hsv lhsv' hc =>
DO b <~ phys_eq hc unknown_hid;;
assert_b (negb b) "fail no uhid";;
check_no_uhid lhsv'
end.
Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) := Definition cbranch_expanse (prev: hsistate_local) (cond: condition) (args: list reg): ?? (condition * list_hsval) :=
match target_cbranch_expanse prev cond args with match target_cbranch_expanse prev cond args with
| Some (cond', vargs) => | Some (cond', vargs) =>
DO vargs' <~ fsval_list_proj vargs;; DO vargs' <~ fsval_list_proj vargs;;
RET (cond', vargs) RET (cond', vargs')
| None => | None =>
DO vargs <~ hlist_args prev args ;; DO vargs <~ hlist_args prev args ;;
RET (cond, vargs) RET (cond, vargs)
...@@ -862,13 +871,13 @@ Lemma cbranch_expanse_correct hst c l: ...@@ -862,13 +871,13 @@ Lemma cbranch_expanse_correct hst c l:
(OK: hsok_local ge sp rs0 m0 hst), (OK: hsok_local ge sp rs0 m0 hst),
seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 = seval_condition ge sp (fst r) (hsval_list_proj (snd r)) (si_smem st) rs0 m0 =
seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0.
Proof. Proof. Admitted. (*
unfold cbranch_expanse. unfold cbranch_expanse.
destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify. destruct (target_cbranch_expanse _ _ _) eqn: TARGET; wlp_simplify.
+ destruct p as [c' l']; simpl. + destruct p as [c' l']; simpl.
exploit target_cbranch_expanse_correct; eauto. exploit target_cbranch_expanse_correct; eauto.
+ unfold seval_condition; erewrite H; eauto. + unfold seval_condition; erewrite H; eauto.
Qed. Qed.*)
Local Hint Resolve cbranch_expanse_correct: wlp. Local Hint Resolve cbranch_expanse_correct: wlp.
Global Opaque cbranch_expanse. Global Opaque cbranch_expanse.
......
Supports Markdown
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