aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backend/Allocation.v3
-rw-r--r--backend/Allocproof.v5
-rw-r--r--backend/Asmexpandaux.ml3
-rw-r--r--backend/CminorSel.v6
-rw-r--r--backend/Deadcode.v2
-rw-r--r--backend/Deadcodeproof.v9
-rw-r--r--backend/Inlining.v1
-rw-r--r--backend/Inliningproof.v8
-rw-r--r--backend/PrintAsmaux.ml4
-rw-r--r--backend/RTLgen.v4
-rw-r--r--backend/RTLgenproof.v27
-rw-r--r--backend/RTLtyping.v2
-rw-r--r--backend/Regalloc.ml15
-rw-r--r--backend/Stacking.v2
-rw-r--r--backend/Stackingproof.v4
-rw-r--r--backend/Unusedglobproof.v4
-rw-r--r--backend/ValueAnalysis.v5
-rw-r--r--backend/XTL.ml1
-rw-r--r--common/AST.v21
-rw-r--r--common/Events.v11
-rw-r--r--common/PrintAST.ml3
-rw-r--r--test/regression/Makefile2
-rw-r--r--test/regression/Results/volatile45
-rw-r--r--test/regression/volatile4.c29
-rw-r--r--x86/Asmexpand.ml2
-rw-r--r--x86/Machregs.v6
-rw-r--r--x86/Op.v21
-rw-r--r--x86/SelectOp.vp17
-rw-r--r--x86/SelectOpproof.v26
29 files changed, 211 insertions, 37 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v
index 3dd4cb09..3ac99a47 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -808,6 +808,9 @@ Fixpoint add_equations_builtin_arg
| BA_splitlong hi lo, BA_splitlong hi' lo' =>
do e1 <- add_equations_builtin_arg env hi hi' e;
add_equations_builtin_arg env lo lo' e1
+ | BA_addptr a1 a2, BA_addptr a1' a2' =>
+ do e1 <- add_equations_builtin_arg env a1 a1' e;
+ add_equations_builtin_arg env a2 a2' e1
| _, _ =>
None
end.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 3b2ecd35..6c10d27f 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1560,6 +1560,11 @@ Proof.
intros (v1 & A & B).
exploit IHeval_builtin_arg2; eauto. intros (v2 & C & D).
exists (Val.longofwords v1 v2); split; auto with barg. apply Val.longofwords_lessdef; auto.
+- exploit IHeval_builtin_arg1; eauto. eapply add_equations_builtin_arg_satisf; eauto.
+ intros (v1' & A & B).
+ exploit IHeval_builtin_arg2; eauto. intros (v2' & C & D).
+ econstructor; split. eauto with barg.
+ destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef.
Qed.
Lemma add_equations_builtin_args_satisf:
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index 13aa71d2..07e33efa 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -82,7 +82,8 @@ let translate_annot sp preg_to_dwarf annot =
| BA_single _
| BA_loadglobal _
| BA_addrglobal _
- | BA_loadstack _ -> None
+ | BA_loadstack _
+ | BA_addptr _ -> None
| BA_addrstack ofs -> Some (sp,BA_addrstack ofs)
| BA_splitlong (hi,lo) ->
begin
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 9439c269..96cb8ae6 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -272,7 +272,11 @@ Inductive eval_builtin_arg: builtin_arg expr -> val -> Prop :=
eval_builtin_arg (BA_addrglobal id ofs) (Genv.symbol_address ge id ofs)
| eval_BA_splitlong: forall a1 a2 v1 v2,
eval_expr nil a1 v1 -> eval_expr nil a2 v2 ->
- eval_builtin_arg (BA_splitlong (BA a1) (BA a2)) (Val.longofwords v1 v2).
+ eval_builtin_arg (BA_splitlong (BA a1) (BA a2)) (Val.longofwords v1 v2)
+ | eval_BA_addptr: forall a1 v1 a2 v2,
+ eval_builtin_arg a1 v1 -> eval_builtin_arg a2 v2 ->
+ eval_builtin_arg (BA_addptr a1 a2)
+ (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2).
End EVAL_EXPR.
diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index e5b2ce3a..f491d678 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -68,6 +68,8 @@ Fixpoint transfer_builtin_arg (nv: nval) (na: NA.t) (a: builtin_arg reg) : NA.t
| BA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk))
| BA_splitlong hi lo =>
transfer_builtin_arg All (transfer_builtin_arg All na hi) lo
+ | BA_addptr hi lo =>
+ transfer_builtin_arg All (transfer_builtin_arg All na hi) lo
end.
Definition transfer_builtin_args (na: NA.t) (al: list (builtin_arg reg)) : NA.t :=
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 3f0c5a4c..07c3f84a 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -609,6 +609,12 @@ Proof.
constructor; auto.
apply vagree_lessdef.
apply Val.longofwords_lessdef; apply lessdef_vagree; auto.
+- destruct (transfer_builtin_arg All (ne1, nm1) a1) as [ne' nm'] eqn:TR.
+ exploit IHeval_builtin_arg2; eauto. intros (v2' & A & B & C & D).
+ exploit IHeval_builtin_arg1; eauto. intros (v1' & P & Q & R & S).
+ econstructor; intuition auto.
+ econstructor; eauto.
+ destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef, vagree_lessdef, lessdef_vagree.
Qed.
Lemma transfer_builtin_args_sound:
@@ -657,6 +663,9 @@ Proof.
- destruct IHeval_builtin_arg1 as (v1' & A1).
destruct IHeval_builtin_arg2 as (v2' & A2).
exists (Val.longofwords v1' v2'); constructor; auto.
+- destruct IHeval_builtin_arg1 as (v1' & A1).
+ destruct IHeval_builtin_arg2 as (v2' & A2).
+ econstructor; econstructor; eauto.
Qed.
Lemma can_eval_builtin_args:
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 61776743..17139dbd 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -203,6 +203,7 @@ Fixpoint sbuiltinarg (ctx: context) (a: builtin_arg reg) : builtin_arg reg :=
| BA_loadstack chunk ofs => BA_loadstack chunk (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk)))
| BA_addrstack ofs => BA_addrstack (Ptrofs.add ofs (Ptrofs.repr ctx.(dstk)))
| BA_splitlong hi lo => BA_splitlong (sbuiltinarg ctx hi) (sbuiltinarg ctx lo)
+ | BA_addptr a1 a2 => BA_addptr (sbuiltinarg ctx a1) (sbuiltinarg ctx a2)
| _ => a
end.
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index bc991f0f..c3b0cfc3 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -436,9 +436,13 @@ Proof.
unfold Senv.symbol_address; simpl; unfold Genv.symbol_address.
rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
inv MG. econstructor. eauto. rewrite Ptrofs.add_zero; auto.
-- destruct IHeval_builtin_arg1 as (v1 & A1 & B1).
- destruct IHeval_builtin_arg2 as (v2 & A2 & B2).
+- destruct IHeval_builtin_arg1 as (v1' & A1 & B1).
+ destruct IHeval_builtin_arg2 as (v2' & A2 & B2).
econstructor; split. eauto with barg. apply Val.longofwords_inject; auto.
+- destruct IHeval_builtin_arg1 as (v1' & A1 & B1).
+ destruct IHeval_builtin_arg2 as (v2' & A2 & B2).
+ econstructor; split. eauto with barg.
+ destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject.
Qed.
Lemma tr_builtin_args:
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index c8f8ea82..f54c8698 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -178,6 +178,10 @@ let rec print_annot print_preg sp_reg_name oc = function
fprintf oc "(%a * 0x100000000 + %a)"
(print_annot print_preg sp_reg_name) hi
(print_annot print_preg sp_reg_name) lo
+ | BA_addptr(a1, a2) ->
+ fprintf oc "(%a + %a)"
+ (print_annot print_preg sp_reg_name) a1
+ (print_annot print_preg sp_reg_name) a2
let print_annot_text print_preg sp_reg_name oc txt args =
let print_fragment = function
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index cfbf57d6..6d81f84b 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -396,6 +396,10 @@ Fixpoint convert_builtin_arg {A: Type} (a: builtin_arg expr) (rl: list A) : buil
let (hi', rl1) := convert_builtin_arg hi rl in
let (lo', rl2) := convert_builtin_arg lo rl1 in
(BA_splitlong hi' lo', rl2)
+ | BA_addptr a1 a2 =>
+ let (a1', rl1) := convert_builtin_arg a1 rl in
+ let (a2', rl2) := convert_builtin_arg a2 rl1 in
+ (BA_addptr a1' a2', rl2)
end.
Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list A) : list (builtin_arg A) :=
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index b635fd58..93f209b7 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -1010,10 +1010,18 @@ Lemma invert_eval_builtin_arg:
/\ Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v
/\ (forall vl', convert_builtin_arg a (vl ++ vl') = (fst (convert_builtin_arg a vl), vl')).
Proof.
- induction 1; simpl; econstructor; intuition eauto with evalexpr barg.
- constructor.
- constructor.
- repeat constructor.
+ induction 1; simpl; try (econstructor; intuition eauto with evalexpr barg; fail).
+- econstructor; split; eauto with evalexpr. split. constructor. auto.
+- econstructor; split; eauto with evalexpr. split. constructor. auto.
+- econstructor; split; eauto with evalexpr. split. repeat constructor. auto.
+- destruct IHeval_builtin_arg1 as (vl1 & A1 & B1 & C1).
+ destruct IHeval_builtin_arg2 as (vl2 & A2 & B2 & C2).
+ destruct (convert_builtin_arg a1 vl1) as [a1' rl1] eqn:E1; simpl in *.
+ destruct (convert_builtin_arg a2 vl2) as [a2' rl2] eqn:E2; simpl in *.
+ exists (vl1 ++ vl2); split.
+ apply eval_exprlist_append; auto.
+ split. rewrite C1, E2. constructor; auto.
+ intros. rewrite app_ass, !C1, C2, E2. auto.
Qed.
Lemma invert_eval_builtin_args:
@@ -1057,6 +1065,17 @@ Proof.
rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2).
exists (Val.longofwords v1' v2'); split. constructor; auto.
split; auto. apply Val.longofwords_lessdef; auto.
+- destruct (convert_builtin_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *.
+ destruct (convert_builtin_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *.
+ destruct (convert_builtin_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *.
+ destruct (convert_builtin_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *.
+ inv EV.
+ exploit IHa1; eauto. rewrite CV1; simpl; eauto.
+ rewrite CV1, CV3; simpl. intros (v1' & A1 & B1 & C1).
+ exploit IHa2. eexact C1. rewrite CV2; simpl; eauto.
+ rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2).
+ econstructor; split. constructor; eauto.
+ split; auto. destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef.
Qed.
Lemma transl_eval_builtin_args:
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 9992ab79..fef74706 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -77,6 +77,7 @@ Definition type_of_builtin_arg (a: builtin_arg reg) : typ :=
| BA_loadglobal chunk id ofs => type_of_chunk chunk
| BA_addrglobal id ofs => Tptr
| BA_splitlong hi lo => Tlong
+ | BA_addptr a1 a2 => Tptr
end.
Definition type_of_builtin_res (r: builtin_res reg) : typ :=
@@ -249,6 +250,7 @@ Definition type_builtin_arg (e: S.typenv) (a: builtin_arg reg) (ty: typ) : res S
| BA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk)
| BA_addrglobal id ofs => type_expect e ty Tptr
| BA_splitlong hi lo => type_expect e ty Tlong
+ | BA_addptr a1 a2 => type_expect e ty Tptr
end.
Fixpoint type_builtin_args (e: S.typenv) (al: list (builtin_arg reg)) (tyl: list typ) : res S.typenv :=
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index c14852f4..d4d7362d 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -167,6 +167,8 @@ let rec convert_builtin_arg tyenv = function
| BA_addrglobal(id, ofs) -> BA_addrglobal(id, ofs)
| BA_splitlong(hi, lo) ->
BA_splitlong(convert_builtin_arg tyenv hi, convert_builtin_arg tyenv lo)
+ | BA_addptr(a1, a2) ->
+ BA_addptr(convert_builtin_arg tyenv a1, convert_builtin_arg tyenv a2)
let convert_builtin_res tyenv = function
| BR r ->
@@ -185,6 +187,10 @@ let rec constrain_builtin_arg a cl =
let (hi', cl1) = constrain_builtin_arg hi cl in
let (lo', cl2) = constrain_builtin_arg lo cl1 in
(BA_splitlong(hi', lo'), cl2)
+ | BA_addptr(a1, a2), _ ->
+ let (a1', cl1) = constrain_builtin_arg a1 cl in
+ let (a2', cl2) = constrain_builtin_arg a2 cl1 in
+ (BA_addptr(a1', a2'), cl2)
| _, _ -> (a, cl)
let rec constrain_builtin_args al cl =
@@ -335,6 +341,7 @@ let rec vset_addarg a after =
match a with
| BA v -> VSet.add v after
| BA_splitlong(hi, lo) -> vset_addarg hi (vset_addarg lo after)
+ | BA_addptr(a1, a2) -> vset_addarg a1 (vset_addarg a2 after)
| _ -> after
let vset_addargs al after = List.fold_right vset_addarg al after
@@ -432,8 +439,8 @@ let rec dce_parmove srcs dsts after =
let rec keep_builtin_arg after = function
| BA v -> VSet.mem v after
- | BA_splitlong(hi, lo) ->
- keep_builtin_arg after hi && keep_builtin_arg after lo
+ | BA_splitlong(a1, a2) | BA_addptr(a1, a2) ->
+ keep_builtin_arg after a1 && keep_builtin_arg after a2
| _ -> true
let dce_instr instr after k =
@@ -855,6 +862,10 @@ let rec reload_arg tospill eqs = function
let (hi', c1, eqs1) = reload_arg tospill eqs hi in
let (lo', c2, eqs2) = reload_arg tospill eqs1 lo in
(BA_splitlong(hi', lo'), c1 @ c2, eqs2)
+ | BA_addptr(a1, a2) ->
+ let (a1', c1, eqs1) = reload_arg tospill eqs a1 in
+ let (a2', c2, eqs2) = reload_arg tospill eqs1 a2 in
+ (BA_addptr(a1', a2'), c1 @ c2, eqs2)
| a -> (a, [], eqs)
let rec reload_args tospill eqs = function
diff --git a/backend/Stacking.v b/backend/Stacking.v
index f51848f2..7b382d05 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -97,6 +97,8 @@ Fixpoint transl_builtin_arg (fe: frame_env) (a: builtin_arg loc) : builtin_arg m
| BA_addrglobal id ofs => BA_addrglobal id ofs
| BA_splitlong hi lo =>
BA_splitlong (transl_builtin_arg fe hi) (transl_builtin_arg fe lo)
+ | BA_addptr a1 a2 =>
+ BA_addptr (transl_builtin_arg fe a1) (transl_builtin_arg fe a2)
end.
(** Translation of a Linear instruction. Prepends the corresponding
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index b885d22c..d3d901b6 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -1744,6 +1744,10 @@ Local Opaque fe.
destruct IHeval_builtin_arg2 as (v2 & A2 & B2); auto using in_or_app.
exists (Val.longofwords v1 v2); split; auto with barg.
apply Val.longofwords_inject; auto.
+- destruct IHeval_builtin_arg1 as (v1' & A1 & B1); auto using in_or_app.
+ destruct IHeval_builtin_arg2 as (v2' & A2 & B2); auto using in_or_app.
+ econstructor; split. eauto with barg.
+ destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject.
Qed.
Lemma transl_builtin_args_correct:
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index db03d0b3..446ffb7f 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -853,6 +853,10 @@ Proof.
destruct IHeval_builtin_arg2 as (v2' & A2 & B2); eauto using in_or_app.
exists (Val.longofwords v1' v2'); split; auto with barg.
apply Val.longofwords_inject; auto.
+- destruct IHeval_builtin_arg1 as (v1' & A1 & B1); eauto using in_or_app.
+ destruct IHeval_builtin_arg2 as (v2' & A2 & B2); eauto using in_or_app.
+ econstructor; split; eauto with barg.
+ destruct Archi.ptr64; auto using Val.add_inject, Val.addl_inject.
Qed.
Lemma eval_builtin_args_inject:
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 17a518cd..7c4c0525 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -59,6 +59,10 @@ Fixpoint abuiltin_arg (ae: aenv) (am: amem) (rm: romem) (ba: builtin_arg reg) :
| BA_loadglobal chunk id ofs => loadv chunk rm am (Ptr (Gl id ofs))
| BA_addrglobal id ofs => Ptr (Gl id ofs)
| BA_splitlong hi lo => longofwords (abuiltin_arg ae am rm hi) (abuiltin_arg ae am rm lo)
+ | BA_addptr ba1 ba2 =>
+ let v1 := abuiltin_arg ae am rm ba1 in
+ let v2 := abuiltin_arg ae am rm ba2 in
+ if Archi.ptr64 then addl v1 v2 else add v1 v2
end.
Definition set_builtin_res (br: builtin_res reg) (av: aval) (ae: aenv) : aenv :=
@@ -338,6 +342,7 @@ Proof.
- simpl. rewrite Ptrofs.add_zero_l. auto with va.
- eapply loadv_sound; eauto. apply symbol_address_sound; auto.
- apply symbol_address_sound; auto.
+- destruct Archi.ptr64; auto with va.
Qed.
Lemma abuiltin_args_sound:
diff --git a/backend/XTL.ml b/backend/XTL.ml
index a1b7f23b..f10efeed 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -133,6 +133,7 @@ let rec type_builtin_arg a ty =
match a with
| BA v -> set_var_type v ty
| BA_splitlong(a1, a2) -> type_builtin_arg a1 Tint; type_builtin_arg a2 Tint
+ | BA_addptr(a1, a2) -> type_builtin_arg a1 coq_Tptr; type_builtin_arg a2 coq_Tptr
| _ -> ()
let rec type_builtin_args al tyl =
diff --git a/common/AST.v b/common/AST.v
index 8a46a153..9eeca5b1 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -627,7 +627,8 @@ Inductive builtin_arg (A: Type) : Type :=
| BA_addrstack (ofs: ptrofs)
| BA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: ptrofs)
| BA_addrglobal (id: ident) (ofs: ptrofs)
- | BA_splitlong (hi lo: builtin_arg A).
+ | BA_splitlong (hi lo: builtin_arg A)
+ | BA_addptr (a1 a2: builtin_arg A).
Inductive builtin_res (A: Type) : Type :=
| BR (x: A)
@@ -639,6 +640,7 @@ Fixpoint globals_of_builtin_arg (A: Type) (a: builtin_arg A) : list ident :=
| BA_loadglobal chunk id ofs => id :: nil
| BA_addrglobal id ofs => id :: nil
| BA_splitlong hi lo => globals_of_builtin_arg hi ++ globals_of_builtin_arg lo
+ | BA_addptr a1 a2 => globals_of_builtin_arg a1 ++ globals_of_builtin_arg a2
| _ => nil
end.
@@ -649,6 +651,7 @@ Fixpoint params_of_builtin_arg (A: Type) (a: builtin_arg A) : list A :=
match a with
| BA x => x :: nil
| BA_splitlong hi lo => params_of_builtin_arg hi ++ params_of_builtin_arg lo
+ | BA_addptr a1 a2 => params_of_builtin_arg a1 ++ params_of_builtin_arg a2
| _ => nil
end.
@@ -675,6 +678,8 @@ Fixpoint map_builtin_arg (A B: Type) (f: A -> B) (a: builtin_arg A) : builtin_ar
| BA_addrglobal id ofs => BA_addrglobal id ofs
| BA_splitlong hi lo =>
BA_splitlong (map_builtin_arg f hi) (map_builtin_arg f lo)
+ | BA_addptr a1 a2 =>
+ BA_addptr (map_builtin_arg f a1) (map_builtin_arg f a2)
end.
Fixpoint map_builtin_res (A B: Type) (f: A -> B) (a: builtin_res A) : builtin_res B :=
@@ -691,17 +696,5 @@ Inductive builtin_arg_constraint : Type :=
| OK_default
| OK_const
| OK_addrstack
- | OK_addrglobal
- | OK_addrany
+ | OK_addressing
| OK_all.
-
-Definition builtin_arg_ok
- (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
- match ba, c with
- | (BA _ | BA_splitlong (BA _) (BA _)), _ => true
- | (BA_int _ | BA_long _ | BA_float _ | BA_single _), OK_const => true
- | BA_addrstack _, (OK_addrstack | OK_addrany) => true
- | BA_addrglobal _ _, (OK_addrglobal | OK_addrany) => true
- | _, OK_all => true
- | _, _ => false
- end.
diff --git a/common/Events.v b/common/Events.v
index 14cd27c5..ab804aa7 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1555,7 +1555,11 @@ Inductive eval_builtin_arg: builtin_arg A -> val -> Prop :=
eval_builtin_arg (BA_addrglobal id ofs) (Senv.symbol_address ge id ofs)
| eval_BA_splitlong: forall hi lo vhi vlo,
eval_builtin_arg hi vhi -> eval_builtin_arg lo vlo ->
- eval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo).
+ eval_builtin_arg (BA_splitlong hi lo) (Val.longofwords vhi vlo)
+ | eval_BA_addptr: forall a1 a2 v1 v2,
+ eval_builtin_arg a1 v1 -> eval_builtin_arg a2 v2 ->
+ eval_builtin_arg (BA_addptr a1 a2)
+ (if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2).
Definition eval_builtin_args (al: list (builtin_arg A)) (vl: list val) : Prop :=
list_forall2 eval_builtin_arg al vl.
@@ -1565,6 +1569,7 @@ Lemma eval_builtin_arg_determ:
Proof.
induction 1; intros v' EV; inv EV; try congruence.
f_equal; eauto.
+ apply IHeval_builtin_arg1 in H3. apply IHeval_builtin_arg2 in H5. subst; auto.
Qed.
Lemma eval_builtin_args_determ:
@@ -1637,6 +1642,10 @@ Proof.
- destruct IHeval_builtin_arg1 as (vhi' & P & Q).
destruct IHeval_builtin_arg2 as (vlo' & R & S).
econstructor; split; eauto with barg. apply Val.longofwords_lessdef; auto.
+- destruct IHeval_builtin_arg1 as (vhi' & P & Q).
+ destruct IHeval_builtin_arg2 as (vlo' & R & S).
+ econstructor; split; eauto with barg.
+ destruct Archi.ptr64; auto using Val.add_lessdef, Val.addl_lessdef.
Qed.
Lemma eval_builtin_args_lessdef:
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 48172dfd..ac7d2276 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -70,6 +70,9 @@ let rec print_builtin_arg px oc = function
| BA_splitlong(hi, lo) ->
fprintf oc "splitlong(%a, %a)"
(print_builtin_arg px) hi (print_builtin_arg px) lo
+ | BA_addptr(a1, a2) ->
+ fprintf oc "addptr(%a, %a)"
+ (print_builtin_arg px) a1 (print_builtin_arg px) a2
let rec print_builtin_args px oc = function
| [] -> ()
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 54745863..25b47c7e 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -10,7 +10,7 @@ LIBS=$(LIBMATH)
TESTS=int32 int64 floats floats-basics \
expr1 expr6 funptr2 initializers initializers2 initializers3 \
- volatile1 volatile2 volatile3 \
+ volatile1 volatile2 volatile3 volatile4 \
funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \
sizeof1 sizeof2 binops bool for1 switch switch2 compound \
decl1 interop1 bitfields9 ptrs3 \
diff --git a/test/regression/Results/volatile4 b/test/regression/Results/volatile4
new file mode 100644
index 00000000..e650a8e5
--- /dev/null
+++ b/test/regression/Results/volatile4
@@ -0,0 +1,5 @@
+l = 42
+a[5] = 255
+g = 3
+b[2] = -1
+p[1] = 80
diff --git a/test/regression/volatile4.c b/test/regression/volatile4.c
new file mode 100644
index 00000000..b72e1bb9
--- /dev/null
+++ b/test/regression/volatile4.c
@@ -0,0 +1,29 @@
+/* Addressing modes in volatiles */
+
+#include <stdio.h>
+
+volatile int g = 1;
+volatile int b[10];
+
+void test1(volatile int * p)
+{
+ volatile int l;
+ volatile int a[10];
+
+ l = 42;
+ printf ("l = %d\n", l);
+ a[5] = 0xff;
+ printf ("a[5] = %d\n", a[5]);
+ g = 3;
+ printf ("g = %d\n", g);
+ b[2] = -1;
+ printf ("b[2] = %d\n", b[2]);
+ p[1] = 80;
+ printf ("p[1] = %d\n", p[1]);
+}
+
+int main()
+{
+ test1(&b[0]);
+ return 0;
+}
diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml
index 8e69061e..1b716165 100644
--- a/x86/Asmexpand.ml
+++ b/x86/Asmexpand.ml
@@ -108,6 +108,8 @@ let addressing_of_builtin_arg = function
| BA (IR r) -> linear_addr r Z.zero
| BA_addrstack ofs -> linear_addr RSP (Integers.Ptrofs.unsigned ofs)
| BA_addrglobal(id, ofs) -> global_addr id ofs
+ | BA_addptr(BA (IR r), BA_int n) -> linear_addr r (Integers.Int.signed n)
+ | BA_addptr(BA (IR r), BA_long n) -> linear_addr r (Integers.Int64.signed n)
| _ -> assert false
(* Handling of memcpy *)
diff --git a/x86/Machregs.v b/x86/Machregs.v
index ffaf2531..5d1b4515 100644
--- a/x86/Machregs.v
+++ b/x86/Machregs.v
@@ -358,9 +358,9 @@ Definition two_address_op (op: operation) : bool :=
Definition builtin_constraints (ef: external_function) :
list builtin_arg_constraint :=
match ef with
- | EF_vload _ => OK_addrany :: nil
- | EF_vstore _ => OK_addrany :: OK_default :: nil
- | EF_memcpy _ _ => OK_addrany :: OK_addrany :: nil
+ | EF_vload _ => OK_addressing :: nil
+ | EF_vstore _ => OK_addressing :: OK_default :: nil
+ | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil
| EF_annot txt targs => map (fun _ => OK_all) targs
| EF_debug kind txt targs => map (fun _ => OK_all) targs
| _ => nil
diff --git a/x86/Op.v b/x86/Op.v
index 8ace5067..136c900b 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1455,3 +1455,24 @@ Proof.
Qed.
End EVAL_INJECT.
+
+(** * Handling of builtin arguments *)
+
+Definition builtin_arg_ok_1
+ (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
+ match c, ba with
+ | OK_all, _ => true
+ | OK_const, (BA_int _ | BA_long _ | BA_float _ | BA_single _) => true
+ | OK_addrstack, BA_addrstack _ => true
+ | OK_addressing, BA_addrstack _ => true
+ | OK_addressing, BA_addrglobal _ _ => true
+ | OK_addressing, BA_addptr (BA _) (BA_int _ | BA_long _) => true
+ | _, _ => false
+ end.
+
+Definition builtin_arg_ok
+ (A: Type) (ba: builtin_arg A) (c: builtin_arg_constraint) :=
+ match ba with
+ | (BA _ | BA_splitlong (BA _) (BA _)) => true
+ | _ => builtin_arg_ok_1 ba c
+ end.
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index 1200c3d7..a1583600 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -516,14 +516,23 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
(** ** Arguments of builtins *)
+Nondetfunction builtin_arg_addr (addr: Op.addressing) (el: exprlist) :=
+ match addr, el with
+ | Aindexed n, e1 ::: Enil =>
+ BA_addptr (BA e1) (if Archi.ptr64 then BA_long (Int64.repr n) else BA_int (Int.repr n))
+ | Aglobal id ofs, Enil => BA_addrglobal id ofs
+ | Ainstack ofs, Enil => BA_addrstack ofs
+ | _, _ => BA (Eop (Olea_ptr addr) el)
+ end.
+
Nondetfunction builtin_arg (e: expr) :=
match e with
| Eop (Ointconst n) Enil => BA_int n
| Eop (Olongconst n) Enil => BA_long n
- | Eop (Olea (Aglobal id ofs)) Enil => if Archi.ptr64 then BA e else BA_addrglobal id ofs
- | Eop (Olea (Ainstack ofs)) Enil => if Archi.ptr64 then BA e else BA_addrstack ofs
- | Eop (Oleal (Aglobal id ofs)) Enil => if Archi.ptr64 then BA_addrglobal id ofs else BA e
- | Eop (Oleal (Ainstack ofs)) Enil => if Archi.ptr64 then BA_addrstack ofs else BA e
+ | Eop (Olea addr) el =>
+ if Archi.ptr64 then BA e else builtin_arg_addr addr el
+ | Eop (Oleal addr) el =>
+ if Archi.ptr64 then builtin_arg_addr addr el else BA e
| Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
BA_long (Int64.ofwords h l)
| Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index e2e0b830..fdbadaa8 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -947,6 +947,22 @@ Proof.
- apply D; auto.
Qed.
+Theorem eval_builtin_arg_addr:
+ forall addr al vl v,
+ eval_exprlist ge sp e m nil al vl ->
+ Op.eval_addressing ge sp addr vl = Some v ->
+ CminorSel.eval_builtin_arg ge sp e m (builtin_arg_addr addr al) v.
+Proof.
+ intros until v. unfold builtin_arg_addr; case (builtin_arg_addr_match addr al); intros; InvEval.
+- set (v2 := if Archi.ptr64 then Vlong (Int64.repr n) else Vint (Int.repr n)).
+ assert (EQ: v = if Archi.ptr64 then Val.addl v1 v2 else Val.add v1 v2).
+ { unfold Op.eval_addressing in H0; unfold v2; destruct Archi.ptr64; simpl in H0; inv H0; auto. }
+ rewrite EQ. constructor. constructor; auto. unfold v2; destruct Archi.ptr64; constructor.
+- rewrite eval_addressing_Aglobal in H0. inv H0. constructor.
+- rewrite eval_addressing_Ainstack in H0. inv H0. constructor.
+- constructor. econstructor. eauto. rewrite eval_Olea_ptr. auto.
+Qed.
+
Theorem eval_builtin_arg:
forall a v,
eval_expr ge sp e m nil a v ->
@@ -955,10 +971,12 @@ Proof.
intros until v. unfold builtin_arg; case (builtin_arg_match a); intros; InvEval.
- constructor.
- constructor.
-- constructor.
-- constructor.
-- constructor.
-- constructor.
+- destruct Archi.ptr64 eqn:SF.
++ constructor; auto.
++ inv H. eapply eval_builtin_arg_addr. eauto. unfold Op.eval_addressing; rewrite SF; assumption.
+- destruct Archi.ptr64 eqn:SF.
++ inv H. eapply eval_builtin_arg_addr. eauto. unfold Op.eval_addressing; rewrite SF; assumption.
++ constructor; auto.
- simpl in H5. inv H5. constructor.
- constructor; auto.
- inv H. InvEval. rewrite eval_addressing_Aglobal in H6. inv H6. constructor; auto.
generated by cgit (git 2.34.1) at 2024-06-02 21:18:11 +0000