From 23fa2a18e015b9d330ad6f1f08cf50adf90bd80b Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Thu, 21 Mar 2019 22:39:27 +0100
Subject: try to be portable across archs

---
 x86/Conventions1.v  | 3 ++-
 x86/Machregsaux.ml  | 9 +++++++--
 x86/Machregsaux.mli | 2 ++
 3 files changed, 11 insertions(+), 3 deletions(-)

(limited to 'x86')

diff --git a/x86/Conventions1.v b/x86/Conventions1.v
index 646c4afb..35d555f9 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/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
-- 
cgit 


From 5a425ba34f3f2520de752ea95a4636a9437c312a Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 22 Mar 2019 08:12:41 +0100
Subject: ça recompile sur x86
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 x86/SelectLong.vp     |  2 +-
 x86/SelectLongproof.v |  1 +
 x86/SelectOp.vp       |  8 ++++++++
 x86/SelectOpproof.v   | 29 +++++++++++++++++++++++++++--
 4 files changed, 37 insertions(+), 3 deletions(-)

(limited to 'x86')

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 a1583600..eadda093 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -40,6 +40,7 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats.
 Require Import Op CminorSel.
+Require Import OpHelpers.
 
 Local Open Scope cminorsel_scope.
 
@@ -540,3 +541,10 @@ Nondetfunction builtin_arg (e: expr) :=
   | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
   | _ => 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).
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index fdbadaa8..1eeb5906 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -23,6 +23,8 @@ Require Import Cminor.
 Require Import Op.
 Require Import CminorSel.
 Require Import SelectOp.
+Require Import OpHelpers.
+Require Import OpHelpersproof.
 
 Local Open Scope cminorsel_scope.
 
@@ -74,8 +76,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.
@@ -984,4 +988,25 @@ 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.
 End CMCONSTR.
-- 
cgit 


From 4c379d48b35e7c8156f3953fede31d5e47faf8ca Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 19 Jul 2019 18:59:44 +0200
Subject: helpers broke compilation

---
 x86/SelectOp.vp     | 7 +------
 x86/SelectOpproof.v | 5 +----
 2 files changed, 2 insertions(+), 10 deletions(-)

(limited to 'x86')

diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index d734ecc6..a23c37d5 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -40,11 +40,8 @@ Require Import Coqlib.
 Require Import Compopts.
 Require Import AST Integers Floats Builtins.
 Require Import Op CminorSel.
-<<<<<<< HEAD
 Require Import OpHelpers.
-=======
 Require Archi.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 
 Local Open Scope cminorsel_scope.
 
@@ -580,16 +577,14 @@ Nondetfunction builtin_arg (e: expr) :=
   | _ => BA e
   end.
 
-<<<<<<< HEAD
 (* 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 :=
   None.
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index b59f4a87..5703c758 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -1016,8 +1016,6 @@ Proof.
 - constructor; auto.
 Qed.
 
-<<<<<<< HEAD
-
 (* floating-point division without HELPERS *)
 Theorem eval_divf_base:
   forall le a b x y,
@@ -1038,7 +1036,7 @@ Proof.
   intros; unfold divfs_base.
   TrivialExists.
 Qed.
-=======
+
 (** Platform-specific known builtins *)
 
 Theorem eval_platform_builtin:
@@ -1051,5 +1049,4 @@ Proof.
   intros. discriminate.
 Qed.
 
->>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf
 End CMCONSTR.
-- 
cgit 


From 75109076ec027675e297ff1273660fc6b5a5f239 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 6 Sep 2019 23:46:15 +0200
Subject: for nontrap

---
 x86/Op.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

(limited to 'x86')

diff --git a/x86/Op.v b/x86/Op.v
index 16d75426..a1000a51 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1199,6 +1199,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 +1440,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. *)
-- 
cgit 


From f2831013b46d0486e5e134f26fde9ece7b78ff93 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 7 Sep 2019 09:49:58 +0200
Subject: more for passing notrap through x86

---
 x86/Asmgen.v       | 12 +++++++++---
 x86/Asmgenproof.v  | 12 +++++++++---
 x86/Asmgenproof1.v |  8 +++++---
 x86/Op.v           | 13 +++++++++++++
 x86/ValueAOp.v     | 21 ++++++++++++++++++++-
 5 files changed, 56 insertions(+), 10 deletions(-)

(limited to 'x86')

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/Op.v b/x86/Op.v
index a1000a51..a7176ce4 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1505,6 +1505,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/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.
 
-- 
cgit 


From c7156a4fd9c449c7610942a2fbf1e0908459b7f6 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Mon, 23 Sep 2019 19:48:20 +0200
Subject: add: non trapping ops

---
 x86/Op.v | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

(limited to 'x86')

diff --git a/x86/Op.v b/x86/Op.v
index a7176ce4..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 *)
-- 
cgit 


From 1b6667cf268189104bc3320e83fa23fe0d053717 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Fri, 7 Feb 2020 14:29:32 +0100
Subject: stubs to keep compiling on architectures not K1c

---
 x86/DuplicateOpcodeHeuristic.ml | 3 +++
 1 file changed, 3 insertions(+)
 create mode 100644 x86/DuplicateOpcodeHeuristic.ml

(limited to 'x86')

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 = ()
-- 
cgit