aboutsummaryrefslogtreecommitdiffstats
path: root/riscV
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-04-06 23:37:22 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-04-06 23:37:22 +0200
commitdd4767e17235adb5de922626ed1fea15f4eb9e3b (patch)
tree37843b101add33cf6ea56e055ddae2df96c6dc67 /riscV
parentdf9aab806ae8d20393b56e4175e210ed6cff1ef1 (diff)
downloadcompcert-kvx-dd4767e17235adb5de922626ed1fea15f4eb9e3b.tar.gz
compcert-kvx-dd4767e17235adb5de922626ed1fea15f4eb9e3b.zip
Important commit on expansions' mini CSE, and a draft for addptrofs
Diffstat (limited to 'riscV')
-rw-r--r--riscV/Asm.v2
-rw-r--r--riscV/Asmgen.v58
-rw-r--r--riscV/Asmgenproof.v3
-rw-r--r--riscV/Asmgenproof1.v56
-rw-r--r--riscV/ExpansionOracle.ml1106
-rw-r--r--riscV/NeedOp.v6
-rw-r--r--riscV/Op.v296
-rw-r--r--riscV/PrintOp.ml17
-rw-r--r--riscV/RTLpathSE_simplify.v156
-rw-r--r--riscV/ValueAOp.v133
10 files changed, 1077 insertions, 756 deletions
diff --git a/riscV/Asm.v b/riscV/Asm.v
index 5d3518f2..a16f57b5 100644
--- a/riscV/Asm.v
+++ b/riscV/Asm.v
@@ -982,6 +982,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
end
| Pbuiltin ef args res =>
Stuck (**r treated specially below *)
+ | Pnop => Next (nextinstr rs) m (**r Pnop is used by an oracle during expansion *)
(** The following instructions and directives are not generated directly by Asmgen,
so we do not model them. *)
@@ -1002,7 +1003,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
| Pfmsubd _ _ _ _
| Pfnmaddd _ _ _ _
| Pfnmsubd _ _ _ _
- | Pnop
=> Stuck
end.
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 88d4f73f..ff5d1a6e 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -204,19 +204,23 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
| Cgt => (Pflts rd fs2 fs1, true)
| Cge => (Pfles rd fs2 fs1, true)
end.
-
+
+(** Functions to select a special register according to the op "oreg" argument from RTL *)
+
Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) :=
match optR with
| None => (r1, r2)
| Some X0_L => (X0, r1)
| Some X0_R => (r1, X0)
+ | Some SP_S => (X SP, r1)
end.
-Definition get_opimmR0 (rd: ireg) (opi: opimm) :=
- match opi with
- | OPimmADD i => Paddiw rd X0 i
- | OPimmADDL i => Paddil rd X0 i
- end.
+Definition get_oreg (optR: option oreg) (r: ireg0) :=
+ match optR with
+ | Some SP_S => X SP
+ | Some X0_L | Some X0_R => X0
+ | _ => r
+ end.
Definition transl_cbranch
(cond: condition) (args: list mreg) (lbl: label) (k: code) :=
@@ -785,9 +789,8 @@ Definition transl_op
| Ocmp cmp, _ =>
do rd <- ireg_of res;
transl_cond_op cmp rd args k
- | OEimmR0 opi, nil =>
- do rd <- ireg_of res;
- OK (get_opimmR0 rd opi :: k)
+
+ (* Instructions expanded in RTL *)
| OEseqw optR, a1 :: a2 :: nil =>
do rd <- ireg_of res;
do rs1 <- ireg_of a1;
@@ -839,10 +842,21 @@ Definition transl_op
| OEluiw n, nil =>
do rd <- ireg_of res;
OK (Pluiw rd n :: k)
- | OEaddiw n, a1 :: nil =>
+ | OEaddiw optR n, nil =>
do rd <- ireg_of res;
- do rs <- ireg_of a1;
+ let rs := get_oreg optR X0 in
OK (Paddiw rd rs n :: k)
+ | OEaddiw (Some SP_S) n, a1 :: nil =>
+ do rd <- ireg_of res;
+ do rs <- ireg_of a1;
+ if Int.eq n Int.zero then
+ OK (Paddw rd SP rs :: k)
+ else Error (msg "Asmgen.transl_op")
+ | OEaddiw optR n, a1 :: nil =>
+ do rd <- ireg_of res;
+ do rs <- ireg_of a1;
+ let rs' := get_oreg optR rs in
+ OK (Paddiw rd rs' n :: k)
| OEandiw n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
@@ -902,10 +916,21 @@ Definition transl_op
| OEluil n, nil =>
do rd <- ireg_of res;
OK (Pluil rd n :: k)
- | OEaddil n, a1 :: nil =>
+ | OEaddil optR n, nil =>
do rd <- ireg_of res;
- do rs <- ireg_of a1;
+ let rs := get_oreg optR X0 in
OK (Paddil rd rs n :: k)
+ | OEaddil (Some SP_S) n, a1 :: nil =>
+ do rd <- ireg_of res;
+ do rs <- ireg_of a1;
+ if Int64.eq n Int64.zero then
+ OK (Paddl rd SP rs :: k)
+ else Error (msg "Asmgen.transl_op")
+ | OEaddil optR n, a1 :: nil =>
+ do rd <- ireg_of res;
+ do rs <- ireg_of a1;
+ let rs' := get_oreg optR rs in
+ OK (Paddil rd rs' n :: k)
| OEandil n, a1 :: nil =>
do rd <- ireg_of res;
do rs <- ireg_of a1;
@@ -947,6 +972,13 @@ Definition transl_op
do r1 <- freg_of f1;
do r2 <- freg_of f2;
OK (Pfles rd r1 r2 :: k)
+ | OEmayundef _, a1 :: a2 :: nil =>
+ do rd <- ireg_of res;
+ do r2 <- ireg_of a2;
+ if ireg_eq rd r2 then
+ OK (Pnop :: k)
+ else
+ OK (Pmv rd r2 :: k)
| Obits_of_single, a1 :: nil =>
do rd <- ireg_of res; do rs <- freg_of a1;
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index 101bfa9c..bf9ede7f 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -308,7 +308,8 @@ Opaque Int.eq.
- apply opimm64_label; intros; exact I.
- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel.
- eapply transl_cond_op_label; eauto.
-- destruct opi; simpl; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
+- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
- destruct optR as [[]|]; simpl in *; TailNoLabel.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 1e17c4e2..cbe68577 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -529,31 +529,37 @@ Proof.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
@@ -591,31 +597,37 @@ Proof.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
- destruct optR as [[]|];
unfold apply_bin_oreg_ireg0, apply_bin_oreg in *;
unfold zero32, Op.zero32, zero64, Op.zero64 in *; inv EQ2;
+ try (destruct (rs x); simpl in EVAL'; discriminate; fail);
eexists; eexists; eauto; split; constructor;
simpl in *; try rewrite EVAL'; auto.
Qed.
@@ -1262,12 +1274,7 @@ Opaque Int.eq.
{ exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C).
exists rs'; split. eexact A. eauto with asmgen. }
(* Expanded instructions from RTL *)
- { unfold get_opimmR0; destruct opi; simpl;
- econstructor; split; try apply exec_straight_one; simpl; eauto;
- split; intros; Simpl.
- try rewrite Int.add_commut; auto.
- try rewrite Int64.add_commut; auto. }
- 7,8,9,16,17,18:
+ 8,9,17,18:
econstructor; split; try apply exec_straight_one; simpl; eauto;
split; intros; Simpl; try destruct (rs x0);
try rewrite Int64.add_commut;
@@ -1276,12 +1283,41 @@ Opaque Int.eq.
try rewrite Int.and_commut; auto;
try rewrite Int64.or_commut;
try rewrite Int.or_commut; auto.
- 1-12:
- destruct optR as [[]|]; unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; inv EQ3;
+ 1-14:
+ destruct optR as [[]|]; try discriminate;
+ try (ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl);
+ unfold apply_bin_oreg_ireg0, apply_bin_oreg in *; try inv EQ3; try inv EQ2;
+ try destruct (Int.eq _ _) eqn:A; try inv H0;
+ try destruct (Int64.eq _ _) eqn:A; try inv H1;
econstructor; split; try apply exec_straight_one; simpl; eauto;
split; intros; Simpl;
- destruct (rs x0); auto;
- destruct (rs x1); auto.
+ try apply Int.same_if_eq in A; subst;
+ try apply Int64.same_if_eq in A; subst;
+ unfold get_sp;
+ try destruct (rs x0); auto;
+ try destruct (rs x1); auto;
+ try destruct (rs X2); auto;
+ try destruct Archi.ptr64 eqn:B;
+ try fold (Val.add (Vint Int.zero) (get_sp (rs X2)));
+ try fold (Val.addl (Vlong Int64.zero) (get_sp (rs X2)));
+ try rewrite Val.add_commut; auto;
+ try rewrite Val.addl_commut; auto;
+ try rewrite Int.add_commut; auto;
+ try rewrite Int64.add_commut; auto;
+ replace (Ptrofs.of_int Int.zero) with (Ptrofs.zero) by auto;
+ replace (Ptrofs.of_int64 Int64.zero) with (Ptrofs.zero) by auto;
+ try rewrite Ptrofs.add_zero; auto.
+ (* mayundef *)
+ { destruct (ireg_eq x x0); inv EQ2;
+ econstructor; split;
+ try apply exec_straight_one; simpl; eauto;
+ split; unfold eval_may_undef;
+ destruct mu eqn:EQMU; simpl; intros; Simpl; auto.
+ all:
+ destruct (rs (preg_of m0)) eqn:EQM0; simpl; auto;
+ destruct (rs x0); simpl; auto; Simpl;
+ try destruct (Int.ltu _ _); simpl;
+ Simpl; auto. }
(* select *)
{ econstructor; split. apply exec_straight_one. simpl; eauto. auto.
split; intros; Simpl.
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 16f1ee4b..e0c9b9b2 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -17,15 +17,19 @@ open Maps
open RTL
open Op
open Asmgen
-open DebugPrint
open RTLpath
open! Integers
open Camlcoq
open Option
+open AST
+open Printf
-type sop = Sop of operation * P.t list
+(** Mini CSE (a dynamic numbering is applied during expansion.
+ The CSE algorithm is inspired by the "static" one used in backend/CSE.v *)
-type sval = Si of RTL.instruction | Sr of P.t
+let exp_debug = false
+
+(** Managing virtual registers and node index *)
let reg = ref 1
@@ -45,6 +49,181 @@ let n2pi () =
node := !node + 1;
n2p ()
+(** Below are the types for rhs and equations *)
+
+type rhs = Sop of operation * int list | Smove
+
+type seq = Seq of int * rhs
+
+(** This is a mini abstraction to have a simpler representation during expansion
+ - Snop will be converted to Inop
+ - (Sr r) is inserted if the value was found in register r
+ - (Sexp dest rhs args succ) represent an instruction
+ (succesor may not be defined at this point, hence the use of type option)
+ - (Sfinalcond cond args succ1 succ2 info) represents a condition (which must
+ always be the last instruction in expansion list *)
+
+type expl =
+ | Snop of P.t
+ | Sr of P.t
+ | Sexp of P.t * rhs * P.t list * node option
+ | Sfinalcond of condition * P.t list * node * node * bool option
+
+(** Record used during the "dynamic" value numbering *)
+
+type numb = {
+ mutable nnext : int; (** Next unusued value number *)
+ mutable seqs : seq list; (** equations *)
+ mutable nreg : (P.t, int) Hashtbl.t; (** mapping registers to values *)
+ mutable nval : (int, P.t list) Hashtbl.t;
+ (** reverse mapping values to registers containing it *)
+}
+
+let print_list_pos l =
+ if exp_debug then eprintf "[";
+ List.iter (fun i -> if exp_debug then eprintf "%d;" (p2i i)) l;
+ if exp_debug then eprintf "]\n"
+
+let empty_numbering () =
+ { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 }
+
+let rec get_nvalues vn = function
+ | [] -> []
+ | r :: rs ->
+ let v =
+ match Hashtbl.find_opt !vn.nreg r with
+ | Some v ->
+ if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) v;
+ v
+ | None ->
+ let n = !vn.nnext in
+ if exp_debug then eprintf "getnval r=%d |-> v=%d\n" (p2i r) n;
+ !vn.nnext <- !vn.nnext + 1;
+ Hashtbl.replace !vn.nreg r n;
+ Hashtbl.replace !vn.nval n [ r ];
+ n
+ in
+ let vs = get_nvalues vn rs in
+ v :: vs
+
+let get_nval_ornil vn v =
+ match Hashtbl.find_opt !vn.nval v with None -> [] | Some l -> l
+
+let forget_reg vn rd =
+ match Hashtbl.find_opt !vn.nreg rd with
+ | Some v ->
+ if exp_debug then eprintf "forget_reg: r=%d |-> v=%d\n" (p2i rd) v;
+ let old_regs = get_nval_ornil vn v in
+ if exp_debug then eprintf "forget_reg: old_regs are:\n";
+ print_list_pos old_regs;
+ Hashtbl.replace !vn.nval v
+ (List.filter (fun n -> not (P.eq n rd)) old_regs)
+ | None ->
+ if exp_debug then eprintf "forget_reg: no mapping for r=%d\n" (p2i rd)
+
+let update_reg vn rd v =
+ if exp_debug then eprintf "update_reg: update v=%d with r=%d\n" v (p2i rd);
+ forget_reg vn rd;
+ let old_regs = get_nval_ornil vn v in
+ Hashtbl.replace !vn.nval v (rd :: old_regs)
+
+let rec find_valnum_rhs rh = function
+ | [] -> None
+ | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl
+
+let set_unknown vn rd =
+ if exp_debug then eprintf "set_unknown: rd=%d\n" (p2i rd);
+ forget_reg vn rd;
+ Hashtbl.remove !vn.nreg rd
+
+let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> ()
+
+let addrhs vn rd rh =
+ match find_valnum_rhs rh !vn.seqs with
+ | Some vres ->
+ if exp_debug then eprintf "addrhs: Some v=%d\n" vres;
+ Hashtbl.replace !vn.nreg rd vres;
+ update_reg vn rd vres
+ | None ->
+ let n = !vn.nnext in
+ if exp_debug then eprintf "addrhs: None v=%d\n" n;
+ !vn.nnext <- !vn.nnext + 1;
+ !vn.seqs <- Seq (n, rh) :: !vn.seqs;
+ update_reg vn rd n;
+ Hashtbl.replace !vn.nreg rd n
+
+let addsop vn v op rd =
+ if exp_debug then eprintf "addsop\n";
+ if op = Omove then (
+ update_reg vn rd (List.hd v);
+ Hashtbl.replace !vn.nreg rd (List.hd v))
+ else addrhs vn rd (Sop (op, v))
+
+let rec kill_mem_operations = function
+ | (Seq (v, Sop (op, vl)) as eq) :: tl ->
+ if op_depends_on_memory op then kill_mem_operations tl
+ else eq :: kill_mem_operations tl
+ | [] -> []
+ | eq :: tl -> eq :: kill_mem_operations tl
+
+let reg_valnum vn v =
+ if exp_debug then eprintf "reg_valnum: trying to find a mapping for v=%d\n" v;
+ match Hashtbl.find !vn.nval v with
+ | [] -> None
+ | r :: rs ->
+ if exp_debug then eprintf "reg_valnum: found a mapping r=%d\n" (p2i r);
+ Some r
+
+let rec reg_valnums vn = function
+ | [] -> Some []
+ | v :: vs -> (
+ match (reg_valnum vn v, reg_valnums vn vs) with
+ | Some r, Some rs -> Some (r :: rs)
+ | _, _ -> None)
+
+let find_rhs vn rh =
+ match find_valnum_rhs rh !vn.seqs with
+ | None -> None
+ | Some vres -> reg_valnum vn vres
+
+(** Functions to perform the dynamic reduction during CSE *)
+
+let extract_arg l =
+ if List.length l > 0 then
+ match List.hd l with
+ | Sr r -> (r, List.tl l)
+ | Sexp (rd, _, _, _) -> (rd, l)
+ | _ -> failwith "extract_arg: final instruction arg can not be extracted"
+ else failwith "extract_arg: trying to extract on an empty list"
+
+let extract_final vn fl fdest succ =
+ if List.length fl > 0 then
+ match List.hd fl with
+ | Sr r ->
+ if not (P.eq r fdest) then (
+ let v = get_nvalues vn [ r ] in
+ addsop vn v Omove fdest;
+ Sexp (fdest, Smove, [ r ], Some succ) :: List.tl fl)
+ else Snop succ :: List.tl fl
+ | Sexp (rd, rh, args, None) ->
+ assert (rd = fdest);
+ Sexp (fdest, rh, args, Some succ) :: List.tl fl
+ | _ -> fl
+ else failwith "extract_final: trying to extract on an empty list"
+
+let addinst vn op args rd =
+ let v = get_nvalues vn args in
+ let rh = Sop (op, v) in
+ match find_rhs vn rh with
+ | Some r ->
+ if exp_debug then eprintf "addinst: rhs found with r=%d\n" (p2i r);
+ Sr r
+ | None ->
+ addsop vn v op rd;
+ Sexp (rd, rh, args, None)
+
+(** Expansion functions *)
+
type immt =
| Addiw
| Addil
@@ -59,152 +238,109 @@ type immt =
| Sltil
| Sltiul
-let find_or_addnmove op args rd succ map_consts not_final =
- let sop = Sop (op, args) in
- match Hashtbl.find_opt map_consts sop with
- | Some r ->
- if not_final then node := !node - 1;
- Sr (P.of_int r)
- | None ->
- if (not (List.exists (fun a -> a = rd) args)) && not_final then
- Hashtbl.add map_consts sop (p2i rd);
- Si (Iop (op, args, rd, succ))
-
-let build_head_tuple head sv =
- match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r)
-
-let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r
-
-let unzip_head_tuple_move ht r succ =
- match ht with
- | l, Some r' ->
- if r' != r then [ Iop (Omove, [ r' ], r, succ) ] else [ Inop succ ]
- | l, None -> l
-
-let build_full_ilist op args dest succ hd k map_consts =
- let sv = find_or_addnmove op args dest succ map_consts false in
- let ht = build_head_tuple hd sv in
- unzip_head_tuple_move ht dest succ @ k
-
-let load_hilo32 dest hi lo succ map_consts not_final =
+let load_hilo32 vn dest hi lo =
let op1 = OEluiw hi in
- if Int.eq lo Int.zero then
- let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
- build_head_tuple [] sv
+ if Int.eq lo Int.zero then [ addinst vn op1 [] dest ]
else
let r = r2pi () in
- let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in
- let ht1 = build_head_tuple [] sv1 in
- let r' = unzip_head_tuple ht1 r in
- let op2 = OEaddiw lo in
- let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in
- build_head_tuple (fst ht1) sv2
-
-let load_hilo64 dest hi lo succ map_consts not_final =
+ let op2 = OEaddiw (None, lo) in
+ let i1 = addinst vn op1 [] r in
+ let r', l = extract_arg [ i1 ] in
+ let i2 = addinst vn op2 [ r' ] dest in
+ i2 :: l
+
+let load_hilo64 vn dest hi lo =
let op1 = OEluil hi in
- if Int64.eq lo Int64.zero then
- let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
- build_head_tuple [] sv
+ if Int64.eq lo Int64.zero then [ addinst vn op1 [] dest ]
else
let r = r2pi () in
- let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts not_final in
- let ht1 = build_head_tuple [] sv1 in
- let r' = unzip_head_tuple ht1 r in
- let op2 = OEaddil lo in
- let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts not_final in
- build_head_tuple (fst ht1) sv2
-
-let loadimm32 dest n succ map_consts not_final =
+ let op2 = OEaddil (None, lo) in
+ let i1 = addinst vn op1 [] r in
+ let r', l = extract_arg [ i1 ] in
+ let i2 = addinst vn op2 [ r' ] dest in
+ i2 :: l
+
+let loadimm32 vn dest n =
match make_immed32 n with
| Imm32_single imm ->
- let op1 = OEimmR0 (OPimmADD imm) in
- let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
- build_head_tuple [] sv
- | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts not_final
+ let op1 = OEaddiw (Some X0_R, imm) in
+ [ addinst vn op1 [] dest ]
+ | Imm32_pair (hi, lo) -> load_hilo32 vn dest hi lo
-let loadimm64 dest n succ map_consts not_final =
+let loadimm64 vn dest n =
match make_immed64 n with
| Imm64_single imm ->
- let op1 = OEimmR0 (OPimmADDL imm) in
- let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
- build_head_tuple [] sv
- | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts not_final
+ let op1 = OEaddil (Some X0_R, imm) in
+ [ addinst vn op1 [] dest ]
+ | Imm64_pair (hi, lo) -> load_hilo64 vn dest hi lo
| Imm64_large imm ->
let op1 = OEloadli imm in
- let sv = find_or_addnmove op1 [] dest succ map_consts not_final in
- build_head_tuple [] sv
+ [ addinst vn op1 [] dest ]
-let get_opimm imm = function
- | Addiw -> OEaddiw imm
+let get_opimm optR imm = function
+ | Addiw -> OEaddiw (optR, imm)
| Andiw -> OEandiw imm
| Oriw -> OEoriw imm
| Xoriw -> OExoriw imm
| Sltiw -> OEsltiw imm
| Sltiuw -> OEsltiuw imm
- | Addil -> OEaddil imm
+ | Addil -> OEaddil (optR, imm)
| Andil -> OEandil imm
| Oril -> OEoril imm
| Xoril -> OExoril imm
| Sltil -> OEsltil imm
| Sltiul -> OEsltiul imm
-let opimm32 a1 dest n succ k op opimm map_consts =
+let opimm32 vn a1 dest n optR op opimm =
match make_immed32 n with
- | Imm32_single imm ->
- build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts
+ | Imm32_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ]
| Imm32_pair (hi, lo) ->
let r = r2pi () in
- let ht = load_hilo32 r hi lo (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts
+ let l = load_hilo32 vn r hi lo in
+ let r', l' = extract_arg l in
+ let i = addinst vn op [ a1; r' ] dest in
+ i :: l'
-let opimm64 a1 dest n succ k op opimm map_consts =
+let opimm64 vn a1 dest n optR op opimm =
match make_immed64 n with
- | Imm64_single imm ->
- build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts
+ | Imm64_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ]
| Imm64_pair (hi, lo) ->
let r = r2pi () in
- let ht = load_hilo64 r hi lo (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts
+ let l = load_hilo64 vn r hi lo in
+ let r', l' = extract_arg l in
+ let i = addinst vn op [ a1; r' ] dest in
+ i :: l'
| Imm64_large imm ->
let r = r2pi () in
let op1 = OEloadli imm in
- let inode = n2pi () in
- let sv = find_or_addnmove op1 [] r inode map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts
+ let i1 = addinst vn op1 [] r in
+ let r', l' = extract_arg [ i1 ] in
+ let i2 = addinst vn op [ a1; r' ] dest in
+ i2 :: l'
-let addimm32 a1 dest n succ k map_consts =
- opimm32 a1 dest n succ k Oadd Addiw map_consts
+let addimm32 vn a1 dest n optR = opimm32 vn a1 dest n optR Oadd Addiw
-let andimm32 a1 dest n succ k map_consts =
- opimm32 a1 dest n succ k Oand Andiw map_consts
+let andimm32 vn a1 dest n = opimm32 vn a1 dest n None Oand Andiw
-let orimm32 a1 dest n succ k map_consts =
- opimm32 a1 dest n succ k Oor Oriw map_consts
+let orimm32 vn a1 dest n = opimm32 vn a1 dest n None Oor Oriw
-let xorimm32 a1 dest n succ k map_consts =
- opimm32 a1 dest n succ k Oxor Xoriw map_consts
+let xorimm32 vn a1 dest n = opimm32 vn a1 dest n None Oxor Xoriw
-let sltimm32 a1 dest n succ k map_consts =
- opimm32 a1 dest n succ k (OEsltw None) Sltiw map_consts
+let sltimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltw None) Sltiw
-let sltuimm32 a1 dest n succ k map_consts =
- opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts
+let sltuimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltuw None) Sltiuw
-let addimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oaddl Addil
+let addimm64 vn a1 dest n optR = opimm64 vn a1 dest n optR Oaddl Addil
-let andimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oandl Andil
+let andimm64 vn a1 dest n = opimm64 vn a1 dest n None Oandl Andil
-let orimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oorl Oril
+let orimm64 vn a1 dest n = opimm64 vn a1 dest n None Oorl Oril
-let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril
+let xorimm64 vn a1 dest n = opimm64 vn a1 dest n None Oxorl Xoril
-let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil
+let sltimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltl None) Sltil
-let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul
+let sltuimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltul None) Sltiul
let is_inv_cmp = function Cle | Cgt -> true | _ -> false
@@ -214,276 +350,288 @@ let make_optR is_x0 is_inv =
let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k =
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
- | Ceq -> Icond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Cne -> Icond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Clt -> Icond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Cle -> Icond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k
- | Cgt -> Icond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k
- | Cge -> Icond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Ceq -> Sfinalcond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Cne -> Sfinalcond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Clt -> Sfinalcond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Cle -> Sfinalcond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k
+ | Cgt -> Sfinalcond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k
+ | Cge -> Sfinalcond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k
let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k =
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
- | Ceq -> Icond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Cne -> Icond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Clt -> Icond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Cle -> Icond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k
- | Cgt -> Icond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k
- | Cge -> Icond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Ceq -> Sfinalcond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Cne -> Sfinalcond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Clt -> Sfinalcond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Cle -> Sfinalcond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k
+ | Cgt -> Sfinalcond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k
+ | Cge -> Sfinalcond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k
let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k =
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
- | Ceq -> Icond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Cne -> Icond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Clt -> Icond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Cle -> Icond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k
- | Cgt -> Icond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k
- | Cge -> Icond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Ceq -> Sfinalcond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Cne -> Sfinalcond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Clt -> Sfinalcond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Cle -> Sfinalcond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k
+ | Cgt -> Sfinalcond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k
+ | Cge -> Sfinalcond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k
let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k =
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
- | Ceq -> Icond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Cne -> Icond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Clt -> Icond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k
- | Cle -> Icond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k
- | Cgt -> Icond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k
- | Cge -> Icond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k
-
-let cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
+ | Ceq -> Sfinalcond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Cne -> Sfinalcond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Clt -> Sfinalcond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k
+ | Cle -> Sfinalcond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k
+ | Cgt -> Sfinalcond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k
+ | Cge -> Sfinalcond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k
+
+let cond_int32s vn is_x0 cmp a1 a2 dest =
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
- | Ceq -> [ Iop (OEseqw optR, [ a1; a2 ], dest, succ) ]
- | Cne -> [ Iop (OEsnew optR, [ a1; a2 ], dest, succ) ]
- | Clt -> [ Iop (OEsltw optR, [ a1; a2 ], dest, succ) ]
+ | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest ]
+ | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest ]
+ | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest ]
| Cle ->
let r = r2pi () in
let op = OEsltw optR in
- let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
- | Cgt -> [ Iop (OEsltw optR, [ a2; a1 ], dest, succ) ]
+ let i1 = addinst vn op [ a2; a1 ] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
+ | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest ]
| Cge ->
let r = r2pi () in
let op = OEsltw optR in
- let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
+ let i1 = addinst vn op [ a1; a2 ] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
-let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
+let cond_int32u vn is_x0 cmp a1 a2 dest =
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
- | Ceq -> [ Iop (OEsequw optR, [ a1; a2 ], dest, succ) ]
- | Cne -> [ Iop (OEsneuw optR, [ a1; a2 ], dest, succ) ]
- | Clt -> [ Iop (OEsltuw optR, [ a1; a2 ], dest, succ) ]
+ | Ceq -> [ addinst vn (OEsequw optR) [ a1; a2 ] dest ]
+ | Cne -> [ addinst vn (OEsneuw optR) [ a1; a2 ] dest ]
+ | Clt -> [ addinst vn (OEsltuw optR) [ a1; a2 ] dest ]
| Cle ->
let r = r2pi () in
let op = OEsltuw optR in
- let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
- | Cgt -> [ Iop (OEsltuw optR, [ a2; a1 ], dest, succ) ]
+ let i1 = addinst vn op [ a2; a1 ] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
+ | Cgt -> [ addinst vn (OEsltuw optR) [ a2; a1 ] dest ]
| Cge ->
let r = r2pi () in
let op = OEsltuw optR in
- let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
+ let i1 = addinst vn op [ a1; a2 ] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
-let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
+let cond_int64s vn is_x0 cmp a1 a2 dest =
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
- | Ceq -> [ Iop (OEseql optR, [ a1; a2 ], dest, succ) ]
- | Cne -> [ Iop (OEsnel optR, [ a1; a2 ], dest, succ) ]
- | Clt -> [ Iop (OEsltl optR, [ a1; a2 ], dest, succ) ]
+ | Ceq -> [ addinst vn (OEseql optR) [ a1; a2 ] dest ]
+ | Cne -> [ addinst vn (OEsnel optR) [ a1; a2 ] dest ]
+ | Clt -> [ addinst vn (OEsltl optR) [ a1; a2 ] dest ]
| Cle ->
let r = r2pi () in
let op = OEsltl optR in
- let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
- | Cgt -> [ Iop (OEsltl optR, [ a2; a1 ], dest, succ) ]
+ let i1 = addinst vn op [ a2; a1 ] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
+ | Cgt -> [ addinst vn (OEsltl optR) [ a2; a1 ] dest ]
| Cge ->
let r = r2pi () in
let op = OEsltl optR in
- let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
+ let i1 = addinst vn op [ a1; a2 ] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
-let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ map_consts =
+let cond_int64u vn is_x0 cmp a1 a2 dest =
let optR = make_optR is_x0 (is_inv_cmp cmp) in
match cmp with
- | Ceq -> [ Iop (OEsequl optR, [ a1; a2 ], dest, succ) ]
- | Cne -> [ Iop (OEsneul optR, [ a1; a2 ], dest, succ) ]
- | Clt -> [ Iop (OEsltul optR, [ a1; a2 ], dest, succ) ]
+ | Ceq -> [ addinst vn (OEsequl optR) [ a1; a2 ] dest ]
+ | Cne -> [ addinst vn (OEsneul optR) [ a1; a2 ] dest ]
+ | Clt -> [ addinst vn (OEsltul optR) [ a1; a2 ] dest ]
| Cle ->
let r = r2pi () in
let op = OEsltul optR in
- let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
- | Cgt -> [ Iop (OEsltul optR, [ a2; a1 ], dest, succ) ]
+ let i1 = addinst vn op [ a2; a1 ] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
+ | Cgt -> [ addinst vn (OEsltul optR) [ a2; a1 ] dest ]
| Cge ->
let r = r2pi () in
let op = OEsltul optR in
- let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
- fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ]
+ let i1 = addinst vn op [ a1; a2 ] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
let is_normal_cmp = function Cne -> false | _ -> true
-let cond_float cmp f1 f2 dest succ map_consts =
+let cond_float vn cmp f1 f2 dest =
match cmp with
- | Ceq -> [ Iop (OEfeqd, [ f1; f2 ], dest, succ) ]
- | Cne -> [ Iop (OEfeqd, [ f1; f2 ], dest, succ) ]
- | Clt -> [ Iop (OEfltd, [ f1; f2 ], dest, succ) ]
- | Cle -> [ Iop (OEfled, [ f1; f2 ], dest, succ) ]
- | Cgt -> [ Iop (OEfltd, [ f2; f1 ], dest, succ) ]
- | Cge -> [ Iop (OEfled, [ f2; f1 ], dest, succ) ]
-
-let cond_single cmp f1 f2 dest succ map_consts =
+ | Ceq -> [ addinst vn OEfeqd [ f1; f2 ] dest ]
+ | Cne -> [ addinst vn OEfeqd [ f1; f2 ] dest ]
+ | Clt -> [ addinst vn OEfltd [ f1; f2 ] dest ]
+ | Cle -> [ addinst vn OEfled [ f1; f2 ] dest ]
+ | Cgt -> [ addinst vn OEfltd [ f2; f1 ] dest ]
+ | Cge -> [ addinst vn OEfled [ f2; f1 ] dest ]
+
+let cond_single vn cmp f1 f2 dest =
match cmp with
- | Ceq -> [ Iop (OEfeqs, [ f1; f2 ], dest, succ) ]
- | Cne -> [ Iop (OEfeqs, [ f1; f2 ], dest, succ) ]
- | Clt -> [ Iop (OEflts, [ f1; f2 ], dest, succ) ]
- | Cle -> [ Iop (OEfles, [ f1; f2 ], dest, succ) ]
- | Cgt -> [ Iop (OEflts, [ f2; f1 ], dest, succ) ]
- | Cge -> [ Iop (OEfles, [ f2; f1 ], dest, succ) ]
-
-let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k map_consts =
- if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k
+ | Ceq -> [ addinst vn OEfeqs [ f1; f2 ] dest ]
+ | Cne -> [ addinst vn OEfeqs [ f1; f2 ] dest ]
+ | Clt -> [ addinst vn OEflts [ f1; f2 ] dest ]
+ | Cle -> [ addinst vn OEfles [ f1; f2 ] dest ]
+ | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ]
+ | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ]
+
+let expanse_cbranchimm_int32s vn cmp a1 n info succ1 succ2 =
+ if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 []
else
let r = r2pi () in
- let ht = loadimm32 r n (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k
+ let l = loadimm32 vn r n in
+ let r', l' = extract_arg l in
+ cbranch_int32s false cmp a1 r' info succ1 succ2 l'
-let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k map_consts =
- if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k
+let expanse_cbranchimm_int32u vn cmp a1 n info succ1 succ2 =
+ if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 []
else
let r = r2pi () in
- let ht = loadimm32 r n (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k
+ let l = loadimm32 vn r n in
+ let r', l' = extract_arg l in
+ cbranch_int32u false cmp a1 r' info succ1 succ2 l'
-let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k map_consts =
- if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k
+let expanse_cbranchimm_int64s vn cmp a1 n info succ1 succ2 =
+ if Int64.eq n Int64.zero then
+ cbranch_int64s true cmp a1 a1 info succ1 succ2 []
else
let r = r2pi () in
- let ht = loadimm64 r n (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k
+ let l = loadimm64 vn r n in
+ let r', l' = extract_arg l in
+ cbranch_int64s false cmp a1 r' info succ1 succ2 l'
-let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts =
- if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k
+let expanse_cbranchimm_int64u vn cmp a1 n info succ1 succ2 =
+ if Int64.eq n Int64.zero then
+ cbranch_int64u true cmp a1 a1 info succ1 succ2 []
else
let r = r2pi () in
- let ht = loadimm64 r n (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k
-
-let get_tmp_reg = function Cle | Cge -> Some (n2pi ()) | _ -> None
+ let l = loadimm64 vn r n in
+ let r', l' = extract_arg l in
+ cbranch_int64u false cmp a1 r' info succ1 succ2 l'
-let expanse_condimm_int32s cmp a1 n dest succ map_consts =
- if Int.eq n Int.zero then
- let tmp_reg = get_tmp_reg cmp in
- cond_int32s true cmp a1 a1 dest tmp_reg succ map_consts
+let expanse_condimm_int32s vn cmp a1 n dest =
+ if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest
else
match cmp with
| Ceq | Cne ->
let r = r2pi () in
- xorimm32 a1 r n (n2pi ())
- (cond_int32s true cmp r r dest None succ map_consts)
- map_consts
- | Clt -> sltimm32 a1 dest n succ [] map_consts
+ let l = xorimm32 vn a1 r n in
+ let r', l' = extract_arg l in
+ cond_int32s vn true cmp r' r' dest @ l'
+ | Clt -> sltimm32 vn a1 dest n
| Cle ->
if Int.eq n (Int.repr Int.max_signed) then
- let ht = loadimm32 dest Int.one succ map_consts false in
- fst ht
- else sltimm32 a1 dest (Int.add n Int.one) succ [] map_consts
+ let l = loadimm32 vn dest Int.one in
+ let r, l' = extract_arg l in
+ addinst vn (OEmayundef MUint) [ a1; r ] dest :: l'
+ else sltimm32 vn a1 dest (Int.add n Int.one)
| _ ->
let r = r2pi () in
- let tmp_reg = get_tmp_reg cmp in
- let ht = loadimm32 r n (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- fst ht @ cond_int32s false cmp a1 r' dest tmp_reg succ map_consts
-
-let expanse_condimm_int32u cmp a1 n dest succ map_consts =
- let tmp_reg = get_tmp_reg cmp in
- if Int.eq n Int.zero then
- cond_int32u true cmp a1 a1 dest tmp_reg succ map_consts
+ let l = loadimm32 vn r n in
+ let r', l' = extract_arg l in
+ cond_int32s vn false cmp a1 r' dest @ l'
+
+let expanse_condimm_int32u vn cmp a1 n dest =
+ if Int.eq n Int.zero then cond_int32u vn true cmp a1 a1 dest
else
match cmp with
- | Clt -> sltuimm32 a1 dest n succ [] map_consts
+ | Clt -> sltuimm32 vn a1 dest n
| _ ->
let r = r2pi () in
- let ht = loadimm32 r n (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- fst ht @ cond_int32u false cmp a1 r' dest tmp_reg succ map_consts
+ let l = loadimm32 vn r n in
+ let r', l' = extract_arg l in
+ cond_int32u vn false cmp a1 r' dest @ l'
-let expanse_condimm_int64s cmp a1 n dest succ map_consts =
- if Int64.eq n Int64.zero then
- let tmp_reg = get_tmp_reg cmp in
- cond_int64s true cmp a1 a1 dest tmp_reg succ map_consts
+let expanse_condimm_int64s vn cmp a1 n dest =
+ if Int64.eq n Int64.zero then cond_int64s vn true cmp a1 a1 dest
else
match cmp with
| Ceq | Cne ->
let r = r2pi () in
- xorimm64 a1 r n (n2pi ())
- (cond_int64s true cmp r r dest None succ map_consts)
- map_consts
- | Clt -> sltimm64 a1 dest n succ [] map_consts
+ let l = xorimm64 vn a1 r n in
+ let r', l' = extract_arg l in
+ cond_int64s vn true cmp r' r' dest @ l'
+ | Clt -> sltimm64 vn a1 dest n
| Cle ->
if Int64.eq n (Int64.repr Int64.max_signed) then
- let ht = loadimm32 dest Int.one succ map_consts false in
- fst ht
- else sltimm64 a1 dest (Int64.add n Int64.one) succ [] map_consts
+ let l = loadimm32 vn dest Int.one in
+ let r, l' = extract_arg l in
+ addinst vn (OEmayundef MUlong) [ a1; r ] dest :: l'
+ else sltimm64 vn a1 dest (Int64.add n Int64.one)
| _ ->
let r = r2pi () in
- let tmp_reg = get_tmp_reg cmp in
- let ht = loadimm64 r n (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- fst ht @ cond_int64s false cmp a1 r' dest tmp_reg succ map_consts
+ let l = loadimm64 vn r n in
+ let r', l' = extract_arg l in
+ cond_int64s vn false cmp a1 r' dest @ l'
-let expanse_condimm_int64u cmp a1 n dest succ map_consts =
- let tmp_reg = get_tmp_reg cmp in
- if Int64.eq n Int64.zero then
- cond_int64u true cmp a1 a1 dest tmp_reg succ map_consts
+let expanse_condimm_int64u vn cmp a1 n dest =
+ if Int64.eq n Int64.zero then cond_int64u vn true cmp a1 a1 dest
else
match cmp with
- | Clt -> sltuimm64 a1 dest n succ [] map_consts
+ | Clt -> sltuimm64 vn a1 dest n
| _ ->
let r = r2pi () in
- let ht = loadimm64 r n (n2pi ()) map_consts true in
- let r' = unzip_head_tuple ht r in
- fst ht @ cond_int64u false cmp a1 r' dest tmp_reg succ map_consts
+ let l = loadimm64 vn r n in
+ let r', l' = extract_arg l in
+ cond_int64u vn false cmp a1 r' dest @ l'
-let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ map_consts =
+let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest =
let normal = is_normal_cmp cmp in
let normal' = if cnot then not normal else normal in
- let succ' = if normal' then succ else n2pi () in
- let insn = fn_cond cmp f1 f2 dest succ' map_consts in
+ let insn = fn_cond vn cmp f1 f2 dest in
if normal' then insn
- else build_full_ilist (OExoriw Int.one) [ dest ] dest succ insn [] map_consts
+ else
+ let r', l = extract_arg insn in
+ addinst vn (OExoriw Int.one) [ r' ] dest :: l
-let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 map_consts =
+let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 info succ1 succ2 =
let r = r2pi () in
let normal = is_normal_cmp cmp in
let normal' = if cnot then not normal else normal in
- let insn = List.hd (fn_cond cmp f1 f2 r (n2pi ()) map_consts) in
- insn
- ::
- (if normal' then [ Icond (CEbnew (Some X0_R), [ r; r ], succ1, succ2, info) ]
- else [ Icond (CEbeqw (Some X0_R), [ r; r ], succ1, succ2, info) ])
+ let insn = fn_cond vn cmp f1 f2 r in
+ let r', l = extract_arg insn in
+ if normal' then
+ Sfinalcond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l
+ else Sfinalcond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l
+
+let addptrofs vn n dest =
+ if Ptrofs.eq_dec n Ptrofs.zero then [ addinst vn OEmoveSP [] dest ]
+ else if Archi.ptr64 then
+ match make_immed64 (Ptrofs.to_int64 n) with
+ | Imm64_single imm -> [ addinst vn (OEaddil (Some SP_S, imm)) [] dest ]
+ | Imm64_pair (hi, lo) ->
+ let r = r2pi () in
+ let l = load_hilo64 vn r hi lo in
+ let r', l' = extract_arg l in
+ addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: l'
+ | Imm64_large imm ->
+ let r = r2pi () in
+ let op1 = OEloadli imm in
+ let i1 = addinst vn op1 [] r in
+ let r', l = extract_arg [ i1 ] in
+ addinst vn (OEaddil (Some SP_S, Int64.zero)) [ r' ] dest :: l
+ else
+ match make_immed32 (Ptrofs.to_int n) with
+ | Imm32_single imm -> [ addinst vn (OEaddiw (Some SP_S, imm)) [] dest ]
+ | Imm32_pair (hi, lo) ->
+ let r = r2pi () in
+ let l = load_hilo32 vn r hi lo in
+ let r', l' = extract_arg l in
+ addinst vn (OEaddiw (Some SP_S, Int.zero)) [ r' ] dest :: l'
+
+(** Form a list containing both sources and destination regs of an instruction *)
let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
@@ -501,11 +649,11 @@ let get_regs_inst = function
| Ireturn (Some r) -> [ r ]
| _ -> []
-let write_initial_node initial code' new_order =
- code' := PTree.set initial (Inop (n2p ())) !code';
- new_order := initial :: !new_order
+(** Modify pathmap according to the size of the expansion list *)
let write_pathmap initial esize pm' =
+ if exp_debug then
+ eprintf "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize;
let path = get_some @@ PTree.get initial !pm' in
let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in
let path' =
@@ -518,22 +666,51 @@ let write_pathmap initial esize pm' =
in
pm' := PTree.set initial path' !pm'
-let rec write_tree exp initial current code' new_order fturn =
- (*Printf.eprintf "wt: node is %d\n" !node;*)
+(** Write a single instruction in the tree and update order *)
+
+let write_inst target_node inst code' new_order =
+ code' := PTree.set (P.of_int target_node) inst !code';
+ new_order := P.of_int target_node :: !new_order
+
+(** Return olds args if the CSE numbering is empty *)
+
+let get_arguments vn vals args =
+ match reg_valnums vn vals with Some args' -> args' | None -> args
+
+(** Update the code tree with the expansion list *)
+
+let rec write_tree vn exp initial current code' new_order fturn =
+ if exp_debug then eprintf "wt: node is %d\n" !node;
let target_node, next_node =
if fturn then (P.to_int initial, current) else (current, current - 1)
in
match exp with
- | inst :: k ->
- (*let open PrintRTL in*)
- (*print_instruction stderr (target_node, inst);*)
- code' := PTree.set (P.of_int target_node) inst !code';
- new_order := P.of_int target_node :: !new_order;
- write_tree k initial next_node code' new_order false
+ | Sr r :: _ ->
+ failwith "write_tree: there are still some symbolic values in the list"
+ | Sexp (rd, Sop (op, vals), args, None) :: k ->
+ let args = get_arguments vn vals args in
+ let inst = Iop (op, args, rd, P.of_int next_node) in
+ write_inst target_node inst code' new_order;
+ write_tree vn k initial next_node code' new_order false
+ | [ Snop succ ] ->
+ let inst = Inop succ in
+ write_inst target_node inst code' new_order
+ | [ Sexp (rd, Sop (op, vals), args, Some succ) ] ->
+ let args = get_arguments vn vals args in
+ let inst = Iop (op, args, rd, succ) in
+ write_inst target_node inst code' new_order
+ | [ Sexp (rd, Smove, args, Some succ) ] ->
+ let inst = Iop (Omove, args, rd, succ) in
+ write_inst target_node inst code' new_order
+ | [ Sfinalcond (cond, args, succ1, succ2, info) ] ->
+ let inst = Icond (cond, args, succ1, succ2, info) in
+ write_inst target_node inst code' new_order
| [] -> ()
+ | _ -> failwith "write_tree: invalid list"
+(** Main expansion function - TODO gourdinl to split? *)
let expanse (sb : superblock) code pm =
- (*debug_flag := true;*)
+ if exp_debug then eprintf "#### New superblock for expansion oracle\n";
let new_order = ref [] in
let liveins = ref sb.liveins in
let exp = ref [] in
@@ -541,336 +718,342 @@ let expanse (sb : superblock) code pm =
let was_exp = ref false in
let code' = ref code in
let pm' = ref pm in
- let map_consts = Hashtbl.create 100 in
+ let vn = ref (empty_numbering ()) in
Array.iter
(fun n ->
was_branch := false;
was_exp := false;
let inst = get_some @@ PTree.get n code in
+ if exp_debug then eprintf "We are checking node %d\n" (p2i n);
(if !Clflags.option_fexpanse_rtlcond then
match inst with
(* Expansion of conditions - Ocmp *)
| Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) ->
- debug "Iop/Ccomp\n";
- let tmp_reg = get_tmp_reg c in
- exp := cond_int32s false c a1 a2 dest tmp_reg succ map_consts;
+ if exp_debug then eprintf "Iop/Ccomp\n";
+ exp := cond_int32s vn false c a1 a2 dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) ->
- debug "Iop/Ccompu\n";
- let tmp_reg = get_tmp_reg c in
- exp := cond_int32u false c a1 a2 dest tmp_reg succ map_consts;
+ if exp_debug then eprintf "Iop/Ccompu\n";
+ exp := cond_int32u vn false c a1 a2 dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) ->
- debug "Iop/Ccompimm\n";
- exp := expanse_condimm_int32s c a1 imm dest succ map_consts;
+ if exp_debug then eprintf "Iop/Ccompimm\n";
+ exp := expanse_condimm_int32s vn c a1 imm dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) ->
- debug "Iop/Ccompuimm\n";
- exp := expanse_condimm_int32u c a1 imm dest succ map_consts;
+ if exp_debug then eprintf "Iop/Ccompuimm\n";
+ exp := expanse_condimm_int32u vn c a1 imm dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) ->
- debug "Iop/Ccompl\n";
- let tmp_reg = get_tmp_reg c in
- exp := cond_int64s false c a1 a2 dest tmp_reg succ map_consts;
+ if exp_debug then eprintf "Iop/Ccompl\n";
+ exp := cond_int64s vn false c a1 a2 dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) ->
- debug "Iop/Ccomplu\n";
- let tmp_reg = get_tmp_reg c in
- exp := cond_int64u false c a1 a2 dest tmp_reg succ map_consts;
+ if exp_debug then eprintf "Iop/Ccomplu\n";
+ exp := cond_int64u vn false c a1 a2 dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) ->
- debug "Iop/Ccomplimm\n";
- exp := expanse_condimm_int64s c a1 imm dest succ map_consts;
+ if exp_debug then eprintf "Iop/Ccomplimm\n";
+ exp := expanse_condimm_int64s vn c a1 imm dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) ->
- debug "Iop/Ccompluimm\n";
- exp := expanse_condimm_int64u c a1 imm dest succ map_consts;
+ if exp_debug then eprintf "Iop/Ccompluimm\n";
+ exp := expanse_condimm_int64u vn c a1 imm dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) ->
- debug "Iop/Ccompf\n";
- exp := expanse_cond_fp false cond_float c f1 f2 dest succ map_consts;
+ if exp_debug then eprintf "Iop/Ccompf\n";
+ exp := expanse_cond_fp vn false cond_float c f1 f2 dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) ->
- debug "Iop/Cnotcompf\n";
- exp := expanse_cond_fp true cond_float c f1 f2 dest succ map_consts;
+ if exp_debug then eprintf "Iop/Cnotcompf\n";
+ exp := expanse_cond_fp vn true cond_float c f1 f2 dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) ->
- debug "Iop/Ccompfs\n";
- exp := expanse_cond_fp false cond_single c f1 f2 dest succ map_consts;
+ if exp_debug then eprintf "Iop/Ccompfs\n";
+ exp := expanse_cond_fp vn false cond_single c f1 f2 dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) ->
- debug "Iop/Cnotcompfs\n";
- exp := expanse_cond_fp true cond_single c f1 f2 dest succ map_consts;
+ if exp_debug then eprintf "Iop/Cnotcompfs\n";
+ exp := expanse_cond_fp vn true cond_single c f1 f2 dest;
+ exp := extract_final vn !exp dest succ;
was_exp := true
(* Expansion of branches - Ccomp *)
| Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccomp\n";
+ if exp_debug then eprintf "Icond/Ccomp\n";
exp := cbranch_int32s false c a1 a2 info succ1 succ2 [];
was_branch := true;
was_exp := true
| Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccompu\n";
+ if exp_debug then eprintf "Icond/Ccompu\n";
exp := cbranch_int32u false c a1 a2 info succ1 succ2 [];
was_branch := true;
was_exp := true
| Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccompimm\n";
- exp :=
- expanse_cbranchimm_int32s c a1 imm info succ1 succ2 [] map_consts;
+ if exp_debug then eprintf "Icond/Ccompimm\n";
+ exp := expanse_cbranchimm_int32s vn c a1 imm info succ1 succ2;
was_branch := true;
was_exp := true
| Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccompuimm\n";
- exp :=
- expanse_cbranchimm_int32u c a1 imm info succ1 succ2 [] map_consts;
+ if exp_debug then eprintf "Icond/Ccompuimm\n";
+ exp := expanse_cbranchimm_int32u vn c a1 imm info succ1 succ2;
was_branch := true;
was_exp := true
| Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccompl\n";
+ if exp_debug then eprintf "Icond/Ccompl\n";
exp := cbranch_int64s false c a1 a2 info succ1 succ2 [];
was_branch := true;
was_exp := true
| Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccomplu\n";
+ if exp_debug then eprintf "Icond/Ccomplu\n";
exp := cbranch_int64u false c a1 a2 info succ1 succ2 [];
was_branch := true;
was_exp := true
| Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccomplimm\n";
- exp :=
- expanse_cbranchimm_int64s c a1 imm info succ1 succ2 [] map_consts;
+ if exp_debug then eprintf "Icond/Ccomplimm\n";
+ exp := expanse_cbranchimm_int64s vn c a1 imm info succ1 succ2;
was_branch := true;
was_exp := true
| Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccompluimm\n";
- exp :=
- expanse_cbranchimm_int64u c a1 imm info succ1 succ2 [] map_consts;
+ if exp_debug then eprintf "Icond/Ccompluimm\n";
+ exp := expanse_cbranchimm_int64u vn c a1 imm info succ1 succ2;
was_branch := true;
was_exp := true
| Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccompf\n";
+ if exp_debug then eprintf "Icond/Ccompf\n";
exp :=
- expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2
- map_consts;
+ expanse_cbranch_fp vn false cond_float c f1 f2 info succ1 succ2;
was_branch := true;
was_exp := true
| Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) ->
- debug "Icond/Cnotcompf\n";
- exp :=
- expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2
- map_consts;
+ if exp_debug then eprintf "Icond/Cnotcompf\n";
+ exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2;
was_branch := true;
was_exp := true
| Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
- debug "Icond/Ccompfs\n";
+ if exp_debug then eprintf "Icond/Ccompfs\n";
exp :=
- expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2
- map_consts;
+ expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2;
was_branch := true;
was_exp := true
| Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) ->
- debug "Icond/Cnotcompfs\n";
+ if exp_debug then eprintf "Icond/Cnotcompfs\n";
exp :=
- expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2
- map_consts;
+ expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2;
was_branch := true;
was_exp := true
| _ -> ());
(if !Clflags.option_fexpanse_others && not !was_exp then
match inst with
- (* Expansion of fp constants *)
| Iop (Ofloatconst f, nil, dest, succ) ->
- debug "Iop/Ofloatconst\n";
+ if exp_debug then eprintf "Iop/Ofloatconst\n";
let r = r2pi () in
- let ht =
- loadimm64 r (Floats.Float.to_bits f) (n2pi ()) map_consts true
- in
- let r' = unzip_head_tuple ht r in
- exp :=
- build_full_ilist Ofloat_of_bits [ r' ] dest succ (fst ht) []
- map_consts;
+ let l = loadimm64 vn r (Floats.Float.to_bits f) in
+ let r', l' = extract_arg l in
+ exp := addinst vn Ofloat_of_bits [ r' ] dest :: l';
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Osingleconst f, nil, dest, succ) ->
- debug "Iop/Osingleconst\n";
+ if exp_debug then eprintf "Iop/Osingleconst\n";
let r = r2pi () in
- let ht =
- loadimm32 r (Floats.Float32.to_bits f) (n2pi ()) map_consts true
- in
- let r' = unzip_head_tuple ht r in
- exp :=
- build_full_ilist Osingle_of_bits [ r' ] dest succ (fst ht) []
- map_consts;
+ let l = loadimm32 vn r (Floats.Float32.to_bits f) in
+ let r', l' = extract_arg l in
+ exp := addinst vn Osingle_of_bits [ r' ] dest :: l';
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ointconst n, nil, dest, succ) ->
- debug "Iop/Ointconst\n";
- let ht = loadimm32 dest n succ map_consts false in
- exp := unzip_head_tuple_move ht dest succ;
+ if exp_debug then eprintf "Iop/Ointconst\n";
+ exp := loadimm32 vn dest n;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Olongconst n, nil, dest, succ) ->
- debug "Iop/Olongconst\n";
- let ht = loadimm64 dest n succ map_consts false in
- exp := unzip_head_tuple_move ht dest succ;
+ if exp_debug then eprintf "Iop/Olongconst\n";
+ exp := loadimm64 vn dest n;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Oaddimm n, a1 :: nil, dest, succ) ->
- debug "Iop/Oaddimm\n";
- exp := addimm32 a1 dest n succ [] map_consts;
+ if exp_debug then eprintf "Iop/Oaddimm\n";
+ exp := addimm32 vn a1 dest n None;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Oaddlimm n, a1 :: nil, dest, succ) ->
- debug "Iop/Oaddlimm\n";
- exp := addimm64 a1 dest n succ [] map_consts;
+ if exp_debug then eprintf "Iop/Oaddlimm\n";
+ exp := addimm64 vn a1 dest n None;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Oandimm n, a1 :: nil, dest, succ) ->
- debug "Iop/Oandimm\n";
- exp := andimm32 a1 dest n succ [] map_consts;
+ if exp_debug then eprintf "Iop/Oandimm\n";
+ exp := andimm32 vn a1 dest n;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Oandlimm n, a1 :: nil, dest, succ) ->
- debug "Iop/Oandlimm\n";
- exp := andimm64 a1 dest n succ [] map_consts;
+ if exp_debug then eprintf "Iop/Oandlimm\n";
+ exp := andimm64 vn a1 dest n;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Oorimm n, a1 :: nil, dest, succ) ->
- debug "Iop/Oorimm\n";
- exp := orimm32 a1 dest n succ [] map_consts;
+ if exp_debug then eprintf "Iop/Oorimm\n";
+ exp := orimm32 vn a1 dest n;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Oorlimm n, a1 :: nil, dest, succ) ->
- debug "Iop/Oorlimm\n";
- exp := orimm64 a1 dest n succ [] map_consts;
+ if exp_debug then eprintf "Iop/Oorlimm\n";
+ exp := orimm64 vn a1 dest n;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocast8signed, a1 :: nil, dest, succ) ->
- debug "Iop/cast8signed";
+ if exp_debug then eprintf "Iop/cast8signed\n";
let op = Oshlimm (Int.repr (Z.of_sint 24)) in
let r = r2pi () in
- let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
+ let i1 = addinst vn op [ a1 ] r in
+ let r', l = extract_arg [ i1 ] in
exp :=
- build_full_ilist
- (Oshrimm (Int.repr (Z.of_sint 24)))
- [ r' ] dest succ (fst ht) [] map_consts;
+ addinst vn (Oshrimm (Int.repr (Z.of_sint 24))) [ r' ] dest :: l;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocast16signed, a1 :: nil, dest, succ) ->
- debug "Iop/cast8signed";
+ if exp_debug then eprintf "Iop/cast16signed\n";
let op = Oshlimm (Int.repr (Z.of_sint 16)) in
let r = r2pi () in
- let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in
- let ht = build_head_tuple [] sv in
- let r' = unzip_head_tuple ht r in
+ let i1 = addinst vn op [ a1 ] r in
+ let r', l = extract_arg [ i1 ] in
exp :=
- build_full_ilist
- (Oshrimm (Int.repr (Z.of_sint 16)))
- [ r' ] dest succ (fst ht) [] map_consts;
+ addinst vn (Oshrimm (Int.repr (Z.of_sint 16))) [ r' ] dest :: l;
+ exp := extract_final vn !exp dest succ;
was_exp := true
| Iop (Ocast32unsigned, a1 :: nil, dest, succ) ->
- debug "Iop/Ocast32unsigned";
- let n2 = n2pi () in
- let n1 = n2pi () in
+ if exp_debug then eprintf "Iop/Ocast32unsigned\n";
let r1 = r2pi () in
let r2 = r2pi () in
let op1 = Ocast32signed in
- let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
- let ht1 = build_head_tuple [] sv1 in
- let r1' = unzip_head_tuple ht1 r1 in
+ let i1 = addinst vn op1 [ a1 ] r1 in
+ let r1', l1 = extract_arg [ i1 ] in
let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in
- let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in
- let ht2 = build_head_tuple (fst ht1) sv2 in
- let r2' = unzip_head_tuple ht2 r2 in
+ let i2 = addinst vn op2 [ r1' ] r2 in
+ let r2', l2 = extract_arg (i2 :: l1) in
let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in
- exp := build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts
+ exp := addinst vn op3 [ r2' ] dest :: l2;
+ exp := extract_final vn !exp dest succ;
+ was_exp := true
| Iop (Oshrximm n, a1 :: nil, dest, succ) ->
- debug "Iop/Oshrximm";
- if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ]
- else if Int.eq n Int.one then
- let n2 = n2pi () in
- let n1 = n2pi () in
+ if Int.eq n Int.zero then (
+ if exp_debug then eprintf "Iop/Oshrximm1\n";
+ exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ])
+ else if Int.eq n Int.one then (
+ if exp_debug then eprintf "Iop/Oshrximm2\n";
let r1 = r2pi () in
let r2 = r2pi () in
let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in
- let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
- let ht1 = build_head_tuple [] sv1 in
- let r1' = unzip_head_tuple ht1 r1 in
+ let i1 = addinst vn op1 [ a1 ] r1 in
+ let r1', l1 = extract_arg [ i1 ] in
let op2 = Oadd in
- let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in
- let ht2 = build_head_tuple (fst ht1) sv2 in
- let r2' = unzip_head_tuple ht2 r2 in
+ let i2 = addinst vn op2 [ a1; r1' ] r2 in
+ let r2', l2 = extract_arg (i2 :: l1) in
let op3 = Oshrimm Int.one in
- exp :=
- build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts
- else
- let n3 = n2pi () in
- let n2 = n2pi () in
- let n1 = n2pi () in
+ let i3 = addinst vn op3 [ r2' ] dest in
+ let r3, l3 = extract_arg (i3 :: l2) in
+ exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3)
+ else (
+ if exp_debug then eprintf "Iop/Oshrximm3\n";
let r1 = r2pi () in
let r2 = r2pi () in
let r3 = r2pi () in
let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in
- let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
- let ht1 = build_head_tuple [] sv1 in
- let r1' = unzip_head_tuple ht1 r1 in
+ let i1 = addinst vn op1 [ a1 ] r1 in
+ let r1', l1 = extract_arg [ i1 ] in
let op2 = Oshruimm (Int.sub Int.iwordsize n) in
- let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in
- let ht2 = build_head_tuple (fst ht1) sv2 in
- let r2' = unzip_head_tuple ht2 r2 in
+ let i2 = addinst vn op2 [ r1' ] r2 in
+ let r2', l2 = extract_arg (i2 :: l1) in
let op3 = Oadd in
- let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in
- let ht3 = build_head_tuple (fst ht2) sv3 in
- let r3' = unzip_head_tuple ht3 r3 in
+ let i3 = addinst vn op3 [ a1; r2' ] r3 in
+ let r3', l3 = extract_arg (i3 :: l2) in
let op4 = Oshrimm n in
- exp :=
- build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts
+ let i4 = addinst vn op4 [ r3' ] dest in
+ let r4, l4 = extract_arg (i4 :: l3) in
+ exp := addinst vn (OEmayundef (MUshrx n)) [ r4; r4 ] dest :: l4);
+ exp := extract_final vn !exp dest succ;
+ was_exp := true
| Iop (Oshrxlimm n, a1 :: nil, dest, succ) ->
- debug "Iop/Oshrxlimm";
- if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ]
- else if Int.eq n Int.one then
- let n2 = n2pi () in
- let n1 = n2pi () in
+ if Int.eq n Int.zero then (
+ if exp_debug then eprintf "Iop/Oshrxlimm1\n";
+ exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ])
+ else if Int.eq n Int.one then (
+ if exp_debug then eprintf "Iop/Oshrxlimm2\n";
let r1 = r2pi () in
let r2 = r2pi () in
let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in
- let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
- let ht1 = build_head_tuple [] sv1 in
- let r1' = unzip_head_tuple ht1 r1 in
+ let i1 = addinst vn op1 [ a1 ] r1 in
+ let r1', l1 = extract_arg [ i1 ] in
let op2 = Oaddl in
- let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in
- let ht2 = build_head_tuple (fst ht1) sv2 in
- let r2' = unzip_head_tuple ht2 r2 in
+ let i2 = addinst vn op2 [ a1; r1' ] r2 in
+ let r2', l2 = extract_arg (i2 :: l1) in
let op3 = Oshrlimm Int.one in
- exp :=
- build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts
- else
- let n3 = n2pi () in
- let n2 = n2pi () in
- let n1 = n2pi () in
+ let i3 = addinst vn op3 [ r2' ] dest in
+ let r3, l3 = extract_arg (i3 :: l2) in
+ exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3)
+ else (
+ if exp_debug then eprintf "Iop/Oshrxlimm3\n";
let r1 = r2pi () in
let r2 = r2pi () in
let r3 = r2pi () in
let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in
- let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in
- let ht1 = build_head_tuple [] sv1 in
- let r1' = unzip_head_tuple ht1 r1 in
+ let i1 = addinst vn op1 [ a1 ] r1 in
+ let r1', l1 = extract_arg [ i1 ] in
let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in
- let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in
- let ht2 = build_head_tuple (fst ht1) sv2 in
- let r2' = unzip_head_tuple ht2 r2 in
+ let i2 = addinst vn op2 [ r1' ] r2 in
+ let r2', l2 = extract_arg (i2 :: l1) in
let op3 = Oaddl in
- let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in
- let ht3 = build_head_tuple (fst ht2) sv3 in
- let r3' = unzip_head_tuple ht3 r3 in
+ let i3 = addinst vn op3 [ a1; r2' ] r3 in
+ let r3', l3 = extract_arg (i3 :: l2) in
let op4 = Oshrlimm n in
- exp :=
- build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts
+ let i4 = addinst vn op4 [ r3' ] dest in
+ let r4, l4 = extract_arg (i4 :: l3) in
+ exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4);
+ exp := extract_final vn !exp dest succ;
+ was_exp := true
+ (*| Iop (Oaddrstack n, nil, dest, succ) ->*)
+ (*if exp_debug then eprintf "Iop/Oaddrstack\n";*)
+ (*exp := addptrofs vn n dest;*)
+ (*exp := extract_final vn !exp dest succ;*)
+ (*was_exp := true*)
| _ -> ());
+ (* Update the CSE numbering *)
+ (if not !was_exp then
+ match inst with
+ | Iop (op, args, dest, succ) ->
+ let v = get_nvalues vn args in
+ addsop vn v op dest
+ | Iload (_, _, _, _, dst, _) -> set_unknown vn dst
+ | Istore (chk, addr, args, src, s) ->
+ !vn.seqs <- kill_mem_operations !vn.seqs
+ | Icall (_, _, _, _, _) | Itailcall (_, _, _) | Ibuiltin (_, _, _, _) ->
+ vn := empty_numbering ()
+ | _ -> ());
+ (* Update code, liveins, pathmap, and order of the superblock for one expansion *)
if !was_exp then (
+ node := !node + List.length !exp - 1;
(if !was_branch && List.length !exp > 1 then
let lives = PTree.get n !liveins in
match lives with
@@ -880,14 +1063,15 @@ let expanse (sb : superblock) code pm =
liveins := PTree.remove n !liveins
| _ -> ());
write_pathmap sb.instructions.(0) (List.length !exp - 1) pm';
- write_tree !exp n !node code' new_order true)
+ write_tree vn (List.rev !exp) n !node code' new_order true)
else new_order := n :: !new_order)
sb.instructions;
sb.instructions <- Array.of_list (List.rev !new_order);
sb.liveins <- !liveins;
- (*debug_flag := false;*)
(!code', !pm')
+(** Compute the last used node and reg indexs *)
+
let rec find_last_node_reg = function
| [] -> ()
| (pc, i) :: k ->
diff --git a/riscV/NeedOp.v b/riscV/NeedOp.v
index 715951a0..d0ca5bb2 100644
--- a/riscV/NeedOp.v
+++ b/riscV/NeedOp.v
@@ -87,7 +87,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| Ointofsingle | Ointuofsingle | Osingleofint | Osingleofintu => op1 (default nv)
| Olongofsingle | Olonguofsingle | Osingleoflong | Osingleoflongu => op1 (default nv)
| Ocmp c => needs_of_condition c
- | OEimmR0 _ => op1 (default nv)
+ | OEmoveSP => nil
| OEseqw _ => op2 (default nv)
| OEsnew _ => op2 (default nv)
| OEsequw _ => op2 (default nv)
@@ -98,7 +98,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| OEsltiuw _ => op1 (default nv)
| OExoriw _ => op1 (bitwise nv)
| OEluiw _ => op1 (default nv)
- | OEaddiw _ => op1 (default nv)
+ | OEaddiw _ _ => op1 (default nv)
| OEandiw n => op1 (andimm nv n)
| OEoriw n => op1 (orimm nv n)
| OEseql _ => op2 (default nv)
@@ -111,7 +111,7 @@ Definition needs_of_operation (op: operation) (nv: nval): list nval :=
| OEsltiul _ => op1 (default nv)
| OExoril _ => op1 (default nv)
| OEluil _ => op1 (default nv)
- | OEaddil _ => op1 (default nv)
+ | OEaddil _ _ => op1 (default nv)
| OEandil _ => op1 (default nv)
| OEoril _ => op1 (default nv)
| OEloadli _ => op1 (default nv)
diff --git a/riscV/Op.v b/riscV/Op.v
index a8ff3666..9d1826ac 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -38,10 +38,12 @@ Set Implicit Arguments.
(** Conditions (boolean-valued operators). *)
-(* Type to modelize the use of a special register in arith operations *)
+(** Type to modelize the use of a special register in arith operations *)
+
Inductive oreg: Type :=
| X0_L: oreg
- | X0_R: oreg.
+ | X0_R: oreg
+ | SP_S: oreg.
Inductive condition : Type :=
| Ccomp (c: comparison) (**r signed integer comparison *)
@@ -75,17 +77,13 @@ Inductive condition : Type :=
| CEbgeul (optR: option oreg). (**r branch-if-greater-or-equal unsigned *)
(* This type will define the eval function of a OEmayundef operation. *)
+
Inductive mayundef: Type :=
| MUint: mayundef
| MUlong: mayundef
| MUshrx: int -> mayundef
| MUshrxl: int -> mayundef.
-(* Type for allowing a single RTL constructor to perform an arith operation between an immediate and X0 *)
-Inductive opimm: Type :=
- | OPimmADD: int -> opimm
- | OPimmADDL: int64 -> opimm.
-
(** Arithmetic and logical operations. In the descriptions, [rd] is the
result of the operation and [r1], [r2], etc, are the arguments. *)
@@ -189,41 +187,41 @@ Inductive operation : Type :=
(*c Boolean tests: *)
| Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *)
(* Expansed conditions *)
- | OEimmR0 (opi: opimm)
+ | OEmoveSP
| OEseqw (optR: option oreg) (**r [rd <- rs1 == rs2] signed *)
| OEsnew (optR: option oreg) (**r [rd <- rs1 != rs2] signed *)
| OEsequw (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *)
| OEsneuw (optR: option oreg) (**r [rd <- rs1 != rs2] unsigned *)
| OEsltw (optR: option oreg) (**r set-less-than *)
| OEsltuw (optR: option oreg) (**r set-less-than unsigned *)
- | OEsltiw (n: int) (**r set-less-than immediate *)
- | OEsltiuw (n: int) (**r set-less-than unsigned immediate *)
- | OEaddiw (n: int) (**r add immediate *)
- | OEandiw (n: int) (**r and immediate *)
- | OEoriw (n: int) (**r or immediate *)
- | OExoriw (n: int) (**r xor immediate *)
- | OEluiw (n: int) (**r load upper-immediate *)
+ | OEsltiw (n: int) (**r set-less-than immediate *)
+ | OEsltiuw (n: int) (**r set-less-than unsigned immediate *)
+ | OEaddiw (optR: option oreg) (n: int) (**r add immediate *)
+ | OEandiw (n: int) (**r and immediate *)
+ | OEoriw (n: int) (**r or immediate *)
+ | OExoriw (n: int) (**r xor immediate *)
+ | OEluiw (n: int) (**r load upper-immediate *)
| OEseql (optR: option oreg) (**r [rd <- rs1 == rs2] signed *)
| OEsnel (optR: option oreg) (**r [rd <- rs1 != rs2] signed *)
| OEsequl (optR: option oreg) (**r [rd <- rs1 == rs2] unsigned *)
| OEsneul (optR: option oreg) (**r [rd <- rs1 != rs2] unsigned *)
| OEsltl (optR: option oreg) (**r set-less-than *)
| OEsltul (optR: option oreg) (**r set-less-than unsigned *)
- | OEsltil (n: int64) (**r set-less-than immediate *)
- | OEsltiul (n: int64) (**r set-less-than unsigned immediate *)
- | OEaddil (n: int64) (**r add immediate *)
- | OEandil (n: int64) (**r and immediate *)
- | OEoril (n: int64) (**r or immediate *)
- | OExoril (n: int64) (**r xor immediate *)
- | OEluil (n: int64) (**r load upper-immediate *)
- | OEloadli (n: int64) (**r load an immediate int64 *)
+ | OEsltil (n: int64) (**r set-less-than immediate *)
+ | OEsltiul (n: int64) (**r set-less-than unsigned immediate *)
+ | OEaddil (optR: option oreg) (n: int64) (**r add immediate *)
+ | OEandil (n: int64) (**r and immediate *)
+ | OEoril (n: int64) (**r or immediate *)
+ | OExoril (n: int64) (**r xor immediate *)
+ | OEluil (n: int64) (**r load upper-immediate *)
+ | OEloadli (n: int64) (**r load an immediate int64 *)
| OEmayundef (mu: mayundef)
- | OEfeqd (**r compare equal *)
- | OEfltd (**r compare less-than *)
- | OEfled (**r compare less-than/equal *)
- | OEfeqs (**r compare equal *)
- | OEflts (**r compare less-than *)
- | OEfles (**r compare less-than/equal *)
+ | OEfeqd (**r compare equal *)
+ | OEfltd (**r compare less-than *)
+ | OEfled (**r compare less-than/equal *)
+ | OEfeqs (**r compare equal *)
+ | OEflts (**r compare less-than *)
+ | OEfles (**r compare less-than/equal *)
| Obits_of_single
| Obits_of_float
| Osingle_of_bits
@@ -277,47 +275,46 @@ Defined.
*)
Global Opaque eq_condition eq_addressing eq_operation.
+
+(** Generic function to evaluate an instruction according to the given specific register *)
Definition zero32 := (Vint Int.zero).
Definition zero64 := (Vlong Int64.zero).
-Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz: val): B :=
+Definition apply_bin_oreg {B} (optR: option oreg) (sem: val -> val -> B) (v1 v2 vz sp: val): B :=
match optR with
| None => sem v1 v2
| Some X0_L => sem vz v1
| Some X0_R => sem v1 vz
+ | Some SP_S => sem v1 sp
end.
+(** Mayundef evaluation according to the above defined type *)
+
Definition eval_may_undef (mu: mayundef) (v1 v2: val): val :=
match mu with
- | MUint => match v1 with
- | Vint _ => v2
- | _ => Vundef
+ | MUint => match v1, v2 with
+ | Vint _, Vint _ => v2
+ | _, _ => Vundef
end
- | MUlong => match v1 with
- | Vlong _ => v2
- | _ => Vundef
+ | MUlong => match v1, v2 with
+ | Vlong _, Vint _ => v2
+ | _, _ => Vundef
end
| MUshrx i =>
- match v1 with
- | Vint _ =>
- if Int.ltu i (Int.repr 31) then v1 else Vundef
- | _ => Vundef
+ match v1, v2 with
+ | Vint _, Vint _ =>
+ if Int.ltu i (Int.repr 31) then v2 else Vundef
+ | _, _ => Vundef
end
| MUshrxl i =>
- match v1 with
- | Vlong _ =>
- if Int.ltu i (Int.repr 63) then v1 else Vundef
- | _ => Vundef
+ match v1, v2 with
+ | Vlong _, Vlong _ =>
+ if Int.ltu i (Int.repr 63) then v2 else Vundef
+ | _, _ => Vundef
end
end.
-Definition eval_opimmR0 (opi: opimm): val :=
- match opi with
- | OPimmADD i => Val.add (Vint i) zero32
- | OPimmADDL i => Val.addl (Vlong i) zero64
- end.
-
(** * Evaluation functions *)
(** Evaluation of conditions, operators and addressing modes applied
@@ -340,25 +337,33 @@ Definition eval_condition (cond: condition) (vl: list val) (m: mem): option bool
| Ccompfs c, v1 :: v2 :: nil => Val.cmpfs_bool c v1 v2
| Cnotcompfs c, v1 :: v2 :: nil => option_map negb (Val.cmpfs_bool c v1 v2)
(* Expansed branches *)
- | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32
- | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32
- | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32
- | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32
- | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32
- | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32
- | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32
- | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32
- | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64
- | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64
- | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64
- | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64
- | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64
- | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64
- | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64
- | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64
+ | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Ceq) v1 v2 zero32 Vundef
+ | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cne) v1 v2 zero32 Vundef
+ | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef
+ | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef
+ | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Clt) v1 v2 zero32 Vundef
+ | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef
+ | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmp_bool Cge) v1 v2 zero32 Vundef
+ | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpu_bool (Mem.valid_pointer m) Cge) v1 v2 zero32 Vundef
+ | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Ceq) v1 v2 zero64 Vundef
+ | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cne) v1 v2 zero64 Vundef
+ | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef
+ | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef
+ | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Clt) v1 v2 zero64 Vundef
+ | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef
+ | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmpl_bool Cge) v1 v2 zero64 Vundef
+ | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (Val.cmplu_bool (Mem.valid_pointer m) Cge) v1 v2 zero64 Vundef
| _, _ => None
end.
+(** Assert sp is a pointer *)
+
+Definition get_sp sp :=
+ match sp with
+ | Vptr _ _ => sp
+ | _ => Vundef
+ end.
+
Definition eval_operation
(F V: Type) (genv: Genv.t F V) (sp: val)
(op: operation) (vl: list val) (m: mem): option val :=
@@ -461,31 +466,41 @@ Definition eval_operation
| Ofloat_of_bits, v1::nil => Some (ExtValues.float_of_bits v1)
| Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m))
(* Expansed conditions *)
- | OEimmR0 opi, nil => Some (eval_opimmR0 opi)
- | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32)
- | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32)
- | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32)
- | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32)
- | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32)
- | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32)
+ | OEmoveSP, nil => Some (get_sp sp)
+ | OEseqw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Ceq) v1 v2 zero32 Vundef)
+ | OEsnew optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Cne) v1 v2 zero32 Vundef)
+ | OEsequw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Ceq) v1 v2 zero32 Vundef)
+ | OEsneuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Cne) v1 v2 zero32 Vundef)
+ | OEsltw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmp Clt) v1 v2 zero32 Vundef)
+ | OEsltuw optR, v1::v2::nil => Some (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) Clt) v1 v2 zero32 Vundef)
| OEsltiw n, v1::nil => Some (Val.cmp Clt v1 (Vint n))
| OEsltiuw n, v1::nil => Some (Val.cmpu (Mem.valid_pointer m) Clt v1 (Vint n))
| OExoriw n, v1::nil => Some (Val.xor v1 (Vint n))
| OEluiw n, nil => Some (Val.shl (Vint n) (Vint (Int.repr 12)))
- | OEaddiw n, v1::nil => Some (Val.add (Vint n) v1)
+ | OEaddiw optR n, nil => Some (apply_bin_oreg optR Val.add (Vint n) Vundef zero32 Vundef)
+ | OEaddiw ((Some SP_S) as optR) n, v1::nil =>
+ let sp' := Val.add (Vint n) (get_sp sp) in
+ Some (apply_bin_oreg optR Val.add v1 Vundef Vundef sp')
+ | OEaddiw optR n, v1::nil =>
+ Some (apply_bin_oreg optR Val.add v1 (Vint n) Vundef (get_sp sp))
| OEandiw n, v1::nil => Some (Val.and (Vint n) v1)
| OEoriw n, v1::nil => Some (Val.or (Vint n) v1)
- | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64))
- | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64))
- | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64))
- | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64))
- | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64))
- | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64))
+ | OEseql optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Ceq) v1 v2 zero64 Vundef))
+ | OEsnel optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Cne) v1 v2 zero64 Vundef))
+ | OEsequl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Ceq) v1 v2 zero64 Vundef))
+ | OEsneul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Cne) v1 v2 zero64 Vundef))
+ | OEsltl optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmpl Clt) v1 v2 zero64 Vundef))
+ | OEsltul optR, v1::v2::nil => Some (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) Clt) v1 v2 zero64 Vundef))
| OEsltil n, v1::nil => Some (Val.maketotal (Val.cmpl Clt v1 (Vlong n)))
| OEsltiul n, v1::nil => Some (Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 (Vlong n)))
| OExoril n, v1::nil => Some (Val.xorl v1 (Vlong n))
| OEluil n, nil => Some (Vlong (Int64.sign_ext 32 (Int64.shl n (Int64.repr 12))))
- | OEaddil n, v1::nil => Some (Val.addl (Vlong n) v1)
+ | OEaddil optR n, nil => Some (apply_bin_oreg optR Val.addl (Vlong n) Vundef zero64 Vundef)
+ | OEaddil ((Some SP_S) as optR) n, v1::nil =>
+ let sp' := Val.addl (Vlong n) (get_sp sp) in
+ Some (apply_bin_oreg optR Val.addl v1 Vundef Vundef sp')
+ | OEaddil optR n, v1::nil =>
+ Some (apply_bin_oreg optR Val.addl v1 (Vlong n) Vundef (get_sp sp))
| OEandil n, v1::nil => Some (Val.andl (Vlong n) v1)
| OEoril n, v1::nil => Some (Val.orl (Vlong n) v1)
| OEloadli n, nil => Some (Vlong n)
@@ -574,12 +589,23 @@ Definition type_of_condition (c: condition) : list typ :=
| CEbgeul _ => Tlong :: Tlong :: nil
end.
-Definition type_of_opimmR0 (opi: opimm) : typ :=
- match opi with
- | OPimmADD _ => Tint
- | OPimmADDL _ => Tlong
+(** The type of mayundef and addsp is dynamic *)
+
+Definition type_of_mayundef mu :=
+ match mu with
+ | MUint | MUshrx _ => (Tint :: Tint :: nil, Tint)
+ | MUlong => (Tlong :: Tint :: nil, Tint)
+ | MUshrxl _ => (Tlong :: Tlong :: nil, Tlong)
end.
+Definition type_addsp (is_long: bool): list typ * typ :=
+ if Archi.ptr64 then (
+ if is_long then (Tlong :: nil, Tptr)
+ else (nil, Tint))
+ else (
+ if is_long then (nil, Tlong)
+ else (Tint :: nil, Tptr)).
+
Definition type_of_operation (op: operation) : list typ * typ :=
match op with
| Omove => (nil, Tint) (* treated specially *)
@@ -675,7 +701,7 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| Osingleoflong => (Tlong :: nil, Tsingle)
| Osingleoflongu => (Tlong :: nil, Tsingle)
| Ocmp c => (type_of_condition c, Tint)
- | OEimmR0 opi => (nil, type_of_opimmR0 opi)
+ | OEmoveSP => (nil, Tptr)
| OEseqw _ => (Tint :: Tint :: nil, Tint)
| OEsnew _ => (Tint :: Tint :: nil, Tint)
| OEsequw _ => (Tint :: Tint :: nil, Tint)
@@ -686,7 +712,9 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| OEsltiuw _ => (Tint :: nil, Tint)
| OExoriw _ => (Tint :: nil, Tint)
| OEluiw _ => (nil, Tint)
- | OEaddiw _ => (Tint :: nil, Tint)
+ | OEaddiw None _ => (Tint :: nil, Tint)
+ | OEaddiw (Some SP_S) _ => type_addsp false
+ | OEaddiw (Some _) _ => (nil, Tint)
| OEandiw _ => (Tint :: nil, Tint)
| OEoriw _ => (Tint :: nil, Tint)
| OEseql _ => (Tlong :: Tlong :: nil, Tint)
@@ -701,9 +729,11 @@ Definition type_of_operation (op: operation) : list typ * typ :=
| OEoril _ => (Tlong :: nil, Tlong)
| OExoril _ => (Tlong :: nil, Tlong)
| OEluil _ => (nil, Tlong)
- | OEaddil _ => (Tlong :: nil, Tlong)
+ | OEaddil None _ => (Tlong :: nil, Tlong)
+ | OEaddil (Some SP_S) _ => type_addsp true
+ | OEaddil (Some _) _ => (nil, Tlong)
| OEloadli _ => (nil, Tlong)
- | OEmayundef _ => (Tany64 :: Tany64 :: nil, Tany64)
+ | OEmayundef mu => type_of_mayundef mu
| OEfeqd => (Tfloat :: Tfloat :: nil, Tint)
| OEfltd => (Tfloat :: Tfloat :: nil, Tint)
| OEfled => (Tfloat :: Tfloat :: nil, Tint)
@@ -746,7 +776,7 @@ Proof.
Qed.
Remark type_mayundef:
- forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) Tany64.
+ forall mu v1 v2, Val.has_type (eval_may_undef mu v1 v2) (snd (type_of_mayundef mu)).
Proof.
intros. unfold eval_may_undef.
destruct mu eqn:EQMU, v1, v2; simpl; auto.
@@ -762,7 +792,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
intros.
destruct op; simpl; simpl in H0; FuncInv; subst; simpl.
(* move *)
- - congruence.
+ - simpl in H; congruence.
(* intconst, longconst, floatconst, singleconst *)
- exact I.
- exact I.
@@ -929,8 +959,9 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
- destruct v0; cbn; trivial.
(* cmp *)
- destruct (eval_condition cond vl m)... destruct b...
- (* OEimmR0 *)
- - destruct opi; unfold eval_opimmR0; simpl; auto.
+ (* OEmoveSP *)
+ - destruct sp; unfold Tptr; destruct Archi.ptr64 eqn:?;
+ simpl; trivial.
(* OEseqw *)
- destruct optR as [[]|]; simpl; unfold Val.cmp;
destruct Val.cmp_bool... all: destruct b...
@@ -955,7 +986,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
(* OEsltiuw *)
- unfold Val.cmpu; destruct Val.cmpu_bool... destruct b...
(* OEaddiw *)
- - fold (Val.add (Vint n) v0); apply type_add.
+ - destruct optR as [[]|]; simpl in *; trivial;
+ destruct vl; inv H0; simpl; trivial;
+ destruct vl; inv H2; simpl; trivial;
+ destruct v0; simpl; trivial;
+ destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial;
+ unfold type_addsp, Tptr; try rewrite HA; simpl; trivial.
(* OEandiw *)
- destruct v0...
(* OEoriw *)
@@ -988,7 +1024,12 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
(* OEsltiul *)
- unfold Val.cmplu; destruct Val.cmplu_bool... destruct b...
(* OEaddil *)
- - fold (Val.addl (Vlong n) v0); apply type_addl.
+ - destruct optR as [[]|]; simpl in *; trivial;
+ destruct vl; inv H0; simpl; trivial;
+ destruct vl; inv H2; simpl; trivial;
+ destruct v0; simpl; trivial;
+ destruct (get_sp sp); destruct Archi.ptr64 eqn:HA; simpl; trivial;
+ unfold type_addsp, Tptr; try rewrite HA; simpl; trivial.
(* OEandil *)
- destruct v0...
(* OEoril *)
@@ -1052,11 +1093,15 @@ Lemma is_trapping_op_sound:
eval_operation genv sp op vl m <> None.
Proof.
unfold args_of_operation.
- destruct op; destruct eq_operation; intros; simpl in *; try congruence.
+ destruct op eqn:E; destruct eq_operation; intros; simpl in *; try congruence.
all: try (destruct vl as [ | vh1 vl1]; try discriminate).
all: try (destruct vl1 as [ | vh2 vl2]; try discriminate).
all: try (destruct vl2 as [ | vh3 vl3]; try discriminate).
all: try (destruct vl3 as [ | vh4 vl4]; try discriminate).
+ all: try destruct optR as [[]|]; simpl in H0; try discriminate.
+ all: unfold type_addsp in *; simpl in *.
+ all: try destruct Archi.ptr64; simpl in *; try discriminate.
+ all: try destruct mu; simpl in *; try discriminate.
Qed.
End SOUNDNESS.
@@ -1181,6 +1226,9 @@ Definition shift_stack_addressing (delta: Z) (addr: addressing) :=
Definition shift_stack_operation (delta: Z) (op: operation) :=
match op with
| Oaddrstack ofs => Oaddrstack (Ptrofs.add ofs (Ptrofs.repr delta))
+ | OEmoveSP => Oaddrstack (Ptrofs.add Ptrofs.zero (Ptrofs.repr delta))
+ | OEaddiw (Some SP_S) n => OEaddiw (Some SP_S) (Ptrofs.to_int (Ptrofs.add (Ptrofs.of_int n) (Ptrofs.repr delta)))
+ | OEaddil (Some SP_S) n => OEaddil (Some SP_S) (Ptrofs.to_int64 (Ptrofs.add (Ptrofs.of_int64 n) (Ptrofs.repr delta)))
| _ => op
end.
@@ -1193,7 +1241,8 @@ Qed.
Lemma type_shift_stack_operation:
forall delta op, type_of_operation (shift_stack_operation delta op) = type_of_operation op.
Proof.
- intros. destruct op; auto.
+ intros. destruct op; auto;
+ try destruct optR as [[]|]; simpl; auto.
Qed.
Lemma eval_shift_stack_addressing:
@@ -1210,8 +1259,21 @@ Lemma eval_shift_stack_operation:
eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m =
eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m.
Proof.
- intros. destruct op; simpl; auto. destruct vl; auto.
- rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
+ intros. destruct op eqn:E; simpl; auto; destruct vl; auto.
+ - rewrite Ptrofs.add_zero_l, Ptrofs.add_commut; auto.
+ - rewrite !Ptrofs.add_zero_l; auto.
+ - destruct optR as [[]|]; simpl; auto.
+ - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto.
+ destruct v, Archi.ptr64 eqn:EA; simpl; try rewrite EA; simpl; auto.
+ rewrite Ptrofs.add_zero_l; auto.
+ rewrite Ptrofs.of_int_to_int; auto.
+ rewrite (Ptrofs.add_commut (Ptrofs.of_int n) (Ptrofs.repr delta)); reflexivity.
+ - destruct optR as [[]|]; simpl; auto.
+ - destruct vl, optR as [[]|]; auto; unfold apply_bin_oreg; simpl; auto.
+ destruct Archi.ptr64 eqn:EA; auto.
+ rewrite Ptrofs.add_zero_l; auto.
+ rewrite Ptrofs.of_int64_to_int64; auto.
+ rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n) (Ptrofs.repr delta)); reflexivity.
Qed.
(** Offset an addressing mode [addr] by a quantity [delta], so that
@@ -1471,8 +1533,8 @@ Qed.
Lemma eval_cmpu_bool_inj_opt: forall c v v' v0 v'0 optR,
Val.inject f v v' ->
Val.inject f v0 v'0 ->
- Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32)
- (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32).
+ Val.inject f (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m1) c) v v0 zero32 Vundef)
+ (apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m2) c) v' v'0 zero32 Vundef).
Proof.
intros until optR. intros HV1 HV2.
destruct optR as [[]|]; simpl; unfold zero32, Val.cmpu;
@@ -1482,6 +1544,9 @@ Proof.
intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+ exploit eval_cmpu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+ + exploit eval_cmpu_bool_inj'. eapply HV1. do 2 instantiate (1:=Vundef).
+ eauto. eapply Heqo.
+ intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+ exploit eval_cmpu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
Qed.
@@ -1512,8 +1577,8 @@ Qed.
Lemma eval_cmplu_bool_inj_opt: forall c v v' v0 v'0 optR,
Val.inject f v v' ->
Val.inject f v0 v'0 ->
- Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64))
- (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64)).
+ Val.inject f (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m1) c) v v0 zero64 Vundef))
+ (Val.maketotal (apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m2) c) v' v'0 zero64 Vundef)).
Proof.
intros until optR. intros HV1 HV2.
destruct optR as [[]|]; simpl; unfold zero64, Val.cmplu;
@@ -1523,6 +1588,9 @@ Proof.
intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+ exploit eval_cmplu_bool_inj'. eapply HV1. eapply HVI. eapply Heqo.
intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+ + exploit eval_cmplu_bool_inj'. eapply HV1. do 2 instantiate (1:=Vundef).
+ eauto. eapply Heqo.
+ intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
+ exploit eval_cmplu_bool_inj'. eapply HV1. eapply HV2. eapply Heqo.
intros EQ; rewrite EQ; destruct b; simpl; constructor; eauto.
Qed.
@@ -1789,8 +1857,9 @@ Proof.
exploit eval_condition_inj; eauto. intros EQ; rewrite EQ.
destruct b; simpl; constructor.
simpl; constructor.
- (* OEimmR0 *)
- - destruct opi; unfold eval_opimmR0; simpl; auto.
+ (* moveSP *)
+ - unfold get_sp; inv H; auto.
+ econstructor; eauto.
(* OEseqw *)
- destruct optR as [[]|]; simpl; unfold zero32, Val.cmp;
inv H4; inv H2; simpl; try destruct (Int.eq _ _); simpl; cbn; auto;
@@ -1814,9 +1883,14 @@ Proof.
(* OEsltiuw *)
- apply eval_cmpu_bool_inj; auto.
(* OEaddiw *)
- - fold (Val.add (Vint n) v);
- fold (Val.add (Vint n) v');
+ - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists;
+ try fold (Val.add (Vint n) (get_sp sp1));
+ try fold (Val.add (Vint n) (get_sp sp2));
+ (*try destruct (get_sp sp1), (get_sp sp2);*)
apply Val.add_inject; auto.
+ apply Val.add_inject; auto.
+ destruct sp1, sp2; simpl; auto;
+ inv H.
(* OEandiw *)
- inv H4; cbn; auto.
(* OEoriw *)
@@ -1848,9 +1922,13 @@ Proof.
(* OEsltiul *)
- apply eval_cmplu_bool_inj; auto.
(* OEaddil *)
- - fold (Val.addl (Vlong n) v);
- fold (Val.addl (Vlong n) v');
+ - destruct optR as [[]|]; auto; simpl; FuncInv; InvInject; TrivialExists;
+ try fold (Val.addl (Vlong n) (get_sp sp1));
+ try fold (Val.addl (Vlong n) (get_sp sp2));
+ apply Val.addl_inject; auto.
apply Val.addl_inject; auto.
+ destruct sp1, sp2; simpl; auto;
+ inv H.
(* OEandil *)
- inv H4; cbn; auto.
(* OEoril *)
diff --git a/riscV/PrintOp.ml b/riscV/PrintOp.ml
index e18d31f6..53730a1b 100644
--- a/riscV/PrintOp.ml
+++ b/riscV/PrintOp.ml
@@ -36,14 +36,16 @@ let mu_name pp = function
| MUshrx i -> fprintf pp "MUshrx(%ld)" (camlint_of_coqint i)
| MUshrxl i -> fprintf pp "MUshrxl(%ld)" (camlint_of_coqint i)
-let get_immR0 pp = function
- | OPimmADD i -> fprintf pp "OPimmADD(%ld)" (camlint_of_coqint i)
- | OPimmADDL i -> fprintf pp "OPimmADDL(%ld)" (camlint_of_coqint i)
-
let get_optR_s c reg pp r1 r2 = function
| None -> fprintf pp "(%a %s %a)" reg r1 (comparison_name c) reg r2
| Some X0_L -> fprintf pp "(X0 %s %a)" (comparison_name c) reg r1
| Some X0_R -> fprintf pp "(%a %s X0)" reg r1 (comparison_name c)
+ | Some SP_S -> failwith "PrintOp: SP_S in get_optR_s instruction (problem with RTL expansions?)"
+
+let get_optR_a pp = function
+ | None -> failwith "PrintOp: None in get_optR_a instruction (problem with RTL expansions?)"
+ | Some X0_L | Some X0_R -> fprintf pp "X0"
+ | Some SP_S -> fprintf pp "SP"
let print_condition reg pp = function
| (Ccomp c, [r1;r2]) ->
@@ -203,7 +205,6 @@ let print_operation reg pp = function
| Osingleoflong, [r1] -> fprintf pp "singleoflong(%a)" reg r1
| Osingleoflongu, [r1] -> fprintf pp "singleoflongu(%a)" reg r1
| Ocmp c, args -> print_condition reg pp (c, args)
- | OEimmR0 opi, [] -> fprintf pp "OEimmR0(%a)" get_immR0 opi
| OEseqw optR, [r1;r2] -> fprintf pp "OEseqw"; (get_optR_s Ceq reg pp r1 r2 optR)
| OEsnew optR, [r1;r2] -> fprintf pp "OEsnew"; (get_optR_s Cne reg pp r1 r2 optR)
| OEsequw optR, [r1;r2] -> fprintf pp "OEsequw"; (get_optR_s Ceq reg pp r1 r2 optR)
@@ -214,7 +215,8 @@ let print_operation reg pp = function
| OEsltiuw n, [r1] -> fprintf pp "OEsltiuw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OExoriw n, [r1] -> fprintf pp "OExoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEluiw n, _ -> fprintf pp "OEluiw(%ld)" (camlint_of_coqint n)
- | OEaddiw n, [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n)
+ | OEaddiw (optR, n), [] -> fprintf pp "OEaddiw(%a,%ld)" get_optR_a optR (camlint_of_coqint n)
+ | OEaddiw (optR, n), [r1] -> fprintf pp "OEaddiw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEandiw n, [r1] -> fprintf pp "OEandiw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEoriw n, [r1] -> fprintf pp "OEoriw(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEseql optR, [r1;r2] -> fprintf pp "OEseql"; (get_optR_s Ceq reg pp r1 r2 optR)
@@ -227,7 +229,8 @@ let print_operation reg pp = function
| OEsltiul n, [r1] -> fprintf pp "OEsltiul(%a,%ld)" reg r1 (camlint_of_coqint n)
| OExoril n, [r1] -> fprintf pp "OExoril(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEluil n, _ -> fprintf pp "OEluil(%ld)" (camlint_of_coqint n)
- | OEaddil n, [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n)
+ | OEaddil (optR, n), [] -> fprintf pp "OEaddil(%a,%ld)" get_optR_a optR (camlint_of_coqint n)
+ | OEaddil (optR, n), [r1] -> fprintf pp "OEaddil(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEandil n, [r1] -> fprintf pp "OEandil(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEoril n, [r1] -> fprintf pp "OEoril(%a,%ld)" reg r1 (camlint_of_coqint n)
| OEloadli n, _ -> fprintf pp "OEloadli(%ld)" (camlint_of_coqint n)
diff --git a/riscV/RTLpathSE_simplify.v b/riscV/RTLpathSE_simplify.v
index 5b44caba..c453dfb8 100644
--- a/riscV/RTLpathSE_simplify.v
+++ b/riscV/RTLpathSE_simplify.v
@@ -30,9 +30,9 @@ Definition make_lhsv_cmp (is_inv: bool) (hv1 hv2: hsval) : list_hsval :=
Definition make_lhsv_single (hvs: hsval) : list_hsval :=
fScons hvs fSnil.
-(** Expansion functions *)
+(** * Expansion functions *)
-(* Immediate loads *)
+(** ** Immediate loads *)
Definition load_hilo32 (hi lo: int) :=
if Int.eq lo Int.zero then
@@ -40,7 +40,7 @@ Definition load_hilo32 (hi lo: int) :=
else
let hvs := fSop (OEluiw hi) fSnil in
let hl := make_lhsv_single hvs in
- fSop (OEaddiw lo) hl.
+ fSop (OEaddiw None lo) hl.
Definition load_hilo64 (hi lo: int64) :=
if Int64.eq lo Int64.zero then
@@ -48,19 +48,19 @@ Definition load_hilo64 (hi lo: int64) :=
else
let hvs := fSop (OEluil hi) fSnil in
let hl := make_lhsv_single hvs in
- fSop (OEaddil lo) hl.
+ fSop (OEaddil None lo) hl.
Definition loadimm32 (n: int) :=
match make_immed32 n with
| Imm32_single imm =>
- fSop (OEimmR0 (OPimmADD imm)) fSnil
+ fSop (OEaddiw (Some X0_R) imm) fSnil
| Imm32_pair hi lo => load_hilo32 hi lo
end.
Definition loadimm64 (n: int64) :=
match make_immed64 n with
| Imm64_single imm =>
- fSop (OEimmR0 (OPimmADDL imm)) fSnil
+ fSop (OEaddil (Some X0_R) imm) fSnil
| Imm64_pair hi lo => load_hilo64 hi lo
| Imm64_large imm => fSop (OEloadli imm) fSnil
end.
@@ -91,20 +91,20 @@ Definition opimm64 (hv1: hsval) (n: int64) (op: operation) (opimm: int64 -> oper
fSop op hl
end.
-Definition addimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oadd OEaddiw.
+Definition addimm32 (hv1: hsval) (n: int) (or: option oreg) := opimm32 hv1 n Oadd (OEaddiw or).
Definition andimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oand OEandiw.
Definition orimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oor OEoriw.
Definition xorimm32 (hv1: hsval) (n: int) := opimm32 hv1 n Oxor OExoriw.
Definition sltimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltw None) OEsltiw.
Definition sltuimm32 (hv1: hsval) (n: int) := opimm32 hv1 n (OEsltuw None) OEsltiuw.
-Definition addimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oaddl OEaddil.
+Definition addimm64 (hv1: hsval) (n: int64) (or: option oreg) := opimm64 hv1 n Oaddl (OEaddil or).
Definition andimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oandl OEandil.
Definition orimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oorl OEoril.
Definition xorimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n Oxorl OExoril.
Definition sltimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltl None) OEsltil.
Definition sltuimm64 (hv1: hsval) (n: int64) := opimm64 hv1 n (OEsltul None) OEsltiul.
-(* Comparisons intructions *)
+(** ** Comparisons intructions *)
Definition cond_int32s (cmp: comparison) (lhsv: list_hsval) (optR: option oreg) :=
match cmp with
@@ -260,7 +260,7 @@ Definition expanse_cond_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) :=
let hl := make_lhsv_single hvs in
if normal' then hvs else fSop (OExoriw Int.one) hl.
-(* Branches instructions *)
+(** ** Branches instructions *)
Definition transl_cbranch_int32s (cmp: comparison) (optR: option oreg) :=
match cmp with
@@ -309,18 +309,37 @@ Definition expanse_cbranch_fp (cnot: bool) fn_cond cmp (lhsv: list_hsval) : (con
let hl := make_lhsv_cmp false hvs hvs in
if normal' then ((CEbnew (Some X0_R)), hl) else ((CEbeqw (Some X0_R)), hl).
-(** Add pointer expansion *)
+(** ** Add pointer expansion *)
-(*Definition addptrofs (hv1: hsval) (n: ptrofs) :=*)
- (*if Ptrofs.eq_dec n Ptrofs.zero then*)
- (*let lhsv := make_lhsv_single hv1 in*)
- (*fSop Omove lhsv*)
- (*else*)
- (*if Archi.ptr64*)
- (*then addimm64 hv1 (Ptrofs.to_int64 n)*)
- (*else addimm32 hv1 (Ptrofs.to_int n).*)
-
-(** Target op simplifications using "fake" values *)
+Definition addptrofs (n: ptrofs) :=
+ if Ptrofs.eq_dec n Ptrofs.zero then
+ fSop OEmoveSP fSnil
+ else
+ if Archi.ptr64
+ then (
+ match make_immed64 (Ptrofs.to_int64 n) with
+ | Imm64_single imm =>
+ fSop (OEaddil (Some SP_S) imm) fSnil
+ | Imm64_pair hi lo =>
+ let hvs := load_hilo64 hi lo in
+ let hl := make_lhsv_single hvs in
+ fSop (OEaddil (Some SP_S) Int64.zero) hl
+ | Imm64_large imm =>
+ let hvs := fSop (OEloadli imm) fSnil in
+ let hl := make_lhsv_single hvs in
+ fSop (OEaddil (Some SP_S) Int64.zero) hl
+ end)
+ else (
+ match make_immed32 (Ptrofs.to_int n) with
+ | Imm32_single imm =>
+ fSop (OEaddiw (Some SP_S) imm) fSnil
+ | Imm32_pair hi lo =>
+ let hvs := load_hilo32 hi lo in
+ let hl := make_lhsv_single hvs in
+ fSop (OEaddiw (Some SP_S) Int.zero) hl
+ end).
+
+(** * Target simplifications using "fake" values *)
Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_local): option hsval :=
match op, lr with
@@ -402,10 +421,10 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
Some (loadimm64 n)
| Oaddimm n, a1 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
- Some (addimm32 hv1 n)
+ Some (addimm32 hv1 n None)
| Oaddlimm n, a1 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
- Some (addimm64 hv1 n)
+ Some (addimm64 hv1 n None)
| Oandimm n, a1 :: nil =>
let hv1 := fsi_sreg_get hst a1 in
Some (andimm32 hv1 n)
@@ -442,9 +461,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
let hv1 := fsi_sreg_get hst a1 in
let hl := make_lhsv_single hv1 in
if Int.eq n Int.zero then
- let move_s := fSop Omove hl in
- let move_l := make_lhsv_cmp false move_s move_s in
- Some (fSop (OEmayundef (MUshrx n)) move_l)
+ let lhl := make_lhsv_cmp false hv1 hv1 in
+ Some (fSop (OEmayundef (MUshrx n)) lhl)
else
if Int.eq n Int.one then
let srliw_s := fSop (Oshruimm (Int.repr 31)) hl in
@@ -468,9 +486,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
let hv1 := fsi_sreg_get hst a1 in
let hl := make_lhsv_single hv1 in
if Int.eq n Int.zero then
- let move_s := fSop Omove hl in
- let move_l := make_lhsv_cmp false move_s move_s in
- Some (fSop (OEmayundef (MUshrxl n)) move_l)
+ let lhl := make_lhsv_cmp false hv1 hv1 in
+ Some (fSop (OEmayundef (MUshrxl n)) lhl)
else
if Int.eq n Int.one then
let srlil_s := fSop (Oshrluimm (Int.repr 63)) hl in
@@ -490,9 +507,8 @@ Definition target_op_simplify (op: operation) (lr: list reg) (hst: hsistate_loca
let srail_s' := fSop (Oshrlimm n) addl_l in
let srail_l' := make_lhsv_cmp false srail_s' srail_s' in
Some (fSop (OEmayundef (MUshrxl n)) srail_l')
- (*| Oaddrstack n, nil =>*)
- (*let hv1 := fsi_sreg_get hst a1 in*)
- (*OK (addptrofs hv1 n)*)
+ (* TODO gourdinl | Oaddrstack n, nil =>*)
+ (*Some (addptrofs n)*)
| _, _ => None
end.
@@ -601,9 +617,9 @@ Definition target_cbranch_expanse (prev: hsistate_local) (cond: condition) (args
| _, _ => None
end.
-(** Auxiliary lemmas on comparisons *)
+(** * Auxiliary lemmas on comparisons *)
-(* Signed ints *)
+(** ** Signed ints *)
Lemma xor_neg_ltle_cmp: forall v1 v2,
Some (Val.xor (Val.cmp Clt v1 v2) (Vint Int.one)) =
@@ -618,7 +634,7 @@ Proof.
auto.
Qed.
-(* Unsigned ints *)
+(** ** Unsigned ints *)
Lemma xor_neg_ltle_cmpu: forall mptr v1 v2,
Some (Val.xor (Val.cmpu (Mem.valid_pointer mptr) Clt v1 v2) (Vint Int.one)) =
@@ -652,7 +668,7 @@ Proof.
rewrite !Int.unsigned_repr; try cbn; try omega.
Qed.
-(* Signed longs *)
+(** ** Signed longs *)
Lemma xor_neg_ltle_cmpl: forall v1 v2,
Some (Val.xor (Val.maketotal (Val.cmpl Clt v1 v2)) (Vint Int.one)) =
@@ -748,7 +764,7 @@ Proof.
apply Z.le_ge. trivial.
Qed.
-(* Unsigned longs *)
+(** ** Unsigned longs *)
Lemma xor_neg_ltle_cmplu: forall mptr v1 v2,
Some (Val.xor (Val.maketotal (Val.cmplu (Mem.valid_pointer mptr) Clt v1 v2)) (Vint Int.one)) =
@@ -794,7 +810,7 @@ Proof.
repeat destruct (_ && _); simpl; auto.
Qed.
-(* Floats *)
+(** ** Floats *)
Lemma xor_neg_eqne_cmpf: forall v1 v2,
Some (Val.xor (Val.cmpf Ceq v1 v2) (Vint Int.one)) =
@@ -807,7 +823,7 @@ Proof.
destruct (Float.cmp _ _ _); simpl; auto.
Qed.
-(* Singles *)
+(** ** Singles *)
Lemma xor_neg_eqne_cmpfs: forall v1 v2,
Some (Val.xor (Val.cmpfs Ceq v1 v2) (Vint Int.one)) =
@@ -820,7 +836,7 @@ Proof.
destruct (Float32.cmp _ _ _); simpl; auto.
Qed.
-(* More useful lemmas *)
+(** ** More useful lemmas *)
Lemma xor_neg_optb: forall v,
Some (Val.xor (Val.of_optbool (option_map negb v))
@@ -863,7 +879,7 @@ Proof.
destruct x; destruct y; simpl; auto. rewrite Float32.cmp_swap. auto.
Qed.
-(* Intermediates lemmas on each expansed instruction *)
+(** * Intermediates lemmas on each expanded instruction *)
Lemma simplify_ccomp_correct ge sp hst st c r r0 rs0 m0 v v0: forall
(SREG: forall r: positive,
@@ -1026,7 +1042,6 @@ Proof.
try rewrite EQIMM; try destruct (Archi.ptr64) eqn:EQARCH; simpl;
try rewrite ltu_12_wordsize; trivial;
try rewrite Int.add_commut, Int.add_zero_l in *;
- try rewrite Int.add_commut;
try rewrite Int.add_zero_l;
try destruct (Int.ltu _ _) eqn:EQLTU; simpl;
try rewrite EQLTU; simpl; try rewrite EQIMM;
@@ -1149,25 +1164,21 @@ Proof.
1,2,3,4,5,6,7,8,9,10,11,12:
try rewrite <- optbool_mktotal; trivial;
try rewrite Int64.add_commut, Int64.add_zero_l in *;
- try rewrite Int64.add_commut;
- try rewrite Int64.add_zero_l;
try fold (Val.cmpl Clt (Vlong i) (Vlong imm));
try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12)))));
try fold (Val.cmpl Clt (Vlong i) (Vlong (Int64.add (Int64.sign_ext 32 (Int64.shl hi (Int64.repr 12))) lo)));
try rewrite xor_neg_ltge_cmpl; trivial;
try rewrite xor_neg_ltle_cmpl; trivial.
6:
- try rewrite Int64.add_commut;
rewrite <- H;
try apply cmpl_ltle_add_one; auto.
all:
try rewrite <- H;
try apply cmpl_ltle_add_one; auto;
+ try rewrite <- cmpl_ltle_add_one; auto;
try rewrite ltu_12_wordsize;
try rewrite Int.add_commut, Int.add_zero_l in *;
try rewrite Int64.add_commut, Int64.add_zero_l in *;
- try rewrite Int.add_commut;
- try rewrite Int64.add_commut;
try rewrite Int64.add_zero_l;
simpl; try rewrite lt_maxsgn_false_long;
try (rewrite <- H; trivial; fail);
@@ -1216,7 +1227,6 @@ Proof.
unfold Val.cmplu, eval_may_undef, zero64, Val.addl;
try apply Int64.same_if_eq in EQLO; subst;
try rewrite Int64.add_commut, Int64.add_zero_l in *; trivial;
- try rewrite Int64.add_commut;
try rewrite Int64.add_zero_l;
try (rewrite <- xor_neg_ltle_cmplu; unfold Val.cmplu;
trivial; fail);
@@ -1362,8 +1372,7 @@ Proof.
- apply Int64.same_if_eq in EQLO; subst.
try rewrite Int64.add_commut, Int64.add_zero_l in H.
rewrite <- H; try rewrite Float.of_to_bits; trivial.
- - try rewrite Int64.add_commut;
- rewrite <- H; try rewrite Float.of_to_bits; trivial.
+ - rewrite <- H; try rewrite Float.of_to_bits; trivial.
- rewrite <- H; try rewrite Float.of_to_bits; trivial.
Qed.
@@ -1392,7 +1401,6 @@ Proof.
all:
try apply Int.same_if_eq in EQLO; subst;
try rewrite Int.add_commut, Int.add_zero_l in H; simpl;
- try rewrite Int.add_commut in H;
rewrite ltu_12_wordsize; simpl; try rewrite <- H;
try rewrite Float32.of_to_bits; trivial.
Qed.
@@ -1403,7 +1411,7 @@ Lemma simplify_addimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
seval_sval ge sp (si_sreg st r) rs0 m0)
(H : match lr with
| nil => None
- | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n)
+ | a1 :: nil => Some (addimm32 (fsi_sreg_get hst a1) n None)
| a1 :: _ :: _ => None
end = Some fsv)
(OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
@@ -1423,7 +1431,6 @@ Proof.
all:
try apply Int.same_if_eq in EQLO; subst;
try rewrite Int.add_commut, Int.add_zero_l;
- try rewrite Int.add_commut;
try rewrite ltu_12_wordsize; trivial.
Qed.
@@ -1433,7 +1440,7 @@ Lemma simplify_addlimm_correct ge sp rs0 m0 lr n hst fsv st args m: forall
seval_sval ge sp (si_sreg st r) rs0 m0)
(H : match lr with
| nil => None
- | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n)
+ | a1 :: nil => Some (addimm64 (fsi_sreg_get hst a1) n None)
| a1 :: _ :: _ => None
end = Some fsv)
(OK1 : seval_list_sval ge sp (list_sval_inj (map (si_sreg st) lr)) rs0 m0 = Some args),
@@ -1483,7 +1490,6 @@ Proof.
all:
try apply Int.same_if_eq in EQLO; subst;
try rewrite Int.add_commut, Int.add_zero_l;
- try rewrite Int.add_commut;
try rewrite ltu_12_wordsize; trivial.
Qed.
@@ -1543,7 +1549,6 @@ Proof.
all:
try apply Int.same_if_eq in EQLO; subst;
try rewrite Int.add_commut, Int.add_zero_l;
- try rewrite Int.add_commut;
try rewrite ltu_12_wordsize; trivial.
Qed.
@@ -1595,7 +1600,6 @@ Proof.
try destruct (Int.eq lo Int.zero) eqn:EQLO; simpl;
try apply Int.same_if_eq in EQLO; subst;
try rewrite Int.add_commut, Int.add_zero_l;
- try rewrite Int.add_commut;
try rewrite ltu_12_wordsize; try rewrite H; trivial.
Qed.
@@ -1690,9 +1694,8 @@ Lemma simplify_shrximm_correct ge sp rs0 m0 lr hst fsv st args m n: forall
then
Some
(fSop (OEmayundef (MUshrx n))
- (make_lhsv_cmp false
- (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))
- (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))))
+ (make_lhsv_cmp false (fsi_sreg_get hst a1)
+ (fsi_sreg_get hst a1)))
else
if Int.eq n Int.one
then
@@ -1794,9 +1797,8 @@ Lemma simplify_shrxlimm_correct ge sp rs0 m0 lr hst fsv st args m n: forall
then
Some
(fSop (OEmayundef (MUshrxl n))
- (make_lhsv_cmp false
- (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))
- (fSop Omove (make_lhsv_single (fsi_sreg_get hst a1)))))
+ (make_lhsv_cmp false (fsi_sreg_get hst a1)
+ (fsi_sreg_get hst a1)))
else
if Int.eq n Int.one
then
@@ -1885,7 +1887,7 @@ Proof.
destruct Int.ltu eqn:EQN2 in TOTAL; try discriminate.
rewrite !EQN2. rewrite EQN0.
reflexivity.
- Qed.
+Qed.
Lemma simplify_cast32unsigned_correct ge sp rs0 m0 lr hst fsv st args m: forall
(SREG: forall r: positive,
@@ -1924,7 +1926,7 @@ Proof.
rewrite Int64.shru'_zero. reflexivity.
Qed.
-(* Main proof of simplification *)
+(** * Main proof of simplification *)
Lemma target_op_simplify_correct op lr hst fsv ge sp rs0 m0 st args m: forall
(H: target_op_simplify op lr hst = Some fsv)
@@ -1937,28 +1939,22 @@ Proof.
unfold target_op_simplify; simpl.
intros H (LREF & SREF & SREG & SMEM) ? ? ?.
destruct op; try congruence.
- (* int and long constants *)
eapply simplify_intconst_correct; eauto.
eapply simplify_longconst_correct; eauto.
- (* FP const expansions *)
eapply simplify_floatconst_correct; eauto.
eapply simplify_singleconst_correct; eauto.
- (* cast 8/16 operations *)
+ (* TODO gourdinl*)
+ (*admit.*)
eapply simplify_cast8signed_correct; eauto.
eapply simplify_cast16signed_correct; eauto.
- (* Immediate int operations *)
eapply simplify_addimm_correct; eauto.
eapply simplify_andimm_correct; eauto.
eapply simplify_orimm_correct; eauto.
- (* Shrx imm int operation *)
eapply simplify_shrximm_correct; eauto.
- (* cast 32u operation *)
eapply simplify_cast32unsigned_correct; eauto.
- (* Immediate long operations *)
eapply simplify_addlimm_correct; eauto.
eapply simplify_andlimm_correct; eauto.
eapply simplify_orlimm_correct; eauto.
- (* Shrx imm long operation *)
eapply simplify_shrxlimm_correct; eauto.
(* Ocmp expansions *)
destruct cond; repeat (destruct lr; simpl; try congruence);
@@ -1966,31 +1962,20 @@ Proof.
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);
inv H; inv OK1.
- (* Ccomp *)
- eapply simplify_ccomp_correct; eauto.
- (* Ccompu *)
- eapply simplify_ccompu_correct; eauto.
- (* Ccompimm *)
- eapply simplify_ccompimm_correct; eauto.
- (* Ccompuimm *)
- eapply simplify_ccompuimm_correct; eauto.
- (* Ccompl *)
- eapply simplify_ccompl_correct; eauto.
- (* Ccomplu *)
- eapply simplify_ccomplu_correct; eauto.
- (* Ccomplimm *)
- eapply simplify_ccomplimm_correct; eauto.
- (* Ccompluimm *)
- eapply simplify_ccompluimm_correct; eauto.
- (* Ccompf *)
- eapply simplify_ccompf_correct; eauto.
- (* Cnotcompf *)
- eapply simplify_cnotcompf_correct; eauto.
- (* Ccompfs *)
- eapply simplify_ccompfs_correct; eauto.
- (* Cnotcompfs *)
- eapply simplify_cnotcompfs_correct; eauto.
Qed.
+(*Admitted.*)
Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall
(TARGET: target_cbranch_expanse hst c l = Some (c', l'))
@@ -2042,7 +2027,6 @@ Proof.
try destruct v; try rewrite H;
try rewrite ltu_12_wordsize; try rewrite EQLO;
try rewrite Int.add_commut, Int.add_zero_l;
- try rewrite Int.add_commut;
try rewrite Int64.add_commut, Int64.add_zero_l;
try rewrite Int64.add_commut;
try rewrite Int.add_zero_l; try rewrite Int64.add_zero_l;
diff --git a/riscV/ValueAOp.v b/riscV/ValueAOp.v
index e48c4a5b..3ba2732d 100644
--- a/riscV/ValueAOp.v
+++ b/riscV/ValueAOp.v
@@ -19,44 +19,41 @@ Require Import Zbits.
Definition zero32 := (I Int.zero).
Definition zero64 := (L Int64.zero).
-
-Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz: aval): B :=
+
+(** Functions to select a special register (see Op.v) *)
+
+Definition apply_bin_oreg {B} (optR: option oreg) (sem: aval -> aval -> B) (v1 v2 vz sp: aval): B :=
match optR with
| None => sem v1 v2
| Some X0_L => sem vz v1
| Some X0_R => sem v1 vz
+ | Some SP_S => sem v1 sp
end.
Definition eval_may_undef (mu: mayundef) (v1 v2: aval): aval :=
match mu with
- | MUint => match v1 with
- | I _ => v2
- | _ => Ifptr Ptop
+ | MUint => match v1, v2 with
+ | I _, I _ => v2
+ | _, _ => Ifptr Ptop
end
- | MUlong => match v1 with
- | L _ => v2
- | _ => Ifptr Ptop
+ | MUlong => match v1, v2 with
+ | L _, I _ => v2
+ | _, _ => Ifptr Ptop
end
| MUshrx i =>
- match v1 with
- | I _ =>
- if Int.ltu i (Int.repr 31) then v1 else Ifptr Ptop
- | _ => Ifptr Ptop
+ match v1, v2 with
+ | I _, I _ =>
+ if Int.ltu i (Int.repr 31) then v2 else Ifptr Ptop
+ | _, _ => Ifptr Ptop
end
| MUshrxl i =>
- match v1 with
- | L _ =>
- if Int.ltu i (Int.repr 63) then v1 else Ifptr Ptop
- | _ => Ifptr Ptop
+ match v1, v2 with
+ | L _, L _ =>
+ if Int.ltu i (Int.repr 63) then v2 else Ifptr Ptop
+ | _, _ => Ifptr Ptop
end
end.
-Definition eval_opimmR0 (opi: opimm): aval :=
- match opi with
- | OPimmADD i => add (I i) zero32
- | OPimmADDL i => addl (L i) zero64
- end.
-
Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
match cond, vl with
| Ccomp c, v1 :: v2 :: nil => cmp_bool c v1 v2
@@ -71,22 +68,22 @@ Definition eval_static_condition (cond: condition) (vl: list aval): abool :=
| Cnotcompf c, v1 :: v2 :: nil => cnot (cmpf_bool c v1 v2)
| Ccompfs c, v1 :: v2 :: nil => cmpfs_bool c v1 v2
| Cnotcompfs c, v1 :: v2 :: nil => cnot (cmpfs_bool c v1 v2)
- | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32
- | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32
- | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32
- | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32
- | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32
- | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32
- | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32
- | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32
- | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64
- | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64
- | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64
- | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64
- | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64
- | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64
- | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64
- | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64
+ | CEbeqw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop)
+ | CEbnew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop)
+ | CEbequw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop)
+ | CEbneuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop)
+ | CEbltw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop)
+ | CEbltuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop)
+ | CEbgew optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmp_bool Cge) v1 v2 zero32 (Ifptr Ptop)
+ | CEbgeuw optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpu_bool Cge) v1 v2 zero32 (Ifptr Ptop)
+ | CEbeql optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop)
+ | CEbnel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop)
+ | CEbequl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop)
+ | CEbneul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop)
+ | CEbltl optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop)
+ | CEbltul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop)
+ | CEbgel optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmpl_bool Cge) v1 v2 zero64 (Ifptr Ptop)
+ | CEbgeul optR, v1 :: v2 :: nil => apply_bin_oreg optR (cmplu_bool Cge) v1 v2 zero64 (Ifptr Ptop)
| _, _ => Bnone
end.
@@ -226,33 +223,35 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval :=
| Osingleoflong, v1::nil => singleoflong v1
| Osingleoflongu, v1::nil => singleoflongu v1
| Ocmp c, _ => of_optbool (eval_static_condition c vl)
- | OEimmR0 opi, nil => eval_opimmR0 opi
- | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32)
- | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32)
- | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32)
- | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32)
- | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32)
- | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32)
+ | OEmoveSP, nil => Ptr Stack
+ | OEseqw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Ceq) v1 v2 zero32 (Ifptr Ptop))
+ | OEsnew optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Cne) v1 v2 zero32 (Ifptr Ptop))
+ | OEsequw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Ceq) v1 v2 zero32 (Ifptr Ptop))
+ | OEsneuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Cne) v1 v2 zero32 (Ifptr Ptop))
+ | OEsltw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmp_bool Clt) v1 v2 zero32 (Ifptr Ptop))
+ | OEsltuw optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpu_bool Clt) v1 v2 zero32 (Ifptr Ptop))
| OEsltiw n, v1::nil => of_optbool (cmp_bool Clt v1 (I n))
| OEsltiuw n, v1::nil => of_optbool (cmpu_bool Clt v1 (I n))
| OExoriw n, v1::nil => xor v1 (I n)
| OEluiw n, nil => shl (I n) (I (Int.repr 12))
- | OEaddiw n, v1::nil => add (I n) v1
+ | OEaddiw optR n, nil => apply_bin_oreg optR add (I n) (Ifptr Ptop) zero32 (Ifptr Ptop)
+ | OEaddiw optR n, v1::nil => apply_bin_oreg optR add v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack)
| OEandiw n, v1::nil => and (I n) v1
| OEoriw n, v1::nil => or (I n) v1
- | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64)
- | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64)
- | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64)
- | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64)
- | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64)
- | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64)
+ | OEseql optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Ceq) v1 v2 zero64 (Ifptr Ptop))
+ | OEsnel optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Cne) v1 v2 zero64 (Ifptr Ptop))
+ | OEsequl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Ceq) v1 v2 zero64 (Ifptr Ptop))
+ | OEsneul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Cne) v1 v2 zero64 (Ifptr Ptop))
+ | OEsltl optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmpl_bool Clt) v1 v2 zero64 (Ifptr Ptop))
+ | OEsltul optR, v1::v2::nil => of_optbool (apply_bin_oreg optR (cmplu_bool Clt) v1 v2 zero64 (Ifptr Ptop))
| OEsltil n, v1::nil => of_optbool (cmpl_bool Clt v1 (L n))
| OEsltiul n, v1::nil => of_optbool (cmplu_bool Clt v1 (L n))
| OEandil n, v1::nil => andl (L n) v1
| OEoril n, v1::nil => orl (L n) v1
| OExoril n, v1::nil => xorl v1 (L n)
| OEluil n, nil => sign_ext 32 (shll (L n) (L (Int64.repr 12)))
- | OEaddil n, v1::nil => addl (L n) v1
+ | OEaddil optR n, nil => apply_bin_oreg optR addl (L n) (Ifptr Ptop) zero64 (Ifptr Ptop)
+ | OEaddil optR n, v1::nil => apply_bin_oreg optR addl v1 (Ifptr Ptop) (Ifptr Ptop) (Ptr Stack)
| OEloadli n, nil => L (n)
| OEmayundef mu, v1 :: v2 :: nil => eval_may_undef mu v1 v2
| OEfeqd, v1::v2::nil => of_optbool (cmpf_bool Ceq v1 v2)
@@ -419,8 +418,8 @@ Lemma eval_cmpu_sound c: forall a1 b1 a0 b0 optR m,
c = Ceq \/ c = Cne \/ c = Clt->
vmatch bc a1 b1 ->
vmatch bc a0 b0 ->
- vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32)
- (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32)).
+ vmatch bc (Op.apply_bin_oreg optR (Val.cmpu (Mem.valid_pointer m) c) a1 a0 Op.zero32 Vundef)
+ (of_optbool (apply_bin_oreg optR (cmpu_bool c) b1 b0 zero32 (Ifptr Ptop))).
Proof.
intros.
destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
@@ -434,8 +433,8 @@ Lemma eval_cmplu_sound c: forall a1 b1 a0 b0 optR m,
vmatch bc
(Val.maketotal
(Op.apply_bin_oreg optR (Val.cmplu (Mem.valid_pointer m) c) a1 a0
- Op.zero64))
- (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64)).
+ Op.zero64 Vundef))
+ (of_optbool (apply_bin_oreg optR (cmplu_bool c) b1 b0 zero64 (Ifptr Ptop))).
Proof.
intros.
destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
@@ -445,8 +444,8 @@ Qed.
Lemma eval_cmp_sound: forall a1 b1 a0 b0 optR cmp,
vmatch bc a1 b1 ->
vmatch bc a0 b0 ->
- vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32)
- (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32)).
+ vmatch bc (Op.apply_bin_oreg optR (Val.cmp cmp) a1 a0 Op.zero32 Vundef)
+ (of_optbool (apply_bin_oreg optR (cmp_bool cmp) b1 b0 zero32 (Ifptr Ptop))).
Proof.
intros.
destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
@@ -457,8 +456,8 @@ Lemma eval_cmpl_sound: forall a1 b1 a0 b0 optR cmp,
vmatch bc a1 b1 ->
vmatch bc a0 b0 ->
vmatch bc
- (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64))
- (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64)).
+ (Val.maketotal (Op.apply_bin_oreg optR (Val.cmpl cmp) a1 a0 Op.zero64 Vundef))
+ (of_optbool (apply_bin_oreg optR (cmpl_bool cmp) b1 b0 zero64 (Ifptr Ptop))).
Proof.
intros.
destruct optR as [[]|]; unfold Op.apply_bin_oreg, apply_bin_oreg;
@@ -478,19 +477,23 @@ Proof.
rewrite Ptrofs.add_zero_l; eauto with va.
apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
- unfold Op.eval_opimmR0, eval_opimmR0, Op.zero32, zero32, Op.zero64, zero64;
- destruct opi; eauto with va.
3,4,6: apply eval_cmpu_sound; auto.
1,2,3: apply eval_cmp_sound; auto.
unfold Val.cmp; apply of_optbool_sound; eauto with va.
unfold Val.cmpu; apply of_optbool_sound; eauto with va.
- { fold (Val.add (Vint n) a1); eauto with va. }
+ { destruct optR as [[]|]; simpl; eauto with va;
+ InvHyps; eauto with va;
+ destruct Archi.ptr64 eqn:A; simpl;
+ inv H1; simpl; try rewrite A; simpl; eauto with va. }
{ fold (Val.and (Vint n) a1); eauto with va. }
{ fold (Val.or (Vint n) a1); eauto with va. }
{ simpl; try destruct (Int.ltu _ _); eauto with va; unfold ntop1;
try apply vmatch_ifptr_undef. }
- 9: { fold (Val.addl (Vlong n) a1); eauto with va. }
+ 9: { destruct optR as [[]|]; simpl; eauto with va;
+ InvHyps; eauto with va;
+ destruct Archi.ptr64 eqn:A; simpl;
+ inv H1; simpl; try rewrite A; simpl; eauto with va. }
9: { fold (Val.andl (Vlong n) a1); eauto with va. }
9: { fold (Val.orl (Vlong n) a1); eauto with va. }
9: { simpl; unfold ntop1, sign_ext, Int64.sign_ext, sgn; simpl;
generated by cgit (git 2.34.1) at 2024-05-09 02:16:34 +0000