Added volatile_read_global and volatile_store_global builtins.

Finished updating IA32 and ARM ports.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1792 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 444 insertions, 0 deletions

diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
new file mode 100644
index 00000000..432db948
--- /dev/null
+++ b/arm/SelectOp.vp
@@ -0,0 +1,444 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Instruction selection for operators *)
+
+(** The instruction selection pass recognizes opportunities for using
+  combined arithmetic and logical operations and addressing modes
+  offered by the target processor.  For instance, the expression [x + 1]
+  can take advantage of the "immediate add" instruction of the processor,
+  and on the PowerPC, the expression [(x >> 6) & 0xFF] can be turned
+  into a "rotate and mask" instruction.
+
+  This file defines functions for building CminorSel expressions and
+  statements, especially expressions consisting of operator
+  applications.  These functions examine their arguments to choose
+  cheaper forms of operators whenever possible.
+
+  For instance, [add e1 e2] will return a CminorSel expression semantically
+  equivalent to [Eop Oadd (e1 ::: e2 ::: Enil)], but will use a
+  [Oaddimm] operator if one of the arguments is an integer constant,
+  or suppress the addition altogether if one of the arguments is the
+  null integer.  In passing, we perform operator reassociation
+  ([(e + c1) * c2] becomes [(e * c2) + (c1 * c2)]) and a small amount
+  of constant propagation.
+
+  On top of the "smart constructor" functions defined below,
+  module [Selection] implements the actual instruction selection pass.
+*)
+
+Require Import Coqlib.
+Require Import Maps.
+Require Import AST.
+Require Import Integers.
+Require Import Floats.
+Require Import Values.
+Require Import Memory.
+Require Import Globalenvs.
+Require Cminor.
+Require Import Op.
+Require Import CminorSel.
+
+Open Local Scope cminorsel_scope.
+
+(** ** Constants **)
+
+Definition addrsymbol (id: ident) (ofs: int) :=
+  Eop (Oaddrsymbol id ofs) Enil.
+
+Definition addrstack (ofs: int) :=
+  Eop (Oaddrstack ofs) Enil.
+
+(** ** Integer logical negation *)
+
+Nondetfunction notint (e: expr) :=
+  match e with
+  | Eop (Oshift s) (t1:::Enil) => Eop (Onotshift s) (t1:::Enil)
+  | Eop Onot (t1:::Enil) => t1
+  | Eop (Onotshift s) (t1:::Enil) => Eop (Oshift s) (t1:::Enil)
+  | _ => Eop Onot (e:::Enil)
+  end.
+
+(** ** Boolean negation *)
+
+Fixpoint notbool (e: expr) {struct e} : expr :=
+  let default := Eop (Ocmp (Ccompuimm Ceq Int.zero)) (e ::: Enil) in
+  match e with
+  | Eop (Ointconst n) Enil =>
+      Eop (Ointconst (if Int.eq n Int.zero then Int.one else Int.zero)) Enil
+  | Eop (Ocmp cond) args =>
+      Eop (Ocmp (negate_condition cond)) args
+  | Econdition e1 e2 e3 =>
+      Econdition e1 (notbool e2) (notbool e3)
+  | _ =>
+      default
+  end.
+
+(** ** Integer addition and pointer addition *)
+
+Nondetfunction addimm (n: int) (e: expr) :=
+  if Int.eq n Int.zero then e else
+  match e with
+  | Eop (Ointconst m) Enil       => Eop (Ointconst(Int.add n m)) Enil
+  | Eop (Oaddrsymbol s m) Enil   => Eop (Oaddrsymbol s (Int.add n m)) Enil
+  | Eop (Oaddrstack m) Enil      => Eop (Oaddrstack (Int.add n m)) Enil
+  | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil)
+  | _                            => Eop (Oaddimm n) (e ::: Enil)
+  end.
+
+Nondetfunction add (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 => addimm n1 t2
+  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
+      addimm (Int.add n1 n2) (Eop Oadd (t1:::t2:::Enil))
+  | Eop(Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil))
+  | t1, Eop (Ointconst n2) Enil => addimm n2 t1
+  | t1, Eop (Oaddimm n2) (t2:::Enil) => addimm n2 (Eop Oadd (t1:::t2:::Enil))
+  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oaddshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oaddshift s) (t1:::t2:::Enil)
+  | _, _ => Eop Oadd (e1:::e2:::Enil)
+  end.
+
+(** ** Integer and pointer subtraction *)
+
+Nondetfunction sub (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | t1, Eop (Ointconst n2) Enil => addimm (Int.neg n2) t1
+  | Eop (Oaddimm n1) (t1:::Enil), Eop (Oaddimm n2) (t2:::Enil) =>
+      addimm (Int.sub n1 n2) (Eop Osub (t1:::t2:::Enil))
+  | Eop (Oaddimm n1) (t1:::Enil), t2 =>
+      addimm n1 (Eop Osub (t1:::t2:::Enil))
+  | t1, Eop (Oaddimm n2) (t2:::Enil) =>
+      addimm (Int.neg n2) (Eop Osub (t1:::t2:::Enil))
+  | Eop (Ointconst n1) Enil, t2 => Eop (Orsubimm n1) (t2:::Enil)
+  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Orsubshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Osubshift s) (t1:::t2:::Enil)
+  | _, _ => Eop Osub (e1:::e2:::Enil)
+  end.
+
+Definition negint (e: expr) := Eop (Orsubimm Int.zero) (e ::: Enil).
+
+(** ** Immediate shifts *)
+
+Nondetfunction shlimm (e1: expr) (n: int) :=
+  if Int.eq n Int.zero then
+    e1
+  else if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshl (e1 ::: Eop (Ointconst n) Enil ::: Enil)
+  else match e1 with
+    | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shl n1 n)) Enil
+    | Eop (Oshift (Slsl n1)) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshift (Slsl (mk_shift_amount(Int.add n n1)))) (t1:::Enil)
+        else Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
+    | _ => Eop (Oshift (Slsl (mk_shift_amount n))) (e1:::Enil)
+    end.
+
+Nondetfunction shruimm (e1: expr) (n: int) :=
+  if Int.eq n Int.zero then
+    e1
+  else if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshru (e1 ::: Eop (Ointconst n) Enil ::: Enil)
+  else match e1 with
+    | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shru n1 n)) Enil
+    | Eop (Oshift (Slsr n1)) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshift (Slsr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
+        else Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
+    | _ => Eop (Oshift (Slsr (mk_shift_amount n))) (e1:::Enil)
+    end.
+
+Nondetfunction shrimm (e1: expr) (n: int) :=
+  if Int.eq n Int.zero then
+    e1
+  else if negb (Int.ltu n Int.iwordsize) then
+    Eop Oshr (e1 ::: Eop (Ointconst n) Enil ::: Enil)
+  else
+    match e1 with
+    | Eop (Ointconst n1) Enil => Eop (Ointconst(Int.shr n1 n)) Enil
+    | Eop (Oshift (Sasr n1)) (t1:::Enil) =>
+        if Int.ltu (Int.add n n1) Int.iwordsize
+        then Eop (Oshift (Sasr (mk_shift_amount (Int.add n n1)))) (t1:::Enil)
+        else Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
+    | _ => Eop (Oshift (Sasr (mk_shift_amount n))) (e1:::Enil)
+    end.
+
+(** ** Integer multiply *)
+
+Definition mulimm_base (n1: int) (e2: expr) :=
+  match Int.one_bits n1 with
+  | i :: nil =>
+      shlimm e2 i
+  | i :: j :: nil =>
+      Elet e2
+        (add (shlimm (Eletvar 0) i) (shlimm (Eletvar 0) j))
+  | _ =>
+      Eop Omul (Eop (Ointconst n1) Enil ::: e2 ::: Enil)
+  end.
+
+Nondetfunction mulimm (n1: int) (e2: expr) :=
+  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil
+  else if Int.eq n1 Int.one then e2
+  else match e2 with
+  | Eop (Ointconst n2) Enil => Eop (Ointconst(Int.mul n1 n2)) Enil
+  | Eop (Oaddimm n2) (t2:::Enil) => addimm (Int.mul n1 n2) (mulimm_base n1 t2)
+  | _ => mulimm_base n1 e2
+  end.
+
+Nondetfunction mul (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 => mulimm n1 t2
+  | t1, Eop (Ointconst n2) Enil => mulimm n2 t1
+  | _, _ => Eop Omul (e1:::e2:::Enil)
+  end.
+
+(** ** Bitwise and, or, xor *)
+
+Nondetfunction andimm (n1: int) (e2: expr) := 
+  if Int.eq n1 Int.zero then Eop (Ointconst Int.zero) Enil else
+  match e2 with
+  | Eop (Ointconst n2) Enil =>
+      Eop (Ointconst (Int.and n1 n2)) Enil
+  | Eop (Oandimm n2) (t2:::Enil) =>
+      Eop (Oandimm (Int.and n1 n2)) (t2:::Enil)
+  | _ =>
+      Eop (Oandimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction and (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 => andimm n1 t2
+  | t1, Eop (Ointconst n2) Enil => andimm n2 t1
+  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oandshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oandshift s) (t1:::t2:::Enil)
+  | Eop (Onotshift s) (t1:::Enil), t2 => Eop (Obicshift s) (t2:::t1:::Enil)
+  | t1, Eop (Onotshift s) (t2:::Enil) => Eop (Obicshift s) (t1:::t2:::Enil)
+  | Eop Onot (t1:::Enil), t2 => Eop Obic (t2:::t1:::Enil)
+  | t1, Eop Onot (t2:::Enil) => Eop Obic (t1:::t2:::Enil)
+  | _, _ => Eop Oand (e1:::e2:::Enil)
+  end.
+
+Definition same_expr_pure (e1 e2: expr) :=
+  match e1, e2 with
+  | Evar v1, Evar v2 => if ident_eq v1 v2 then true else false
+  | _, _ => false
+  end.
+
+Nondetfunction orimm (n1: int) (e2: expr) :=
+  if Int.eq n1 Int.zero then e2 else
+  match e2 with
+  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.or n1 n2)) Enil
+  | Eop (Oorimm n2) (t2:::Enil) => Eop (Oorimm (Int.or n1 n2)) (t2:::Enil)
+  | _ => Eop (Oorimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction or (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 => orimm n1 t2
+  | t1, Eop (Ointconst n2) Enil => orimm n2 t1
+  | Eop (Oshift (Slsl n1)) (t1:::Enil), Eop (Oshift (Slsr n2)) (t2:::Enil) =>
+      if Int.eq (Int.add n1 n2) Int.iwordsize
+      && same_expr_pure t1 t2
+      then Eop (Oshift (Sror n2)) (t1:::Enil)
+      else Eop (Oorshift (Slsr n2)) (e1:::t2:::Enil)
+  | Eop (Oshift (Slsr n1)) (t1:::Enil), Eop (Oshift (Slsl n2)) (t2:::Enil) =>
+      if Int.eq (Int.add n2 n1) Int.iwordsize
+      && same_expr_pure t1 t2
+      then Eop (Oshift (Sror n1)) (t1:::Enil)
+      else Eop (Oorshift (Slsl n2)) (e1:::t2:::Enil)
+  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oorshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oorshift s) (t1:::t2:::Enil)
+  | _, _ => Eop Oor (e1:::e2:::Enil)
+  end.
+
+Nondetfunction xorimm (n1: int) (e2: expr) :=
+  if Int.eq n1 Int.zero then e2 else
+  match e2 with
+  | Eop (Ointconst n2) Enil => Eop (Ointconst (Int.xor n1 n2)) Enil
+  | Eop (Oxorimm n2) (t2:::Enil) => Eop (Oxorimm (Int.xor n1 n2)) (t2:::Enil)
+  | _ => Eop (Oxorimm n1) (e2:::Enil)
+  end.
+
+Nondetfunction xor (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 => xorimm n1 t2
+  | t1, Eop (Ointconst n2) Enil => xorimm n2 t1
+  | Eop (Oshift s) (t1:::Enil), t2 => Eop (Oxorshift s) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) => Eop (Oxorshift s) (t1:::t2:::Enil)
+  | _, _ => Eop Oxor (e1:::e2:::Enil)
+  end.
+
+(** ** Integer division and modulus *)
+
+Definition mod_aux (divop: operation) (e1 e2: expr) :=
+  Elet e1
+    (Elet (lift e2)
+      (Eop Osub (Eletvar 1 :::
+                 Eop Omul (Eop divop (Eletvar 1 ::: Eletvar 0 ::: Enil) :::
+                           Eletvar 0 :::
+                           Enil) :::
+                 Enil))).
+
+Definition divs (e1: expr) (e2: expr) := Eop Odiv (e1:::e2:::Enil).
+
+Definition mods := mod_aux Odiv.
+
+Definition divuimm (e: expr) (n: int) :=
+  match Int.is_power2 n with
+  | Some l => shruimm e l
+  | None   => Eop Odivu (e ::: Eop (Ointconst n) Enil ::: Enil)
+  end.
+
+Nondetfunction divu (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Ointconst n2) Enil => divuimm e1 n2
+  | _ => Eop Odivu (e1:::e2:::Enil)
+  end.
+
+Definition moduimm (e: expr) (n: int) :=
+  match Int.is_power2 n with
+  | Some l => Eop (Oandimm (Int.sub n Int.one)) (e ::: Enil)
+  | None   => mod_aux Odivu e (Eop (Ointconst n) Enil)
+  end.
+
+Nondetfunction modu (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Ointconst n2) Enil => moduimm e1 n2
+  | _ => mod_aux Odivu e1 e2
+  end.
+
+(** ** General shifts *)
+
+Nondetfunction shl (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Ointconst n2) Enil => shlimm e1 n2
+  | _ => Eop Oshl (e1:::e2:::Enil)
+  end.
+
+Nondetfunction shr (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Ointconst n2) Enil => shrimm e1 n2
+  | _ => Eop Oshr (e1:::e2:::Enil)
+  end.
+
+Nondetfunction shru (e1: expr) (e2: expr) :=
+  match e2 with
+  | Eop (Ointconst n2) Enil => shruimm e1 n2
+  | _ => Eop Oshru (e1:::e2:::Enil)
+  end.
+
+(** ** Floating-point arithmetic *)
+
+Definition negf (e: expr) :=  Eop Onegf (e ::: Enil).
+Definition absf (e: expr) :=  Eop Oabsf (e ::: Enil).
+Definition addf (e1 e2: expr) :=  Eop Oaddf (e1 ::: e2 ::: Enil).
+Definition subf (e1 e2: expr) :=  Eop Osubf (e1 ::: e2 ::: Enil).
+Definition mulf (e1 e2: expr) :=  Eop Omulf (e1 ::: e2 ::: Enil).
+Definition divf (e1 e2: expr) :=  Eop Odivf (e1 ::: e2 ::: Enil).
+
+(** ** Comparisons *)
+
+Nondetfunction comp (c: comparison) (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 =>
+      Eop (Ocmp (Ccompimm (swap_comparison c) n1)) (t2:::Enil)
+  | t1, Eop (Ointconst n2) Enil =>
+      Eop (Ocmp (Ccompimm c n2)) (t1:::Enil)
+  | Eop (Oshift s) (t1:::Enil), t2 =>
+      Eop (Ocmp (Ccompshift (swap_comparison c) s)) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) =>
+      Eop (Ocmp (Ccompshift c s)) (t1:::t2:::Enil)
+  | _, _ =>
+      Eop (Ocmp (Ccomp c)) (e1:::e2:::Enil)
+  end.
+
+Nondetfunction compu (c: comparison) (e1: expr) (e2: expr) :=
+  match e1, e2 with
+  | Eop (Ointconst n1) Enil, t2 =>
+      Eop (Ocmp (Ccompuimm (swap_comparison c) n1)) (t2:::Enil)
+  | t1, Eop (Ointconst n2) Enil =>
+      Eop (Ocmp (Ccompuimm c n2)) (t1:::Enil)
+  | Eop (Oshift s) (t1:::Enil), t2 =>
+      Eop (Ocmp (Ccompushift (swap_comparison c) s)) (t2:::t1:::Enil)
+  | t1, Eop (Oshift s) (t2:::Enil) =>
+      Eop (Ocmp (Ccompushift c s)) (t1:::t2:::Enil)
+  | _, _ =>
+      Eop (Ocmp (Ccompu c)) (e1:::e2:::Enil)
+  end.
+
+Definition compf (c: comparison) (e1: expr) (e2: expr) :=
+  Eop (Ocmp (Ccompf c)) (e1 ::: e2 ::: Enil).
+
+(** ** Integer conversions *)
+
+Definition cast8unsigned (e: expr) := andimm (Int.repr 255) e.
+
+Definition cast8signed (e: expr) := shrimm (shlimm e (Int.repr 24)) (Int.repr 24).
+
+Definition cast16unsigned (e: expr) := andimm (Int.repr 65535) e.
+
+Definition cast16signed (e: expr) := shrimm (shlimm e (Int.repr 16)) (Int.repr 16).
+
+(** ** Floating-point conversions *)
+
+Definition singleoffloat (e: expr) := Eop Osingleoffloat (e ::: Enil).
+Definition intoffloat (e: expr) := Eop Ointoffloat (e ::: Enil).
+Definition intuoffloat (e: expr) := Eop Ointuoffloat (e ::: Enil).
+Definition floatofint (e: expr) := Eop Ofloatofint (e ::: Enil).
+Definition floatofintu (e: expr) := Eop Ofloatofintu (e ::: Enil).
+
+(** ** Recognition of addressing modes for load and store operations *)
+
+(** We do not recognize the [Aindexed2] and [Aindexed2shift] modes
+    for floating-point accesses, since these are not supported
+    by the hardware and emulated inefficiently in [Asmgen].
+    Likewise, [Aindexed2shift] are not supported for halfword
+    and signed byte accesses. *)
+
+Definition can_use_Aindexed2 (chunk: memory_chunk): bool :=
+  match chunk with
+  | Mint8signed => true
+  | Mint8unsigned => true
+  | Mint16signed => true
+  | Mint16unsigned => true
+  | Mint32 => true
+  | Mfloat32 => false
+  | Mfloat64 => false
+  end.
+
+Definition can_use_Aindexed2shift (chunk: memory_chunk): bool :=
+  match chunk with
+  | Mint8signed => false
+  | Mint8unsigned => true
+  | Mint16signed => false
+  | Mint16unsigned => false
+  | Mint32 => true
+  | Mfloat32 => false
+  | Mfloat64 => false
+  end.
+
+Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
+  match e with
+  | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
+  | Eop (Oaddimm n) (e1:::Enil) => (Aindexed n, e1:::Enil)
+  | Eop (Oaddshift s) (e1:::e2:::Enil) =>
+      if can_use_Aindexed2shift chunk
+      then (Aindexed2shift s, e1:::e2:::Enil)
+      else (Aindexed Int.zero, Eop (Oaddshift s) (e1:::e2:::Enil) ::: Enil)
+  | Eop Oadd (e1:::e2:::Enil) =>
+      if can_use_Aindexed2 chunk
+      then (Aindexed2, e1:::e2:::Enil)
+      else (Aindexed Int.zero, Eop Oadd (e1:::e2:::Enil) ::: Enil)
+  | _ => (Aindexed Int.zero, e:::Enil)
+  end.
+
+