aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--extraction/debug/Asmgen.ml87
-rw-r--r--mppa_k1c/Asm.v31
-rw-r--r--mppa_k1c/Asmgen.v29
-rw-r--r--mppa_k1c/Asmgenproof.v10
-rw-r--r--mppa_k1c/Asmgenproof1.v134
-rw-r--r--mppa_k1c/TargetPrinter.ml4
-rw-r--r--test/mppa/Makefile2
-rw-r--r--test/mppa/general/branchz.c12
-rw-r--r--test/mppa/general/branchzu.c12
-rw-r--r--test/mppa/general/output/branchz.exp1
-rw-r--r--test/mppa/general/output/branchzu.exp1
11 files changed, 205 insertions, 118 deletions
diff --git a/extraction/debug/Asmgen.ml b/extraction/debug/Asmgen.ml
index 2ccc5948..e8dfde13 100644
--- a/extraction/debug/Asmgen.ml
+++ b/extraction/debug/Asmgen.ml
@@ -1,79 +1,5 @@
(* Replace transl_op by this wrapper to print the op *)
-let thereal_transl_op op args res0 k =
- match op with
- | Ointconst n ->
- (match args with
- | [] ->
- (match ireg_of res0 with
- | OK x -> OK (loadimm32 x n k)
- | Error msg0 -> Error msg0)
- | _ :: _ ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[]))))))))))))))))))
- | Olongconst n ->
- (match args with
- | [] ->
- (match ireg_of res0 with
- | OK x -> OK (loadimm64 x n k)
- | Error msg0 -> Error msg0)
- | _ :: _ ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[]))))))))))))))))))
- | Oaddl ->
- (match args with
- | [] ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))
- | a1 :: l ->
- (match l with
- | [] ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))
- | a2 :: l0 ->
- (match l0 with
- | [] ->
- (match ireg_of res0 with
- | OK x ->
- (match ireg_of a1 with
- | OK x0 ->
- (match ireg_of a2 with
- | OK x1 -> OK ((Paddl (x, x0, x1)) :: k)
- | Error msg0 -> Error msg0)
- | Error msg0 -> Error msg0)
- | Error msg0 -> Error msg0)
- | _ :: _ ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[]))))))))))))))))))))
- | Oaddlimm n ->
- (match args with
- | [] ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))
- | a1 :: l ->
- (match l with
- | [] ->
- (match ireg_of res0 with
- | OK x ->
- (match ireg_of a1 with
- | OK x0 -> OK (addimm64 x x0 n k)
- | Error msg0 -> Error msg0)
- | Error msg0 -> Error msg0)
- | _ :: _ ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))))
- | _ ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('o'::('p'::[])))))))))))))))))
-
let transl_op op args res0 k =
match op with
| Omove -> (Printf.eprintf "Omove\n"; thereal_transl_op op args res0 k)
@@ -166,19 +92,6 @@ let transl_op op args res0 k =
| Ocmp _ -> (Printf.eprintf "Ocmp _\n"; thereal_transl_op op args res0 k)
| _ -> (Printf.eprintf "_\n"; thereal_transl_op op args res0 k)
-let thereal_transl_instr f i _ k =
- match i with
- | Mop (op, args, res0) -> transl_op op args res0 k
- | Mbuiltin (ef, args, res0) ->
- OK ((Pbuiltin (ef, (map (map_builtin_arg preg_of) args),
- (map_builtin_res preg_of res0))) :: k)
- | Mlabel lbl -> OK ((Plabel lbl) :: k)
- | Mreturn -> OK (make_epilogue f (Pret :: k))
- | _ ->
- Error
- (msg
- ('A'::('s'::('m'::('g'::('e'::('n'::('.'::('t'::('r'::('a'::('n'::('s'::('l'::('_'::('i'::('n'::('s'::('t'::('r'::[]))))))))))))))))))))
-
let transl_instr f i x k =
match i with
| Mgetstack _ -> (Printf.eprintf "Mgetstack\n"; thereal_transl_instr f i x k)
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index d19f9340..060cffd5 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -105,11 +105,11 @@ Inductive btest: Type :=
| BTeven (**r Even (LSB Clear) *)
*)| BTwnez (**r Word Not Equal to Zero *)
| BTweqz (**r Word Equal to Zero *)
-(*| BTwltz (**r Word Less Than Zero *)
+ | BTwltz (**r Word Less Than Zero *)
| BTwgez (**r Word Greater Than or Equal to Zero *)
| BTwlez (**r Word Less Than or Equal to Zero *)
| BTwgtz (**r Word Greater Than Zero *)
-*).
+ .
Inductive itest: Type :=
| ITne (**r Not Equal *)
@@ -582,6 +582,27 @@ Definition itest_for_cmp (c: comparison) (s: signedness) :=
| Cgt, Unsigned => ITgtu
end.
+(* CoMParing Signed Words to Zero *)
+Definition btest_for_cmpswz (c: comparison) :=
+ match c with
+ | Cne => BTwnez
+ | Ceq => BTweqz
+ | Clt => BTwltz
+ | Cge => BTwgez
+ | Cle => BTwlez
+ | Cgt => BTwgtz
+ end.
+
+Definition cmp_for_btest (bt: btest) :=
+ match bt with
+ | BTwnez => Some Cne
+ | BTweqz => Some Ceq
+ | BTwltz => Some Clt
+ | BTwgez => Some Cge
+ | BTwlez => Some Cle
+ | BTwgtz => Some Cgt
+ end.
+
(** Comparing integers *)
Definition compare_int (t: itest) (v1 v2: val) (m: mem): val :=
match t with
@@ -693,9 +714,9 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
(** Conditional branches *)
| Pcb bt r l =>
- match bt with
- | BTwnez => eval_branch f l rs m (Val.cmp_bool Cne rs##r (Vint (Int.repr 0)))
- | _ => Stuck
+ match cmp_for_btest bt with
+ | Some c => eval_branch f l rs m (Val.cmp_bool c rs##r (Vint (Int.repr 0)))
+ | None => Stuck
end
(*
(** Conditional branches, 32-bit comparisons *)
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 710bb32c..5ee86240 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -132,12 +132,33 @@ Definition transl_compl
(c: comparison) (s: signedness) (r1 r2: ireg) (lbl: label) (k: code) : list instruction :=
Pcompd (itest_for_cmp c s) RTMP r1 r2 :: Pcb BTwnez RTMP lbl :: k.
+Definition select_comp (n: int) (c: comparison) : option comparison :=
+ if Int.eq n Int.zero then
+ match c with
+ | Ceq => Some Ceq
+ | Cne => Some Cne
+ | _ => None
+ end
+ else
+ None
+ .
+
+Definition transl_opt_compuimm
+ (n: int) (c: comparison) (r1: ireg) (lbl: label) (k: code) : list instruction :=
+ match select_comp n c with
+ | Some Ceq => Pcb BTweqz r1 lbl :: k
+ | Some Cne => Pcb BTwnez r1 lbl :: k
+ | Some _ => nil (* Never happens *)
+ | None => loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k)
+ end
+ .
+
Definition transl_cbranch
(cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) :=
match cond, args with
| Ccompuimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
- OK (loadimm32 RTMP n (transl_comp c Unsigned r1 RTMP lbl k))
+ OK (transl_opt_compuimm n c r1 lbl k)
| Ccomp c, a1 :: a2 :: nil =>
do r1 <- ireg_of a1; do r2 <- ireg_of a2;
OK (transl_comp c Signed r1 r2 lbl k)
@@ -146,7 +167,11 @@ Definition transl_cbranch
OK (transl_comp c Unsigned r1 r2 lbl k)
| Ccompimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
- OK (loadimm32 RTMP n (transl_comp c Signed r1 RTMP lbl k))
+ OK (if Int.eq n Int.zero then
+ Pcb (btest_for_cmpswz c) r1 lbl :: k
+ else
+ loadimm32 RTMP n (transl_comp c Signed r1 RTMP lbl k)
+ )
| Ccompluimm c n, a1 :: nil =>
do r1 <- ireg_of a1;
OK (loadimm64 RTMP n (transl_compl c Unsigned r1 RTMP lbl k))
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 3dce24cf..e10290fd 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -185,9 +185,15 @@ Proof.
(* Ccompu *)
- unfold transl_comp; TailNoLabel.
(* Ccompimm *)
- - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
+ - destruct (Int.eq n Int.zero); TailNoLabel.
+ unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
(* Ccompuimm *)
- - unfold loadimm32. destruct (make_immed32 n); TailNoLabel. unfold transl_comp; TailNoLabel.
+ - unfold transl_opt_compuimm.
+ remember (select_comp n c0) as selcomp; destruct selcomp.
+ + destruct c; TailNoLabel; contradict Heqselcomp; unfold select_comp;
+ destruct (Int.eq n Int.zero); destruct c0; discriminate.
+ + unfold loadimm32;
+ destruct (make_immed32 n); TailNoLabel; unfold transl_comp; TailNoLabel.
(* Ccompl *)
- unfold transl_compl; TailNoLabel.
(* Ccomplu *)
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index fe037994..27b43c17 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -444,6 +444,77 @@ Proof.
rewrite H0. simpl; auto.
Qed.
+Lemma transl_opt_compuimm_correct:
+ forall n cmp r1 lbl k rs m b c,
+ select_comp n cmp = Some c ->
+ exists rs', exists insn,
+ exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m (insn :: k) rs' m
+ /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r)
+ /\ ( Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 (Vint n) = Some b ->
+ exec_instr ge fn insn rs' m = eval_branch fn lbl rs' m (Some b))
+ .
+Proof.
+ intros.
+ unfold transl_opt_compuimm; rewrite H; simpl.
+ remember c as c'.
+ destruct c'.
+ - (* c = Ceq *)
+ assert (Int.eq n Int.zero = true) as H'.
+ { remember (Int.eq n Int.zero) as termz. destruct termz; auto.
+ generalize H. unfold select_comp; rewrite <- Heqtermz; simpl.
+ discriminate. }
+ assert (n = (Int.repr 0)) as H0. {
+ destruct (Int.eq_dec n (Int.repr 0)) as [Ha|Ha]; auto.
+ generalize (Int.eq_false _ _ Ha). unfold Int.zero in H'.
+ rewrite H'. discriminate.
+ }
+ assert (Ceq = cmp). {
+ remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_comp;
+ rewrite H'; simpl; auto;
+ intros; contradict H; discriminate.
+ }
+
+ exists rs, (Pcb BTweqz r1 lbl).
+ split.
+ * constructor.
+ * split; auto. simpl. intros.
+ assert (Val.cmp_bool Ceq (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S.
+ { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }
+ auto;
+ unfold eval_branch. unfold getw. rewrite EVAL'S; auto.
+ - (* c = Cne *)
+ assert (Int.eq n Int.zero = true) as H'.
+ { remember (Int.eq n Int.zero) as termz. destruct termz; auto.
+ generalize H. unfold select_comp; rewrite <- Heqtermz; simpl.
+ discriminate. }
+ assert (n = (Int.repr 0)) as H0. {
+ destruct (Int.eq_dec n (Int.repr 0)) as [Ha|Ha]; auto.
+ generalize (Int.eq_false _ _ Ha). unfold Int.zero in H'.
+ rewrite H'. discriminate.
+ }
+ assert (Cne = cmp). {
+ remember cmp as c0'. destruct c0'; auto; generalize H; unfold select_comp;
+ rewrite H'; simpl; auto;
+ intros; contradict H; discriminate.
+ }
+ exists rs, (Pcb BTwnez r1 lbl).
+ split.
+ * constructor.
+ * split; auto. simpl. intros.
+ assert (Val.cmp_bool Cne (rs r1) (Vint (Int.repr 0)) = Some b) as EVAL'S.
+ { rewrite <- H2. rewrite <- H0. rewrite <- H1. auto. }
+ auto;
+ unfold eval_branch. unfold getw. rewrite EVAL'S; auto.
+ - (* c = Clt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+ destruct cmp; discriminate.
+ - (* c = Cle *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+ destruct cmp; discriminate.
+ - (* c = Cgt *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+ destruct cmp; discriminate.
+ - (* c = Cge *) contradict H; unfold select_comp; destruct (Int.eq n Int.zero);
+ destruct cmp; discriminate.
+Qed.
+
Lemma transl_cbranch_correct_1:
forall cond args lbl k c m ms b sp rs m',
transl_cbranch cond args lbl k = OK c ->
@@ -474,27 +545,49 @@ Proof.
+ constructor. eexact A.
+ split; auto. apply C; auto.
(* Ccompimm *)
-- exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
- exploit (transl_comp_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
- exists rs'2, (Pcb BTwnez GPR31 lbl).
- split.
- + constructor. apply exec_straight_trans
- with (c2 := (transl_comp c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
- eexact A. eexact A'.
- + split; auto.
- * apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen.
- * intros. rewrite B'; eauto with asmgen.
+- remember (Int.eq n Int.zero) as eqz.
+ destruct eqz.
+ + assert (n = (Int.repr 0)). {
+ destruct (Int.eq_dec n (Int.repr 0)) as [H|H]; auto.
+ generalize (Int.eq_false _ _ H). unfold Int.zero in Heqeqz.
+ rewrite <- Heqeqz. discriminate.
+ }
+ exists rs, (Pcb (btest_for_cmpswz c0) x lbl).
+ split.
+ * constructor.
+ * split; auto.
+ destruct c0; simpl; auto;
+ unfold eval_branch; rewrite <- H; unfold getw; rewrite EVAL'; auto.
+ + exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
+ exploit (transl_comp_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
+ exists rs'2, (Pcb BTwnez GPR31 lbl).
+ split.
+ * constructor. apply exec_straight_trans
+ with (c2 := (transl_comp c0 Signed x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+ eexact A. eexact A'.
+ * split; auto.
+ { apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen. }
+ { intros. rewrite B'; eauto with asmgen. }
(* Ccompuimm *)
-- exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
- exploit (transl_compu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
- exists rs'2, (Pcb BTwnez GPR31 lbl).
- split.
- + constructor. apply exec_straight_trans
- with (c2 := (transl_comp c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
- eexact A. eexact A'.
- + split; auto.
- * apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen.
- * intros. rewrite B'; eauto with asmgen.
+- remember (select_comp n c0) as selcomp.
+ destruct selcomp.
+ + exploit (transl_opt_compuimm_correct n c0 x lbl k). apply eq_sym. apply Heqselcomp.
+ intros (rs' & i & A & B & C).
+ exists rs', i.
+ split.
+ * apply A.
+ * split; auto. apply C. apply EVAL'.
+ + unfold transl_opt_compuimm. rewrite <- Heqselcomp; simpl.
+ exploit (loadimm32_correct GPR31 n); eauto. intros (rs' & A & B & C).
+ exploit (transl_compu_correct c0 x GPR31 lbl); eauto. intros (rs'2 & A' & B' & C').
+ exists rs'2, (Pcb BTwnez GPR31 lbl).
+ split.
+ * constructor. apply exec_straight_trans
+ with (c2 := (transl_comp c0 Unsigned x GPR31 lbl k)) (rs2 := rs') (m2 := m').
+ eexact A. eexact A'.
+ * split; auto.
+ { apply C'; auto. unfold getw. rewrite B, C; eauto with asmgen. }
+ { intros. rewrite B'; eauto with asmgen. }
(* Ccompl *)
- exploit (transl_compl_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C).
exists rs', (Pcb BTwnez GPR31 lbl).
@@ -531,7 +624,6 @@ Proof.
* intros. rewrite B'; eauto with asmgen.
Qed.
-
Lemma transl_cbranch_correct_true:
forall cond args lbl k c m ms sp rs m',
transl_cbranch cond args lbl k = OK c ->
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index ac6f8f1b..72f6e12a 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -177,6 +177,10 @@ module Target : TARGET =
let bcond_name = function
| BTwnez -> "wnez"
| BTweqz -> "weqz"
+ | BTwltz -> "wltz"
+ | BTwgez -> "wgez"
+ | BTwlez -> "wlez"
+ | BTwgtz -> "wgtz"
let bcond oc c = fprintf oc "%s" (bcond_name c)
diff --git a/test/mppa/Makefile b/test/mppa/Makefile
index 60433f03..36bd49bc 100644
--- a/test/mppa/Makefile
+++ b/test/mppa/Makefile
@@ -1,5 +1,5 @@
DIR=general
-TESTNAMES=simple call branch for forvar forvarl
+TESTNAMES=simple call branch for forvar forvarl branchz branchzu
TESTS=$(addprefix $(DIR)/,$(TESTNAMES))
ELF=$(addsuffix .bin,$(TESTS))
diff --git a/test/mppa/general/branchz.c b/test/mppa/general/branchz.c
new file mode 100644
index 00000000..5e3226d5
--- /dev/null
+++ b/test/mppa/general/branchz.c
@@ -0,0 +1,12 @@
+int main(void){
+ int a=1;
+ int b;
+
+ if(a==0){
+ b = a+4;
+ } else {
+ b = a+2;
+ }
+
+ return b;
+}
diff --git a/test/mppa/general/branchzu.c b/test/mppa/general/branchzu.c
new file mode 100644
index 00000000..0ff25763
--- /dev/null
+++ b/test/mppa/general/branchzu.c
@@ -0,0 +1,12 @@
+int main(void){
+ int a=1;
+ int b;
+
+ if(!a){
+ b = a+4;
+ } else {
+ b = a+2;
+ }
+
+ return b;
+}
diff --git a/test/mppa/general/output/branchz.exp b/test/mppa/general/output/branchz.exp
new file mode 100644
index 00000000..00750edc
--- /dev/null
+++ b/test/mppa/general/output/branchz.exp
@@ -0,0 +1 @@
+3
diff --git a/test/mppa/general/output/branchzu.exp b/test/mppa/general/output/branchzu.exp
new file mode 100644
index 00000000..00750edc
--- /dev/null
+++ b/test/mppa/general/output/branchzu.exp
@@ -0,0 +1 @@
+3
generated by cgit (git 2.34.1) at 2024-06-02 20:15:59 +0000