summaryrefslogtreecommitdiff
path: root/arm
diff options
context:
space:
mode:
Diffstat (limited to 'arm')
-rw-r--r--arm/ConstpropOp.vp26
-rw-r--r--arm/ConstpropOpproof.v26
-rw-r--r--arm/Unusedglob1.ml32
3 files changed, 79 insertions, 5 deletions
diff --git a/arm/ConstpropOp.vp b/arm/ConstpropOp.vp
index 0c77305..c0a04f0 100644
--- a/arm/ConstpropOp.vp
+++ b/arm/ConstpropOp.vp
@@ -84,11 +84,13 @@ Definition eval_static_intoffloat (f: float) :=
Definition eval_static_intuoffloat (f: float) :=
match Float.intuoffloat f with Some x => I x | None => Unknown end.
+Parameter propagate_float_constants: unit -> bool.
+
Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
match op, vl with
| Omove, v1::nil => v1
| Ointconst n, nil => I n
- | Ofloatconst n, nil => F n
+ | Ofloatconst n, nil => if propagate_float_constants tt then F n else Unknown
| Oaddrsymbol s n, nil => G s n
| Oaddrstack n, nil => S n
| Oadd, I n1 :: I n2 :: nil => I(Int.add n1 n2)
@@ -138,12 +140,30 @@ Nondetfunction eval_static_operation (op: operation) (vl: list approx) :=
| Osingleoffloat, F n1 :: nil => F(Float.singleoffloat n1)
| Ointoffloat, F n1 :: nil => eval_static_intoffloat n1
| Ointuoffloat, F n1 :: nil => eval_static_intuoffloat n1
- | Ofloatofint, I n1 :: nil => F(Float.floatofint n1)
- | Ofloatofintu, I n1 :: nil => F(Float.floatofintu n1)
+ | Ofloatofint, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofint n1) else Unknown
+ | Ofloatofintu, I n1 :: nil => if propagate_float_constants tt then F(Float.floatofintu n1) else Unknown
| Ocmp c, vl => eval_static_condition_val c vl
| _, _ => Unknown
end.
+Nondetfunction eval_static_addressing (addr: addressing) (vl: list approx) :=
+ match addr, vl with
+ | Aindexed n, I n1::nil => I (Int.add n1 n)
+ | Aindexed n, G id ofs::nil => G id (Int.add ofs n)
+ | Aindexed n, S ofs::nil => S (Int.add ofs n)
+ | Aindexed2, I n1::I n2::nil => I (Int.add n1 n2)
+ | Aindexed2, G id ofs::I n2::nil => G id (Int.add ofs n2)
+ | Aindexed2, I n1::G id ofs::nil => G id (Int.add ofs n1)
+ | Aindexed2, S ofs::I n2::nil => S (Int.add ofs n2)
+ | Aindexed2, I n1::S ofs::nil => S (Int.add ofs n1)
+ | Aindexed2shift s, I n1::I n2::nil => I (Int.add n1 (eval_static_shift s n2))
+ | Aindexed2shift s, G id ofs::I n2::nil => G id (Int.add ofs (eval_static_shift s n2))
+ | Aindexed2shift s, S ofs::I n2::nil => S (Int.add ofs (eval_static_shift s n2))
+ | Ainstack ofs, nil => S ofs
+ | _, _ => Unknown
+ end.
+
+
(** * Operator strength reduction *)
(** We now define auxiliary functions for strength reduction of
diff --git a/arm/ConstpropOpproof.v b/arm/ConstpropOpproof.v
index bf3b216..242f29b 100644
--- a/arm/ConstpropOpproof.v
+++ b/arm/ConstpropOpproof.v
@@ -124,7 +124,7 @@ Proof.
unfold eval_static_operation.
case (eval_static_operation_match op al); intros;
InvVLMA; simpl in *; FuncInv; try (subst v); try (rewrite eval_static_shift_correct); auto.
-
+ destruct (propagate_float_constants tt); simpl; auto.
rewrite shift_symbol_address; auto.
rewrite shift_symbol_address; auto.
rewrite Val.add_assoc; auto.
@@ -145,7 +145,8 @@ Proof.
destruct (Int.ltu n2 Int.iwordsize); simpl; auto.
unfold eval_static_intoffloat. destruct (Float.intoffloat n1); simpl in H0; inv H0; simpl; auto.
unfold eval_static_intuoffloat. destruct (Float.intuoffloat n1); simpl in H0; inv H0; simpl; auto.
-
+ destruct (propagate_float_constants tt); simpl; auto.
+ destruct (propagate_float_constants tt); simpl; auto.
unfold eval_static_condition_val, Val.of_optbool.
destruct (eval_static_condition c vl0) as []_eqn.
rewrite (eval_static_condition_correct _ _ _ m _ H Heqo).
@@ -153,6 +154,27 @@ Proof.
simpl; auto.
Qed.
+Lemma eval_static_addressing_correct:
+ forall addr al vl v,
+ val_list_match_approx al vl ->
+ eval_addressing ge sp addr vl = Some v ->
+ val_match_approx (eval_static_addressing addr al) v.
+Proof.
+ intros until v. unfold eval_static_addressing.
+ case (eval_static_addressing_match addr al); intros;
+ InvVLMA; simpl in *; FuncInv; try (subst v); try (rewrite eval_static_shift_correct); auto.
+ rewrite shift_symbol_address; auto.
+ rewrite Val.add_assoc. auto.
+ repeat rewrite shift_symbol_address. auto.
+ fold (Val.add (Vint n1) (symbol_address ge id ofs)).
+ repeat rewrite shift_symbol_address. apply Val.add_commut.
+ repeat rewrite Val.add_assoc. auto.
+ fold (Val.add (Vint n1) (Val.add sp (Vint ofs))).
+ rewrite Val.add_permut. decEq. rewrite Val.add_commut. auto.
+ rewrite shift_symbol_address. auto.
+ rewrite Val.add_assoc. auto.
+Qed.
+
(** * Correctness of strength reduction *)
(** We now show that strength reduction over operators and addressing
diff --git a/arm/Unusedglob1.ml b/arm/Unusedglob1.ml
new file mode 100644
index 0000000..04ef89a
--- /dev/null
+++ b/arm/Unusedglob1.ml
@@ -0,0 +1,32 @@
+(* *********************************************************************)
+(* *)
+(* The Compcert verified compiler *)
+(* *)
+(* Xavier Leroy, INRIA Paris-Rocquencourt *)
+(* *)
+(* Copyright Institut National de Recherche en Informatique et en *)
+(* Automatique. All rights reserved. This file is distributed *)
+(* under the terms of the INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(* Identifiers referenced from an ARM Asm instruction *)
+
+open Datatypes
+open AST
+open Asm
+
+let referenced_builtin ef =
+ match ef with
+ | EF_vload_global(chunk, id, ofs) -> [id]
+ | EF_vstore_global(chunk, id, ofs) -> [id]
+ | _ -> []
+
+let referenced_instr = function
+ | Pbsymb(s, _) -> [s]
+ | Pblsymb(s, _) -> [s]
+ | Ploadsymbol(_, s, _) -> [s]
+ | Pbuiltin ef -> referenced_builtin ef
+ | _ -> []
+
+let code_of_function f = f.fn_code