aboutsummaryrefslogtreecommitdiffstats
path: root/arm
diff options
context:
space:
mode:
Diffstat (limited to 'arm')
-rw-r--r--arm/Asmgen.v13
-rw-r--r--arm/Asmgenproof.v7
-rw-r--r--arm/Asmgenproof1.v8
-rw-r--r--arm/Machregsaux.ml5
-rw-r--r--arm/Machregsaux.mli2
-rw-r--r--arm/Op.v66
-rw-r--r--arm/SelectLong.vp2
-rw-r--r--arm/SelectLongproof.v1
-rw-r--r--arm/SelectOp.vp9
-rw-r--r--arm/SelectOpproof.v28
10 files changed, 130 insertions, 11 deletions
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 0ec0a4d0..f428feea 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -692,8 +692,12 @@ Definition transl_memory_access_float
None
mk_immed addr args k.
-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 Arm")
+ | TRAP =>
match chunk with
| Mint8signed =>
transl_memory_access_int Pldrsb mk_immed_mem_small dst addr args k
@@ -711,6 +715,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing)
transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k
| _ =>
Error (msg "Asmgen.transl_load")
+ end
end.
Definition transl_store (chunk: memory_chunk) (addr: addressing)
@@ -750,8 +755,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
else loadind_int IR13 f.(fn_link_ofs) IR12 c)
| 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 arg) =>
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 25f91d23..92ae524f 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -303,6 +303,7 @@ Proof.
eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel.
eapply transl_op_label; eauto.
unfold transl_load, transl_memory_access_int, transl_memory_access_float in H.
+ destruct t; try discriminate.
destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto.
unfold transl_store, transl_memory_access_int, transl_memory_access_float in H.
destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto.
@@ -618,6 +619,12 @@ Opaque loadind.
split. eapply agree_set_undef_mreg; eauto. congruence.
simpl; congruence.
+- (* Mload notrap1 *)
+ 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/arm/Asmgenproof1.v b/arm/Asmgenproof1.v
index 2b125cda..cdac697e 100644
--- a/arm/Asmgenproof1.v
+++ b/arm/Asmgenproof1.v
@@ -1558,8 +1558,8 @@ Proof.
Qed.
Lemma transl_load_correct:
- forall chunk addr args dst k c (rs: regset) a m v,
- transl_load chunk addr args dst k = OK c ->
+ forall trap chunk addr args dst k c (rs: regset) a m v,
+ transl_load trap chunk addr args dst k = OK c ->
eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a ->
Mem.loadv chunk m a = Some v ->
exists rs',
@@ -1567,7 +1567,9 @@ Lemma transl_load_correct:
/\ rs'#(preg_of dst) = v
/\ forall r, data_preg r = true -> r <> preg_of dst -> rs'#r = rs#r.
Proof.
- intros. destruct chunk; simpl in H.
+ intros.
+ destruct trap; try (simpl in *; discriminate).
+ destruct chunk; simpl in H.
eapply transl_load_int_correct; eauto.
eapply transl_load_int_correct; eauto.
eapply transl_load_int_correct; eauto.
diff --git a/arm/Machregsaux.ml b/arm/Machregsaux.ml
index ce5c67f6..14c75155 100644
--- a/arm/Machregsaux.ml
+++ b/arm/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/arm/Machregsaux.mli b/arm/Machregsaux.mli
index 9404568d..d7117c21 100644
--- a/arm/Machregsaux.mli
+++ b/arm/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/arm/Op.v b/arm/Op.v
index cc90e043..671bdbe4 100644
--- a/arm/Op.v
+++ b/arm/Op.v
@@ -518,6 +518,32 @@ 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 | Odivu
+ | Oshrximm _
+ | Ointoffloat | Ointuoffloat
+ | Ointofsingle | Ointuofsingle
+ | Ofloatofint | Ofloatofintu
+ | Osingleofint | Osingleofintu => 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 *)
@@ -975,6 +1001,20 @@ Proof.
apply Val.offset_ptr_inject; 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. *)
@@ -1080,6 +1120,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. rewrite val_inject_list_lessdef in H.
+ eapply eval_addressing_inj_none with (sp1 := sp).
+ intros. rewrite <- val_inject_lessdef; auto.
+ rewrite <- val_inject_lessdef; auto.
+ eauto. auto.
+Qed.
+
End EVAL_LESSDEF.
(** Compatibility of the evaluation functions with memory injections. *)
@@ -1132,6 +1185,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/arm/SelectLong.vp b/arm/SelectLong.vp
index cc7a38f6..b4cdd0e3 100644
--- a/arm/SelectLong.vp
+++ b/arm/SelectLong.vp
@@ -16,6 +16,6 @@ Require Import Coqlib.
Require Import Compopts.
Require Import AST Integers Floats.
Require Import Op CminorSel.
-Require Import SelectOp SplitLong.
+Require Import OpHelpers SelectOp SplitLong.
(** This file is empty because we use the default implementation provided in [SplitLong]. *)
diff --git a/arm/SelectLongproof.v b/arm/SelectLongproof.v
index a82c082c..a65a38d4 100644
--- a/arm/SelectLongproof.v
+++ b/arm/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/arm/SelectOp.vp b/arm/SelectOp.vp
index 1220abc4..5506157c 100644
--- a/arm/SelectOp.vp
+++ b/arm/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.
Local Open Scope cminorsel_scope.
@@ -516,6 +516,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/arm/SelectOpproof.v b/arm/SelectOpproof.v
index 70f8f191..56534c04 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -17,6 +17,7 @@ Require Import AST Integers Floats.
Require Import Values Memory Builtins Globalenvs.
Require Import Cminor Op CminorSel.
Require Import SelectOp.
+Require Import OpHelpers OpHelpersproof.
Local Open Scope cminorsel_scope.
Local Transparent Archi.ptr64.
@@ -69,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.
@@ -902,6 +905,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:
generated by cgit (git 2.34.1) at 2024-06-02 20:40:06 +0000