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

some bugfix

parent 80db8e4b
...@@ -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
...@@ -436,12 +436,12 @@ let expanse (sb : superblock) code pm = ...@@ -436,12 +436,12 @@ let expanse (sb : superblock) code pm =
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 [];
...@@ -511,7 +511,7 @@ let expanse (sb : superblock) code pm = ...@@ -511,7 +511,7 @@ let expanse (sb : superblock) code pm =
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; 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
......
...@@ -373,14 +373,14 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args ...@@ -373,14 +373,14 @@ 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)*)
(*| (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
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)
| (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
...@@ -388,7 +388,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args ...@@ -388,7 +388,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in let cond := transl_cbranch_int32s c (make_optR0 true is_inv) in
Some (cond, lhsv) Some (cond, lhsv)
else else
let hvs := loadimm32 n in let hvs := loadimm32 hv1 n false in
let lhsv := make_lhsv_cmp is_inv hv1 hvs in let lhsv := make_lhsv_cmp is_inv hv1 hvs 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
Some (cond, lhsv)) Some (cond, lhsv))
...@@ -400,7 +400,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args ...@@ -400,7 +400,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in let cond := transl_cbranch_int32u c (make_optR0 true is_inv) in
Some (cond, lhsv) Some (cond, lhsv)
else else
let hvs := loadimm32 n in let hvs := loadimm32 hv1 n false in
let lhsv := make_lhsv_cmp is_inv hv1 hvs in let lhsv := make_lhsv_cmp is_inv hv1 hvs 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
Some (cond, lhsv)) Some (cond, lhsv))
...@@ -426,7 +426,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args ...@@ -426,7 +426,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in let cond := transl_cbranch_int64s c (make_optR0 true is_inv) in
Some (cond, lhsv) Some (cond, lhsv)
else else
let hvs := loadimm64 n in let hvs := loadimm64 hv1 n in
let lhsv := make_lhsv_cmp is_inv hv1 hvs in let lhsv := make_lhsv_cmp is_inv hv1 hvs in
let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in let cond := transl_cbranch_int64s c (make_optR0 false is_inv) in
Some (cond, lhsv)) Some (cond, lhsv))
...@@ -438,7 +438,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args ...@@ -438,7 +438,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in let cond := transl_cbranch_int64u c (make_optR0 true is_inv) in
Some (cond, lhsv) Some (cond, lhsv)
else else
let hvs := loadimm64 n in let hvs := loadimm64 hv1 n in
let lhsv := make_lhsv_cmp is_inv hv1 hvs in let lhsv := make_lhsv_cmp is_inv hv1 hvs in
let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in let cond := transl_cbranch_int64u c (make_optR0 false is_inv) in
Some (cond, lhsv)) Some (cond, lhsv))
...@@ -465,7 +465,7 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args ...@@ -465,7 +465,7 @@ 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 true cond_single c lhsv*) expanse_cbranch_fp true cond_single c lhsv*)
| _, _ => None | _, _ => None
end. end.
...@@ -1245,15 +1245,20 @@ Proof. ...@@ -1245,15 +1245,20 @@ Proof.
(*unfold target_cbranch_expanse, seval_condition; simpl. (*unfold target_cbranch_expanse, seval_condition; simpl.
intros H (LREF & SREF & SREG & SMEM) ?. intros H (LREF & SREF & SREG & SMEM) ?.
destruct c; try congruence. destruct c; try congruence.
all: all:
repeat (destruct l; simpl in H; try congruence); repeat (destruct l; simpl in H; try congruence).
destruct c; inv H; simpl; inv H; simpl.
erewrite !fsi_sreg_get_correct; eauto; try erewrite !fsi_sreg_get_correct; eauto.
- simpl.
destruct c; inv H; simpl.
try erewrite !fsi_sreg_get_correct; eauto;
try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence); try (destruct (seval_sval ge sp (si_sreg st r) rs0 m0) eqn:OKv1; try congruence);
try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence); try (destruct (seval_sval ge sp (si_sreg st r0) rs0 m0) eqn:OKv2; try congruence);
try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence). try (destruct (seval_smem ge sp (si_smem st) rs0 m0) eqn:OKmem; try congruence).
try destruct (Int.eq n Int.zero) eqn: EQIMM;
try apply Int.same_if_eq in EQIMM;
all: all:
try replace (Cle) with (swap_comparison Cge) by auto; try replace (Cle) with (swap_comparison Cge) by auto;
try replace (Clt) with (swap_comparison Cgt) by auto; try replace (Clt) with (swap_comparison Cgt) by auto;
......
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