Merge branch 'mppa-cse2' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert into mppa-work

11 files changed, 134 insertions, 10 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index a686414a..29e2c028 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -783,8 +783,13 @@ Definition transl_memory_access
       Error(msg "Asmgen.transl_memory_access")
   end.
 
-Definition transl_load (chunk: memory_chunk) (addr: addressing)
-                       (args: list mreg) (dst: mreg) (k: code) :=
+Definition transl_load
+           (trap : trapping_mode)
+           (chunk: memory_chunk) (addr: addressing)
+           (args: list mreg) (dst: mreg) (k: code) :=
+  match trap with
+  | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on PPC")
+  | TRAP =>
   match chunk with
   | Mint8signed =>
       do r <- ireg_of dst;
@@ -812,6 +817,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
       transl_memory_access (Plfd r) (Plfdx r) addr args GPR12 k
   | _ =>
       Error (msg "Asmgen.transl_load")
+  end
   end.
 
 Definition transl_store (chunk: memory_chunk) (addr: addressing)
@@ -869,8 +875,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
          loadind GPR1 f.(fn_link_ofs) Tint R11 k1)
   | Mop op args res =>
       transl_op op args res k
-  | Mload chunk addr args dst =>
-      transl_load chunk addr args dst k
+  | Mload trap chunk addr args dst =>
+      transl_load trap chunk addr args dst k
   | Mstore chunk addr args src =>
       transl_store chunk addr args src k
   | Mcall sig (inl r) =>
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index d653633c..21d5ce48 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -328,6 +328,7 @@ Proof.
   eapply loadind_label; eauto.
   eapply tail_nolabel_trans; eapply loadind_label; eauto.
   eapply transl_op_label; eauto.
+  destruct t; try discriminate.
   destruct m; monadInv H; (eapply tail_nolabel_trans; [eapply transl_memory_access_label; TailNoLabel|TailNoLabel]).
   destruct m; monadInv H; eapply transl_memory_access_label; TailNoLabel.
   destruct s0; monadInv H; TailNoLabel.
@@ -657,6 +658,13 @@ Opaque loadind.
   split. simpl; congruence.
   apply R; auto with asmgen.
 
+
+- (* Mload notrap *) (* isn't there a nicer way? *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
+- (* Mload notrap *)
+  inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate.
+
 - (* Mstore *)
   assert (eval_addressing tge sp addr rs##args = Some a).
     rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index 20cf9c1d..1b797999 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -1679,8 +1679,8 @@ Qed.
 (** Translation of loads *)
 
 Lemma transl_load_correct:
-  forall chunk addr args dst k c (rs: regset) m a v,
-  transl_load chunk addr args dst k = OK c ->
+  forall trap chunk addr args dst k c (rs: regset) m a v,
+  transl_load trap chunk addr args dst k = OK c ->
   eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
@@ -1689,6 +1689,7 @@ Lemma transl_load_correct:
   /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r.
 Proof.
   intros.
+  destruct trap; try discriminate.
   assert (LD: forall v, Val.lessdef a v -> v = a).
   { intros. inv H2; auto. discriminate H1. }
   assert (BASE: forall mk1 mk2 k' chunk' v',
diff --git a/powerpc/DuplicateOpcodeHeuristic.ml b/powerpc/DuplicateOpcodeHeuristic.ml
new file mode 100644
index 00000000..85505245
--- /dev/null
+++ b/powerpc/DuplicateOpcodeHeuristic.ml
@@ -0,0 +1,3 @@
+exception HeuristicSucceeded
+        
+let opcode_heuristic code cond ifso ifnot preferred = ()
diff --git a/powerpc/Machregsaux.ml b/powerpc/Machregsaux.ml
index 664f71a0..0b0d4548 100644
--- a/powerpc/Machregsaux.ml
+++ b/powerpc/Machregsaux.ml
@@ -33,3 +33,8 @@ let register_by_name s =
 let can_reserve_register r =
   List.mem r Conventions1.int_callee_save_regs
   || List.mem r Conventions1.float_callee_save_regs
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/powerpc/Machregsaux.mli b/powerpc/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/powerpc/Machregsaux.mli
+++ b/powerpc/Machregsaux.mli
@@ -16,3 +16,5 @@ val name_of_register: Machregs.mreg -> string option
 val register_by_name: string -> Machregs.mreg option
 val is_scratch_register: string -> bool
 val can_reserve_register: Machregs.mreg -> bool
+
+val class_of_type: AST.typ -> int
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 0f082c1f..b73cb14b 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -581,6 +581,30 @@ Proof with (try exact I; try reflexivity).
   unfold Val.select. destruct (eval_condition c vl m). apply Val.normalize_type. exact I.
 Qed.
 
+Definition is_trapping_op (op : operation) :=
+  match op with
+  | Odiv | Odivl | Odivu | Odivlu
+  | Oshrximm _ | Oshrxlimm _
+  | Ointoffloat | Ointuoffloat
+  | Ofloatofint | Ofloatofintu
+  | Olongoffloat
+  | Ofloatoflong => true
+  | _ => false
+  end.
+
+Lemma is_trapping_op_sound:
+  forall op vl sp m,
+    op <> Omove ->
+    is_trapping_op op = false ->
+    (List.length vl) = (List.length (fst (type_of_operation op))) ->
+    eval_operation genv sp op vl m <> None.
+Proof.
+  destruct op; 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).
+Qed.
 End SOUNDNESS.
 
 (** * Manipulating and transforming operations *)
@@ -1032,6 +1056,21 @@ Proof.
   apply Val.add_inject; auto. apply H; simpl; auto.
 Qed.
 
+
+Lemma eval_addressing_inj_none:
+  forall addr sp1 vl1 sp2 vl2,
+  (forall id ofs,
+      In id (globals_addressing addr) ->
+      Val.inject f (Genv.symbol_address ge1 id ofs) (Genv.symbol_address ge2 id ofs)) ->
+  Val.inject f sp1 sp2 ->
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing ge1 sp1 addr vl1 = None ->
+  eval_addressing ge2 sp2 addr vl2 = None.
+Proof.
+  intros until vl2. intros Hglobal Hinjsp Hinjvl.
+  destruct addr; simpl in *;
+  inv Hinjvl; trivial; try discriminate; inv H0; trivial; try discriminate; inv H2; trivial; try discriminate.
+Qed.
 End EVAL_COMPAT.
 
 (** Compatibility of the evaluation functions with the ``is less defined'' relation over values. *)
@@ -1098,6 +1137,20 @@ Proof.
   rewrite <- val_inject_list_lessdef. eauto. auto.
 Qed.
 
+
+Lemma eval_addressing_lessdef_none:
+  forall sp addr vl1 vl2,
+  Val.lessdef_list vl1 vl2 ->
+  eval_addressing genv sp addr vl1 = None ->
+  eval_addressing genv sp addr vl2 = None.
+Proof.
+  intros until vl2. intros Hlessdef Heval1.
+  destruct addr; simpl in *;
+  inv Hlessdef; trivial; try discriminate;
+  inv H0; trivial; try discriminate;
+  inv H2; trivial; try discriminate.
+Qed.
+
 Lemma eval_operation_lessdef:
   forall sp op vl1 vl2 v1 m1 m2,
   Val.lessdef_list vl1 vl2 ->
@@ -1189,6 +1242,19 @@ Proof.
   econstructor; eauto. rewrite Ptrofs.add_zero_l; auto.
 Qed.
 
+Lemma eval_addressing_inject_none:
+  forall addr vl1 vl2,
+  Val.inject_list f vl1 vl2 ->
+  eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = None ->
+  eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = None.
+Proof.
+  intros.
+  rewrite eval_shift_stack_addressing.
+  eapply eval_addressing_inj_none with (sp1 := Vptr sp1 Ptrofs.zero); eauto.
+  intros. apply symbol_address_inject.
+  econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. 
+Qed.
+
 Lemma eval_operation_inject:
   forall op vl1 vl2 v1 m1 m2,
   Val.inject_list f vl1 vl2 ->
diff --git a/powerpc/SelectLong.vp b/powerpc/SelectLong.vp
index 5f13774b..e4274ba5 100644
--- a/powerpc/SelectLong.vp
+++ b/powerpc/SelectLong.vp
@@ -16,7 +16,7 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
-Require Import SelectOp SplitLong.
+Require Import OpHelpers SelectOp SplitLong.
 
 Local Open Scope cminorsel_scope.
 Local Open Scope string_scope.
diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v
index f16c967e..eba071eb 100644
--- a/powerpc/SelectLongproof.v
+++ b/powerpc/SelectLongproof.v
@@ -16,6 +16,7 @@ Require Import String Coqlib Maps Zbits Integers Floats Errors.
 Require Archi.
 Require Import AST Values Memory Globalenvs Events.
 Require Import Cminor Op CminorSel.
+Require Import OpHelpers OpHelpersproof.
 Require Import SelectOp SelectOpproof SplitLong SplitLongproof.
 Require Import SelectLong.
 
diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index ba6612e8..50b1bdd6 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -39,7 +39,7 @@
 Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats Builtins.
-Require Import Op CminorSel.
+Require Import Op OpHelpers CminorSel.
 Require Archi.
 
 Local Open Scope cminorsel_scope.
@@ -564,6 +564,13 @@ Nondetfunction builtin_arg (e: expr) :=
   | _ => BA e
   end.
 
+(* floats *)
+Definition divf_base (e1: expr) (e2: expr) :=
+  Eop Odivf (e1 ::: e2 ::: Enil).
+
+Definition divfs_base (e1: expr) (e2: expr) :=
+  Eop Odivfs (e1 ::: e2 ::: Enil).
+
 (** Platform-specific known builtins *)
 
 Definition platform_builtin (b: platform_builtin) (args: exprlist) : option expr :=
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index c3eda068..8135bad6 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -18,6 +18,8 @@ Require Import Values Memory Builtins Globalenvs.
 Require Import Cminor Op CminorSel.
 Require Import Compopts.
 Require Import SelectOp.
+Require Import OpHelpers.
+Require Import OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 Local Transparent Archi.ptr64.
@@ -70,8 +72,10 @@ Ltac TrivialExists :=
 (** * Correctness of the smart constructors *)
 
 Section CMCONSTR.
-
-Variable ge: genv.
+Variable prog: program.
+Variable hf: helper_functions.
+Hypothesis HELPERS: helper_functions_declared prog hf.
+Let ge := Genv.globalenv prog.
 Variable sp: val.
 Variable e: env.
 Variable m: mem.
@@ -1058,6 +1062,27 @@ Proof.
 - constructor; auto.
 Qed.
 
+(* floating-point division without HELPERS *)
+Theorem eval_divf_base:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divf_base a b) v /\ Val.lessdef (Val.divf x y) v.
+Proof.
+  intros; unfold divf_base.
+  TrivialExists.
+Qed.
+
+Theorem eval_divfs_base:
+  forall le a b x y,
+  eval_expr ge sp e m le a x ->
+  eval_expr ge sp e m le b y ->
+  exists v, eval_expr ge sp e m le (divfs_base a b) v /\ Val.lessdef (Val.divfs x y) v.
+Proof.
+  intros; unfold divfs_base.
+  TrivialExists.
+Qed.
+
 (** Platform-specific known builtins *)
 
 Theorem eval_platform_builtin: