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

13 files changed, 166 insertions, 16 deletions

diff --git a/x86/Asmgen.v b/x86/Asmgen.v
index 73e3263e..99e9fc2b 100644
--- a/x86/Asmgen.v
+++ b/x86/Asmgen.v
@@ -636,9 +636,14 @@ Definition transl_op
 
 (** Translation of memory loads and stores *)
 
-Definition transl_load (chunk: memory_chunk)
+Definition transl_load
+           (trap : trapping_mode)
+           (chunk: memory_chunk)
                        (addr: addressing) (args: list mreg) (dest: mreg)
                        (k: code) : res code :=
+  match trap with
+  | NOTRAP => Error (msg "Asmgen.transl_load x86 does not support non trapping loads")
+  | TRAP =>
   do am <- transl_addressing addr args;
   match chunk with
   | Mint8unsigned =>
@@ -659,6 +664,7 @@ Definition transl_load (chunk: memory_chunk)
       do r <- freg_of dest; OK(Pmovsd_fm r am :: k)
   | _ =>
       Error (msg "Asmgen.transl_load")
+  end
   end.
 
 Definition transl_store (chunk: memory_chunk)
@@ -699,8 +705,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
          loadind RSP f.(fn_link_ofs) Tptr AX 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 reg) =>
diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index f1fd41e3..6886b2fd 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -235,11 +235,11 @@ Proof.
 Qed.
 
 Remark transl_load_label:
-  forall chunk addr args dest k c,
-  transl_load chunk addr args dest k = OK c ->
+  forall trap chunk addr args dest k c,
+  transl_load trap chunk addr args dest k = OK c ->
   tail_nolabel k c.
 Proof.
-  intros. monadInv H. destruct chunk; TailNoLabel.
+  intros. destruct trap; try discriminate. monadInv H. destruct chunk; TailNoLabel.
 Qed.
 
 Remark transl_store_label:
@@ -567,6 +567,12 @@ Opaque loadind.
   split. eapply agree_set_undef_mreg; eauto. congruence.
   simpl; congruence.
 
+- (* 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/x86/Asmgenproof1.v b/x86/Asmgenproof1.v
index fd88954e..7cff1047 100644
--- a/x86/Asmgenproof1.v
+++ b/x86/Asmgenproof1.v
@@ -1464,8 +1464,8 @@ Qed.
 (** Translation of memory loads. *)
 
 Lemma transl_load_correct:
-  forall chunk addr args dest k c (rs: regset) m a v,
-  transl_load chunk addr args dest k = OK c ->
+  forall trap chunk addr args dest k c (rs: regset) m a v,
+  transl_load trap chunk addr args dest k = OK c ->
   eval_addressing ge (rs#RSP) addr (map rs (map preg_of args)) = Some a ->
   Mem.loadv chunk m a = Some v ->
   exists rs',
@@ -1473,7 +1473,9 @@ Lemma transl_load_correct:
   /\ rs'#(preg_of dest) = v
   /\ forall r, data_preg r = true -> r <> preg_of dest -> rs'#r = rs#r.
 Proof.
-  unfold transl_load; intros. monadInv H.
+  unfold transl_load; intros.
+  destruct trap; simpl; try discriminate.
+  monadInv H.
   exploit transl_addressing_mode_correct; eauto. intro EA.
   assert (EA': eval_addrmode ge x rs = a). destruct a; simpl in H1; try discriminate; inv EA; auto.
   set (rs2 := nextinstr_nf (rs#(preg_of dest) <- v)).
diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index fdd94239..d9f5b8fa 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -15,6 +15,7 @@
 
 Require Import Coqlib Decidableplus.
 Require Import AST Machregs Locations.
+Require Import Errors.
 
 (** * Classification of machine registers *)
 
@@ -26,7 +27,7 @@ Require Import AST Machregs Locations.
   We follow the x86-32 and x86-64 application binary interfaces (ABI)
   in our choice of callee- and caller-save registers.
 *)
-
+  
 Definition is_callee_save (r: mreg) : bool :=
   match r with
   | AX | CX | DX => false
diff --git a/x86/DuplicateOpcodeHeuristic.ml b/x86/DuplicateOpcodeHeuristic.ml
new file mode 100644
index 00000000..85505245
--- /dev/null
+++ b/x86/DuplicateOpcodeHeuristic.ml
@@ -0,0 +1,3 @@
+exception HeuristicSucceeded
+        
+let opcode_heuristic code cond ifso ifnot preferred = ()
diff --git a/x86/Machregsaux.ml b/x86/Machregsaux.ml
index 473e0602..80066b00 100644
--- a/x86/Machregsaux.ml
+++ b/x86/Machregsaux.ml
@@ -14,9 +14,9 @@
 
 open Camlcoq
 open Machregs
-
+   
 let register_names : (mreg, string) Hashtbl.t = Hashtbl.create 31
-
+                                              
 let _ =
   List.iter
     (fun (s, r) -> Hashtbl.add register_names r (camlstring_of_coqstring s))
@@ -31,3 +31,8 @@ let register_by_name s =
   Machregs.register_by_name (coqstring_uppercase_ascii_of_camlstring s)
 
 let can_reserve_register r = Conventions1.is_callee_save r
+                                              
+let class_of_type = function
+  | AST.Tint | AST.Tlong -> 0
+  | AST.Tfloat | AST.Tsingle -> 1
+  | AST.Tany32 | AST.Tany64 -> assert false
diff --git a/x86/Machregsaux.mli b/x86/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/x86/Machregsaux.mli
+++ b/x86/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/x86/Op.v b/x86/Op.v
index 16d75426..15672bbe 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -742,6 +742,37 @@ 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
+  | Omod | Omodl | Omodu | Omodlu
+  | Oshrximm _ | Oshrxlimm _
+  | Ointoffloat
+  | Ointofsingle
+  | Olongoffloat
+  | Olongofsingle 
+  | Osingleofint
+  | Osingleoflong
+  | Ofloatofint
+  | Ofloatoflong
+  | Olea _ | Oleal _ (* TODO this is suboptimal *) => 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 *)
@@ -1199,6 +1230,21 @@ Proof.
   unfold eval_addressing; intros. destruct Archi.ptr64; eauto using eval_addressing32_inj, eval_addressing64_inj.
 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.
+
 Lemma eval_operation_inj:
   forall op sp1 vl1 sp2 vl2 v1,
   (forall id ofs,
@@ -1425,6 +1471,19 @@ Proof.
   destruct H1 as [v2 [A B]]. exists v2; split; auto. rewrite val_inject_lessdef; 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.
+
 End EVAL_LESSDEF.
 
 (** Compatibility of the evaluation functions with memory injections. *)
@@ -1477,6 +1536,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/x86/SelectLong.vp b/x86/SelectLong.vp
index b213e23f..4f9fb518 100644
--- a/x86/SelectLong.vp
+++ b/x86/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/x86/SelectLongproof.v b/x86/SelectLongproof.v
index 3bef632d..f008f39e 100644
--- a/x86/SelectLongproof.v
+++ b/x86/SelectLongproof.v
@@ -16,6 +16,7 @@ Require Import String Coqlib Maps 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/x86/SelectOp.vp b/x86/SelectOp.vp
index 31be8c32..a23c37d5 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -40,6 +40,7 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats Builtins.
 Require Import Op CminorSel.
+Require Import OpHelpers.
 Require Archi.
 
 Local Open Scope cminorsel_scope.
@@ -576,6 +577,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/x86/SelectOpproof.v b/x86/SelectOpproof.v
index 961f602c..af1d4e08 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -17,6 +17,8 @@ Require Import AST Integers Floats.
 Require Import Values Memory Builtins Globalenvs.
 Require Import Cminor Op CminorSel.
 Require Import SelectOp.
+Require Import OpHelpers.
+Require Import OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 
@@ -68,8 +70,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.
@@ -1012,6 +1016,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:
diff --git a/x86/ValueAOp.v b/x86/ValueAOp.v
index d0b8427a..e5584b6a 100644
--- a/x86/ValueAOp.v
+++ b/x86/ValueAOp.v
@@ -261,6 +261,25 @@ Proof.
   apply of_optbool_sound. eapply eval_static_condition_sound; eauto.
   apply select_sound; auto. eapply eval_static_condition_sound; eauto.
 Qed.
-
+(*
+Theorem eval_static_addressing_sound_none:
+  forall addr vargs aargs,
+  eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = None ->
+  list_forall2 (vmatch bc) vargs aargs ->
+  (eval_static_addressing addr aargs) = Vbot.
+Proof.
+  unfold eval_addressing, eval_static_addressing.
+  intros until aargs. intros Heval_none Hlist.
+  destruct (Archi.ptr64).
+  inv Hlist.
+  destruct addr; trivial; discriminate.
+  inv H0.
+  destruct addr; trivial; try discriminate. simpl in *.
+  inv H2.
+  destruct addr; trivial; discriminate.
+  inv H3;
+  destruct addr; trivial; discriminate.
+Qed.
+*)
 End SOUNDNESS.