From 6d25b4f3fc23601b3a84b4a70aab40ba429ac4b9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 30 Dec 2008 14:48:33 +0000 Subject: Reorganized the development, modularizing away machine-dependent parts. Started to merge the ARM code generator. Started to add support for PowerPC/EABI. Use ocamlbuild to construct executable from Caml files. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@930 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Op.v | 1007 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 1007 insertions(+) create mode 100644 arm/Op.v (limited to 'arm/Op.v') diff --git a/arm/Op.v b/arm/Op.v new file mode 100644 index 00000000..6a6df7ed --- /dev/null +++ b/arm/Op.v @@ -0,0 +1,1007 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Operators and addressing modes. The abstract syntax and dynamic + semantics for the CminorSel, RTL, LTL and Mach languages depend on the + following types, defined in this library: +- [condition]: boolean conditions for conditional branches; +- [operation]: arithmetic and logical operations; +- [addressing]: addressing modes for load and store operations. + + These types are processor-specific and correspond roughly to what the + processor can compute in one instruction. In other terms, these + types reflect the state of the program after instruction selection. + For a processor-independent set of operations, see the abstract + syntax and dynamic semantics of the Cminor language. +*) + +Require Import Coqlib. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Globalenvs. + +Set Implicit Arguments. + +Record shift_amount : Set := + mk_shift_amount { + s_amount: int; + s_amount_ltu: Int.ltu s_amount (Int.repr 32) = true + }. + +Inductive shift : Set := + | Slsl: shift_amount -> shift + | Slsr: shift_amount -> shift + | Sasr: shift_amount -> shift + | Sror: shift_amount -> shift. + +(** Conditions (boolean-valued operators). *) + +Inductive condition : Set := + | Ccomp: comparison -> condition (**r signed integer comparison *) + | Ccompu: comparison -> condition (**r unsigned integer comparison *) + | Ccompshift: comparison -> shift -> condition (**r signed integer comparison *) + | Ccompushift: comparison -> shift -> condition (**r unsigned integer comparison *) + | Ccompimm: comparison -> int -> condition (**r signed integer comparison with a constant *) + | Ccompuimm: comparison -> int -> condition (**r unsigned integer comparison with a constant *) + | Ccompf: comparison -> condition (**r floating-point comparison *) + | Cnotcompf: comparison -> condition. (**r negation of a floating-point comparison *) + +(** Arithmetic and logical operations. In the descriptions, [rd] is the + result of the operation and [r1], [r2], etc, are the arguments. *) + +Inductive operation : Set := + | Omove: operation (**r [rd = r1] *) + | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) + | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) + | Oaddrsymbol: ident -> int -> operation (**r [rd] is set to the the address of the symbol plus the offset *) + | Oaddrstack: int -> operation (**r [rd] is set to the stack pointer plus the given offset *) +(*c Integer arithmetic: *) + | Ocast8signed: operation (**r [rd] is 8-bit sign extension of [r1] *) + | Ocast8unsigned: operation (**r [rd] is 8-bit zero extension of [r1] *) + | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) + | Ocast16unsigned: operation (**r [rd] is 16-bit zero extension of [r1] *) + | Oadd: operation (**r [rd = r1 + r2] *) + | Oaddshift: shift -> operation (**r [rd = r1 + shifted r2] *) + | Oaddimm: int -> operation (**r [rd = r1 + n] *) + | Osub: operation (**r [rd = r1 - r2] *) + | Osubshift: shift -> operation (**r [rd = r1 - shifted r2] *) + | Orsubshift: shift -> operation (**r [rd = shifted r2 - r1] *) + | Orsubimm: int -> operation (**r [rd = r1 - n] *) + | Omul: operation (**r [rd = r1 * r2] *) + | Odiv: operation (**r [rd = r1 / r2] (signed) *) + | Odivu: operation (**r [rd = r1 / r2] (unsigned) *) + | Oand: operation (**r [rd = r1 & r2] *) + | Oandshift: shift -> operation (**r [rd = r1 & shifted r2] *) + | Oandimm: int -> operation (**r [rd = r1 & n] *) + | Oor: operation (**r [rd = r1 | r2] *) + | Oorshift: shift -> operation (**r [rd = r1 | shifted r2] *) + | Oorimm: int -> operation (**r [rd = r1 | n] *) + | Oxor: operation (**r [rd = r1 ^ r2] *) + | Oxorshift: shift -> operation (**r [rd = r1 ^ shifted r2] *) + | Oxorimm: int -> operation (**r [rd = r1 ^ n] *) + | Obic: operation (**r [rd = r1 & ~r2] *) + | Obicshift: shift -> operation (**r [rd = r1 & ~(shifted r2)] *) + | Onot: operation (**r [rd = ~r1] *) + | Onotshift: shift -> operation (**r [rd = ~(shifted r1)] *) + | Oshl: operation (**r [rd = r1 << r2] *) + | Oshr: operation (**r [rd = r1 >> r2] (signed) *) + | Oshru: operation (**r [rd = r1 >> r2] (unsigned) *) + | Oshift: shift -> operation (**r [rd = shifted r1] *) + | Oshrximm: int -> operation (**r [rd = r1 / 2^n] (signed) *) +(*c Floating-point arithmetic: *) + | Onegf: operation (**r [rd = - r1] *) + | Oabsf: operation (**r [rd = abs(r1)] *) + | Oaddf: operation (**r [rd = r1 + r2] *) + | Osubf: operation (**r [rd = r1 - r2] *) + | Omulf: operation (**r [rd = r1 * r2] *) + | Odivf: operation (**r [rd = r1 / r2] *) + | Osingleoffloat: operation (**r [rd] is [r1] truncated to single-precision float *) +(*c Conversions between int and float: *) + | Ointoffloat: operation (**r [rd = int_of_float(r1)] *) + | Ointuoffloat: operation (**r [rd = unsigned_int_of_float(r1)] *) + | Ofloatofint: operation (**r [rd = float_of_signed_int(r1)] *) + | Ofloatofintu: operation (**r [rd = float_of_unsigned_int(r1)] *) +(*c Boolean tests: *) + | Ocmp: condition -> operation. (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + +(** Addressing modes. [r1], [r2], etc, are the arguments to the + addressing. *) + +Inductive addressing: Set := + | Aindexed: int -> addressing (**r Address is [r1 + offset] *) + | Aindexed2: addressing (**r Address is [r1 + r2] *) + | Aindexed2shift: shift -> addressing (**r Address is [r1 + shifted r2] *) + | Ainstack: int -> addressing. (**r Address is [stack_pointer + offset] *) + +(** Comparison functions (used in module [CSE]). *) + +Definition eq_shift (x y: shift): {x=y} + {x<>y}. +Proof. + generalize Int.eq_dec; intro. + assert (forall (x y: shift_amount), {x=y}+{x<>y}). + destruct x as [x Px]. destruct y as [y Py]. destruct (H x y). + subst x. rewrite (proof_irrelevance _ Px Py). left; auto. + right. red; intro. elim n. inversion H0. auto. + decide equality. +Qed. + +Definition eq_operation (x y: operation): {x=y} + {x<>y}. +Proof. + generalize Int.eq_dec; intro. + generalize Float.eq_dec; intro. + assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. + generalize eq_shift; intro. + assert (forall (x y: comparison), {x=y}+{x<>y}). decide equality. + assert (forall (x y: condition), {x=y}+{x<>y}). decide equality. + decide equality. +Qed. + +Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. +Proof. + generalize Int.eq_dec; intro. + generalize eq_shift; intro. + decide equality. +Qed. + +(** Evaluation of conditions, operators and addressing modes applied + to lists of values. Return [None] when the computation is undefined: + wrong number of arguments, arguments of the wrong types, undefined + operations such as division by zero. [eval_condition] returns a boolean, + [eval_operation] and [eval_addressing] return a value. *) + +Definition eval_compare_mismatch (c: comparison) : option bool := + match c with Ceq => Some false | Cne => Some true | _ => None end. + +Definition eval_compare_null (c: comparison) (n: int) : option bool := + if Int.eq n Int.zero + then match c with Ceq => Some false | Cne => Some true | _ => None end + else None. + +Definition eval_shift (s: shift) (n: int) : int := + match s with + | Slsl x => Int.shl n (s_amount x) + | Slsr x => Int.shru n (s_amount x) + | Sasr x => Int.shr n (s_amount x) + | Sror x => Int.ror n (s_amount x) + end. + +Definition eval_condition (cond: condition) (vl: list val) (m: mem): + option bool := + match cond, vl with + | Ccomp c, Vint n1 :: Vint n2 :: nil => + Some (Int.cmp c n1 n2) + | Ccomp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => + if valid_pointer m b1 (Int.signed n1) + && valid_pointer m b2 (Int.signed n2) then + if eq_block b1 b2 + then Some (Int.cmp c n1 n2) + else eval_compare_mismatch c + else None + | Ccomp c, Vptr b1 n1 :: Vint n2 :: nil => + eval_compare_null c n2 + | Ccomp c, Vint n1 :: Vptr b2 n2 :: nil => + eval_compare_null c n1 + | Ccompu c, Vint n1 :: Vint n2 :: nil => + Some (Int.cmpu c n1 n2) + | Ccompshift c s, Vint n1 :: Vint n2 :: nil => + Some (Int.cmp c n1 (eval_shift s n2)) + | Ccompshift c s, Vptr b1 n1 :: Vint n2 :: nil => + eval_compare_null c (eval_shift s n2) + | Ccompushift c s, Vint n1 :: Vint n2 :: nil => + Some (Int.cmpu c n1 (eval_shift s n2)) + | Ccompimm c n, Vint n1 :: nil => + Some (Int.cmp c n1 n) + | Ccompimm c n, Vptr b1 n1 :: nil => + eval_compare_null c n + | Ccompuimm c n, Vint n1 :: nil => + Some (Int.cmpu c n1 n) + | Ccompf c, Vfloat f1 :: Vfloat f2 :: nil => + Some (Float.cmp c f1 f2) + | Cnotcompf c, Vfloat f1 :: Vfloat f2 :: nil => + Some (negb (Float.cmp c f1 f2)) + | _, _ => + None + end. + +Definition offset_sp (sp: val) (delta: int) : option val := + match sp with + | Vptr b n => Some (Vptr b (Int.add n delta)) + | _ => None + end. + +Definition eval_operation + (F: Set) (genv: Genv.t F) (sp: val) + (op: operation) (vl: list val) (m: mem): option val := + match op, vl with + | Omove, v1::nil => Some v1 + | Ointconst n, nil => Some (Vint n) + | Ofloatconst n, nil => Some (Vfloat n) + | Oaddrsymbol s ofs, nil => + match Genv.find_symbol genv s with + | None => None + | Some b => Some (Vptr b ofs) + end + | Oaddrstack ofs, nil => offset_sp sp ofs + | Ocast8signed, v1 :: nil => Some (Val.sign_ext 8 v1) + | Ocast8unsigned, v1 :: nil => Some (Val.zero_ext 8 v1) + | Ocast16signed, v1 :: nil => Some (Val.sign_ext 16 v1) + | Ocast16unsigned, v1 :: nil => Some (Val.zero_ext 16 v1) + | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2)) + | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1)) + | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2)) + | Oaddshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 (eval_shift s n2))) + | Oaddshift s, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 (eval_shift s n2))) + | Oaddimm n, Vint n1 :: nil => Some (Vint (Int.add n1 n)) + | Oaddimm n, Vptr b1 n1 :: nil => Some (Vptr b1 (Int.add n1 n)) + | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2)) + | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2)) + | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil => + if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None + | Osubshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 (eval_shift s n2))) + | Osubshift s, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 (eval_shift s n2))) + | Orsubshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub (eval_shift s n2) n1)) + | Orsubimm n, Vint n1 :: nil => Some (Vint (Int.sub n n1)) + | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2)) + | Odiv, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2)) + | Odivu, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) + | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2)) + | Oandshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 (eval_shift s n2))) + | Oandimm n, Vint n1 :: nil => Some (Vint (Int.and n1 n)) + | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2)) + | Oorshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 (eval_shift s n2))) + | Oorimm n, Vint n1 :: nil => Some (Vint (Int.or n1 n)) + | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2)) + | Oxorshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 (eval_shift s n2))) + | Oxorimm n, Vint n1 :: nil => Some (Vint (Int.xor n1 n)) + | Obic, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 (Int.not n2))) + | Obicshift s, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 (Int.not (eval_shift s n2)))) + | Onot, Vint n1 :: nil => Some (Vint (Int.not n1)) + | Onotshift s, Vint n1 :: nil => Some (Vint (Int.not (eval_shift s n1))) + | Oshl, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None + | Oshr, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None + | Oshru, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None + | Oshift s, Vint n :: nil => Some (Vint (eval_shift s n)) + | Oshrximm n, Vint n1 :: nil => + if Int.ltu n (Int.repr 31) then Some (Vint (Int.shrx n1 n)) else None + | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) + | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1)) + | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2)) + | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2)) + | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2)) + | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2)) + | Osingleoffloat, v1 :: nil => + Some (Val.singleoffloat v1) + | Ointoffloat, Vfloat f1 :: nil => + Some (Vint (Float.intoffloat f1)) + | Ointuoffloat, Vfloat f1 :: nil => + Some (Vint (Float.intuoffloat f1)) + | Ofloatofint, Vint n1 :: nil => + Some (Vfloat (Float.floatofint n1)) + | Ofloatofintu, Vint n1 :: nil => + Some (Vfloat (Float.floatofintu n1)) + | Ocmp c, _ => + match eval_condition c vl m with + | None => None + | Some false => Some Vfalse + | Some true => Some Vtrue + end + | _, _ => None + end. + +Definition eval_addressing + (F: Set) (genv: Genv.t F) (sp: val) + (addr: addressing) (vl: list val) : option val := + match addr, vl with + | Aindexed n, Vptr b1 n1 :: nil => + Some (Vptr b1 (Int.add n1 n)) + | Aindexed2, Vptr b1 n1 :: Vint n2 :: nil => + Some (Vptr b1 (Int.add n1 n2)) + | Aindexed2, Vint n1 :: Vptr b2 n2 :: nil => + Some (Vptr b2 (Int.add n1 n2)) + | Aindexed2shift s, Vptr b1 n1 :: Vint n2 :: nil => + Some (Vptr b1 (Int.add n1 (eval_shift s n2))) + | Ainstack ofs, nil => + offset_sp sp ofs + | _, _ => None + end. + +Definition negate_condition (cond: condition): condition := + match cond with + | Ccomp c => Ccomp(negate_comparison c) + | Ccompu c => Ccompu(negate_comparison c) + | Ccompshift c s => Ccompshift (negate_comparison c) s + | Ccompushift c s => Ccompushift (negate_comparison c) s + | Ccompimm c n => Ccompimm (negate_comparison c) n + | Ccompuimm c n => Ccompuimm (negate_comparison c) n + | Ccompf c => Cnotcompf c + | Cnotcompf c => Ccompf c + end. + +Ltac FuncInv := + match goal with + | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => + destruct x; simpl in H; try discriminate; FuncInv + | H: (match ?v with Vundef => _ | Vint _ => _ | Vfloat _ => _ | Vptr _ _ => _ end = Some _) |- _ => + destruct v; simpl in H; try discriminate; FuncInv + | H: (Some _ = Some _) |- _ => + injection H; intros; clear H; FuncInv + | _ => + idtac + end. + +Remark eval_negate_compare_null: + forall c n b, + eval_compare_null c n = Some b -> + eval_compare_null (negate_comparison c) n = Some (negb b). +Proof. + intros until b. unfold eval_compare_null. + case (Int.eq n Int.zero). + destruct c; intro EQ; simplify_eq EQ; intros; subst b; reflexivity. + intro; discriminate. +Qed. + +Lemma eval_negate_condition: + forall (cond: condition) (vl: list val) (b: bool) (m: mem), + eval_condition cond vl m = Some b -> + eval_condition (negate_condition cond) vl m = Some (negb b). +Proof. + intros. + destruct cond; simpl in H; FuncInv; try subst b; simpl. + rewrite Int.negate_cmp. auto. + apply eval_negate_compare_null; auto. + apply eval_negate_compare_null; auto. + destruct (valid_pointer m b0 (Int.signed i) && + valid_pointer m b1 (Int.signed i0)). + destruct (eq_block b0 b1). rewrite Int.negate_cmp. congruence. + destruct c; simpl in H; inv H; auto. + discriminate. + rewrite Int.negate_cmpu. auto. + rewrite Int.negate_cmp. auto. + apply eval_negate_compare_null; auto. + rewrite Int.negate_cmpu. auto. + rewrite Int.negate_cmp. auto. + apply eval_negate_compare_null; auto. + rewrite Int.negate_cmpu. auto. + auto. + rewrite negb_elim. auto. +Qed. + +(** [eval_operation] and [eval_addressing] depend on a global environment + for resolving references to global symbols. We show that they give + the same results if a global environment is replaced by another that + assigns the same addresses to the same symbols. *) + +Section GENV_TRANSF. + +Variable F1 F2: Set. +Variable ge1: Genv.t F1. +Variable ge2: Genv.t F2. +Hypothesis agree_on_symbols: + forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. + +Lemma eval_operation_preserved: + forall sp op vl m, + eval_operation ge2 sp op vl m = eval_operation ge1 sp op vl m. +Proof. + intros. + unfold eval_operation; destruct op; try rewrite agree_on_symbols; + reflexivity. +Qed. + +Lemma eval_addressing_preserved: + forall sp addr vl, + eval_addressing ge2 sp addr vl = eval_addressing ge1 sp addr vl. +Proof. + intros. + assert (UNUSED: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s). + exact agree_on_symbols. + unfold eval_addressing; destruct addr; try rewrite agree_on_symbols; + reflexivity. +Qed. + +End GENV_TRANSF. + +(** [eval_condition] and [eval_operation] depend on a memory store + (to check pointer validity in pointer comparisons). + We show that their results are preserved by a change of + memory if this change preserves pointer validity. + In particular, this holds in case of a memory allocation + or a memory store. *) + +Lemma eval_condition_change_mem: + forall m m' c args b, + (forall b ofs, valid_pointer m b ofs = true -> valid_pointer m' b ofs = true) -> + eval_condition c args m = Some b -> eval_condition c args m' = Some b. +Proof. + intros until b. intro INV. destruct c; simpl; auto. + destruct args; auto. destruct v; auto. destruct args; auto. + destruct v; auto. destruct args; auto. + caseEq (valid_pointer m b0 (Int.signed i)); intro. + caseEq (valid_pointer m b1 (Int.signed i0)); intro. + simpl. rewrite (INV _ _ H). rewrite (INV _ _ H0). auto. + simpl; congruence. simpl; congruence. +Qed. + +Lemma eval_operation_change_mem: + forall (F: Set) m m' (ge: Genv.t F) sp op args v, + (forall b ofs, valid_pointer m b ofs = true -> valid_pointer m' b ofs = true) -> + eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v. +Proof. + intros until v; intro INV. destruct op; simpl; auto. + caseEq (eval_condition c args m); intros. + rewrite (eval_condition_change_mem _ _ _ _ INV H). auto. + discriminate. +Qed. + +Lemma eval_condition_alloc: + forall m lo hi m' b c args v, + Mem.alloc m lo hi = (m', b) -> + eval_condition c args m = Some v -> eval_condition c args m' = Some v. +Proof. + intros. apply eval_condition_change_mem with m; auto. + intros. eapply valid_pointer_alloc; eauto. +Qed. + +Lemma eval_operation_alloc: + forall (F: Set) m lo hi m' b (ge: Genv.t F) sp op args v, + Mem.alloc m lo hi = (m', b) -> + eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v. +Proof. + intros. apply eval_operation_change_mem with m; auto. + intros. eapply valid_pointer_alloc; eauto. +Qed. + +Lemma eval_condition_store: + forall chunk m b ofs v' m' c args v, + Mem.store chunk m b ofs v' = Some m' -> + eval_condition c args m = Some v -> eval_condition c args m' = Some v. +Proof. + intros. apply eval_condition_change_mem with m; auto. + intros. eapply valid_pointer_store; eauto. +Qed. + +Lemma eval_operation_store: + forall (F: Set) chunk m b ofs v' m' (ge: Genv.t F) sp op args v, + Mem.store chunk m b ofs v' = Some m' -> + eval_operation ge sp op args m = Some v -> eval_operation ge sp op args m' = Some v. +Proof. + intros. apply eval_operation_change_mem with m; auto. + intros. eapply valid_pointer_store; eauto. +Qed. + +(** Recognition of move operations. *) + +Definition is_move_operation + (A: Set) (op: operation) (args: list A) : option A := + match op, args with + | Omove, arg :: nil => Some arg + | _, _ => None + end. + +Lemma is_move_operation_correct: + forall (A: Set) (op: operation) (args: list A) (a: A), + is_move_operation op args = Some a -> + op = Omove /\ args = a :: nil. +Proof. + intros until a. unfold is_move_operation; destruct op; + try (intros; discriminate). + destruct args. intros; discriminate. + destruct args. intros. intuition congruence. + intros; discriminate. +Qed. + +(** Static typing of conditions, operators and addressing modes. *) + +Definition type_of_condition (c: condition) : list typ := + match c with + | Ccomp _ => Tint :: Tint :: nil + | Ccompu _ => Tint :: Tint :: nil + | Ccompshift _ _ => Tint :: Tint :: nil + | Ccompushift _ _ => Tint :: Tint :: nil + | Ccompimm _ _ => Tint :: nil + | Ccompuimm _ _ => Tint :: nil + | Ccompf _ => Tfloat :: Tfloat :: nil + | Cnotcompf _ => Tfloat :: Tfloat :: nil + end. + +Definition type_of_operation (op: operation) : list typ * typ := + match op with + | Omove => (nil, Tint) (* treated specially *) + | Ointconst _ => (nil, Tint) + | Ofloatconst _ => (nil, Tfloat) + | Oaddrsymbol _ _ => (nil, Tint) + | Oaddrstack _ => (nil, Tint) + | Ocast8signed => (Tint :: nil, Tint) + | Ocast8unsigned => (Tint :: nil, Tint) + | Ocast16signed => (Tint :: nil, Tint) + | Ocast16unsigned => (Tint :: nil, Tint) + | Oadd => (Tint :: Tint :: nil, Tint) + | Oaddshift _ => (Tint :: Tint :: nil, Tint) + | Oaddimm _ => (Tint :: nil, Tint) + | Osub => (Tint :: Tint :: nil, Tint) + | Osubshift _ => (Tint :: Tint :: nil, Tint) + | Orsubshift _ => (Tint :: Tint :: nil, Tint) + | Orsubimm _ => (Tint :: nil, Tint) + | Omul => (Tint :: Tint :: nil, Tint) + | Odiv => (Tint :: Tint :: nil, Tint) + | Odivu => (Tint :: Tint :: nil, Tint) + | Oand => (Tint :: Tint :: nil, Tint) + | Oandshift _ => (Tint :: Tint :: nil, Tint) + | Oandimm _ => (Tint :: nil, Tint) + | Oor => (Tint :: Tint :: nil, Tint) + | Oorshift _ => (Tint :: Tint :: nil, Tint) + | Oorimm _ => (Tint :: nil, Tint) + | Oxor => (Tint :: Tint :: nil, Tint) + | Oxorshift _ => (Tint :: Tint :: nil, Tint) + | Oxorimm _ => (Tint :: nil, Tint) + | Obic => (Tint :: Tint :: nil, Tint) + | Obicshift _ => (Tint :: Tint :: nil, Tint) + | Onot => (Tint :: nil, Tint) + | Onotshift _ => (Tint :: nil, Tint) + | Oshl => (Tint :: Tint :: nil, Tint) + | Oshr => (Tint :: Tint :: nil, Tint) + | Oshru => (Tint :: Tint :: nil, Tint) + | Oshift _ => (Tint :: nil, Tint) + | Oshrximm _ => (Tint :: nil, Tint) + | Onegf => (Tfloat :: nil, Tfloat) + | Oabsf => (Tfloat :: nil, Tfloat) + | Oaddf => (Tfloat :: Tfloat :: nil, Tfloat) + | Osubf => (Tfloat :: Tfloat :: nil, Tfloat) + | Omulf => (Tfloat :: Tfloat :: nil, Tfloat) + | Odivf => (Tfloat :: Tfloat :: nil, Tfloat) + | Osingleoffloat => (Tfloat :: nil, Tfloat) + | Ointoffloat => (Tfloat :: nil, Tint) + | Ointuoffloat => (Tfloat :: nil, Tint) + | Ofloatofint => (Tint :: nil, Tfloat) + | Ofloatofintu => (Tint :: nil, Tfloat) + | Ocmp c => (type_of_condition c, Tint) + end. + +Definition type_of_addressing (addr: addressing) : list typ := + match addr with + | Aindexed _ => Tint :: nil + | Aindexed2 => Tint :: Tint :: nil + | Aindexed2shift _ => Tint :: Tint :: nil + | Ainstack _ => nil + end. + +Definition type_of_chunk (c: memory_chunk) : typ := + match c with + | Mint8signed => Tint + | Mint8unsigned => Tint + | Mint16signed => Tint + | Mint16unsigned => Tint + | Mint32 => Tint + | Mfloat32 => Tfloat + | Mfloat64 => Tfloat + end. + +(** Weak type soundness results for [eval_operation]: + the result values, when defined, are always of the type predicted + by [type_of_operation]. *) + +Section SOUNDNESS. + +Variable A: Set. +Variable genv: Genv.t A. + +Lemma type_of_operation_sound: + forall op vl sp v m, + op <> Omove -> + eval_operation genv sp op vl m = Some v -> + Val.has_type v (snd (type_of_operation op)). +Proof. + intros. + destruct op; simpl in H0; FuncInv; try subst v; try exact I. + congruence. + destruct (Genv.find_symbol genv i); simplify_eq H0; intro; subst v; exact I. + simpl. unfold offset_sp in H0. destruct sp; try discriminate. + inversion H0. exact I. + destruct v0; exact I. + destruct v0; exact I. + destruct v0; exact I. + destruct v0; exact I. + destruct (eq_block b b0). injection H0; intro; subst v; exact I. + discriminate. + destruct (Int.eq i0 Int.zero). discriminate. + injection H0; intro; subst v; exact I. + destruct (Int.eq i0 Int.zero). discriminate. + injection H0; intro; subst v; exact I. + destruct (Int.ltu i0 (Int.repr 32)). + injection H0; intro; subst v; exact I. discriminate. + destruct (Int.ltu i0 (Int.repr 32)). + injection H0; intro; subst v; exact I. discriminate. + destruct (Int.ltu i0 (Int.repr 32)). + injection H0; intro; subst v; exact I. discriminate. + destruct (Int.ltu i (Int.repr 31)). + injection H0; intro; subst v; exact I. discriminate. + destruct v0; exact I. + destruct (eval_condition c vl). + destruct b; injection H0; intro; subst v; exact I. + discriminate. +Qed. + +Lemma type_of_chunk_correct: + forall chunk m addr v, + Mem.loadv chunk m addr = Some v -> + Val.has_type v (type_of_chunk chunk). +Proof. + intro chunk. + assert (forall v, Val.has_type (Val.load_result chunk v) (type_of_chunk chunk)). + destruct v; destruct chunk; exact I. + intros until v. unfold Mem.loadv. + destruct addr; intros; try discriminate. + generalize (Mem.load_inv _ _ _ _ _ H0). + intros [X Y]. subst v. apply H. +Qed. + +End SOUNDNESS. + +(** Alternate definition of [eval_condition], [eval_op], [eval_addressing] + as total functions that return [Vundef] when not applicable + (instead of [None]). Used in the proof of [PPCgen]. *) + +Section EVAL_OP_TOTAL. + +Variable F: Set. +Variable genv: Genv.t F. + +Definition find_symbol_offset (id: ident) (ofs: int) : val := + match Genv.find_symbol genv id with + | Some b => Vptr b ofs + | None => Vundef + end. + +Definition eval_shift_total (s: shift) (v: val) : val := + match v with + | Vint n => Vint(eval_shift s n) + | _ => Vundef + end. + +Definition eval_condition_total (cond: condition) (vl: list val) : val := + match cond, vl with + | Ccomp c, v1::v2::nil => Val.cmp c v1 v2 + | Ccompu c, v1::v2::nil => Val.cmpu c v1 v2 + | Ccompshift c s, v1::v2::nil => Val.cmp c v1 (eval_shift_total s v2) + | Ccompushift c s, v1::v2::nil => Val.cmpu c v1 (eval_shift_total s v2) + | Ccompimm c n, v1::nil => Val.cmp c v1 (Vint n) + | Ccompuimm c n, v1::nil => Val.cmpu c v1 (Vint n) + | Ccompf c, v1::v2::nil => Val.cmpf c v1 v2 + | Cnotcompf c, v1::v2::nil => Val.notbool(Val.cmpf c v1 v2) + | _, _ => Vundef + end. + +Definition eval_operation_total (sp: val) (op: operation) (vl: list val) : val := + match op, vl with + | Omove, v1::nil => v1 + | Ointconst n, nil => Vint n + | Ofloatconst n, nil => Vfloat n + | Oaddrsymbol s ofs, nil => find_symbol_offset s ofs + | Oaddrstack ofs, nil => Val.add sp (Vint ofs) + | Ocast8signed, v1::nil => Val.sign_ext 8 v1 + | Ocast8unsigned, v1::nil => Val.zero_ext 8 v1 + | Ocast16signed, v1::nil => Val.sign_ext 16 v1 + | Ocast16unsigned, v1::nil => Val.zero_ext 16 v1 + | Oadd, v1::v2::nil => Val.add v1 v2 + | Oaddshift s, v1::v2::nil => Val.add v1 (eval_shift_total s v2) + | Oaddimm n, v1::nil => Val.add v1 (Vint n) + | Osub, v1::v2::nil => Val.sub v1 v2 + | Osubshift s, v1::v2::nil => Val.sub v1 (eval_shift_total s v2) + | Orsubshift s, v1::v2::nil => Val.sub (eval_shift_total s v2) v1 + | Orsubimm n, v1::nil => Val.sub (Vint n) v1 + | Omul, v1::v2::nil => Val.mul v1 v2 + | Odiv, v1::v2::nil => Val.divs v1 v2 + | Odivu, v1::v2::nil => Val.divu v1 v2 + | Oand, v1::v2::nil => Val.and v1 v2 + | Oandshift s, v1::v2::nil => Val.and v1 (eval_shift_total s v2) + | Oandimm n, v1::nil => Val.and v1 (Vint n) + | Oor, v1::v2::nil => Val.or v1 v2 + | Oorshift s, v1::v2::nil => Val.or v1 (eval_shift_total s v2) + | Oorimm n, v1::nil => Val.or v1 (Vint n) + | Oxor, v1::v2::nil => Val.xor v1 v2 + | Oxorshift s, v1::v2::nil => Val.xor v1 (eval_shift_total s v2) + | Oxorimm n, v1::nil => Val.xor v1 (Vint n) + | Obic, v1::v2::nil => Val.and v1 (Val.notint v2) + | Obicshift s, v1::v2::nil => Val.and v1 (Val.notint (eval_shift_total s v2)) + | Onot, v1::nil => Val.notint v1 + | Onotshift s, v1::nil => Val.notint (eval_shift_total s v1) + | Oshl, v1::v2::nil => Val.shl v1 v2 + | Oshr, v1::v2::nil => Val.shr v1 v2 + | Oshru, v1::v2::nil => Val.shru v1 v2 + | Oshrximm n, v1::nil => Val.shrx v1 (Vint n) + | Oshift s, v1::nil => eval_shift_total s v1 + | Onegf, v1::nil => Val.negf v1 + | Oabsf, v1::nil => Val.absf v1 + | Oaddf, v1::v2::nil => Val.addf v1 v2 + | Osubf, v1::v2::nil => Val.subf v1 v2 + | Omulf, v1::v2::nil => Val.mulf v1 v2 + | Odivf, v1::v2::nil => Val.divf v1 v2 + | Osingleoffloat, v1::nil => Val.singleoffloat v1 + | Ointoffloat, v1::nil => Val.intoffloat v1 + | Ointuoffloat, v1::nil => Val.intuoffloat v1 + | Ofloatofint, v1::nil => Val.floatofint v1 + | Ofloatofintu, v1::nil => Val.floatofintu v1 + | Ocmp c, _ => eval_condition_total c vl + | _, _ => Vundef + end. + +Definition eval_addressing_total + (sp: val) (addr: addressing) (vl: list val) : val := + match addr, vl with + | Aindexed n, v1::nil => Val.add v1 (Vint n) + | Aindexed2, v1::v2::nil => Val.add v1 v2 + | Aindexed2shift s, v1::v2::nil => Val.add v1 (eval_shift_total s v2) + | Ainstack ofs, nil => Val.add sp (Vint ofs) + | _, _ => Vundef + end. + +Lemma eval_compare_mismatch_weaken: + forall c b, + eval_compare_mismatch c = Some b -> + Val.cmp_mismatch c = Val.of_bool b. +Proof. + unfold eval_compare_mismatch. intros. destruct c; inv H; auto. +Qed. + +Lemma eval_compare_null_weaken: + forall c i b, + eval_compare_null c i = Some b -> + (if Int.eq i Int.zero then Val.cmp_mismatch c else Vundef) = Val.of_bool b. +Proof. + unfold eval_compare_null. intros. + destruct (Int.eq i Int.zero); try discriminate. + apply eval_compare_mismatch_weaken; auto. +Qed. + +Lemma eval_condition_weaken: + forall c vl m b, + eval_condition c vl m = Some b -> + eval_condition_total c vl = Val.of_bool b. +Proof. + intros. + unfold eval_condition in H; destruct c; FuncInv; + try subst b; try reflexivity; simpl; + try (apply eval_compare_null_weaken; auto). + destruct (valid_pointer m b0 (Int.signed i) && + valid_pointer m b1 (Int.signed i0)). + unfold eq_block in H. destruct (zeq b0 b1); try congruence. + apply eval_compare_mismatch_weaken; auto. + discriminate. + symmetry. apply Val.notbool_negb_1. +Qed. + +Lemma eval_operation_weaken: + forall sp op vl m v, + eval_operation genv sp op vl m = Some v -> + eval_operation_total sp op vl = v. +Proof. + intros. + unfold eval_operation in H; destruct op; FuncInv; + try subst v; try reflexivity; simpl. + unfold find_symbol_offset. + destruct (Genv.find_symbol genv i); try discriminate. + congruence. + unfold offset_sp in H. + destruct sp; try discriminate. simpl. congruence. + unfold eq_block in H. destruct (zeq b b0); congruence. + destruct (Int.eq i0 Int.zero); congruence. + destruct (Int.eq i0 Int.zero); congruence. + destruct (Int.ltu i0 (Int.repr 32)); congruence. + destruct (Int.ltu i0 (Int.repr 32)); congruence. + destruct (Int.ltu i0 (Int.repr 32)); congruence. + unfold Int.ltu in H. destruct (zlt (Int.unsigned i) (Int.unsigned (Int.repr 31))). + unfold Int.ltu. rewrite zlt_true. congruence. + assert (Int.unsigned (Int.repr 31) < Int.unsigned (Int.repr 32)). vm_compute; auto. + omega. discriminate. + caseEq (eval_condition c vl m); intros; rewrite H0 in H. + replace v with (Val.of_bool b). + eapply eval_condition_weaken; eauto. + destruct b; simpl; congruence. + discriminate. +Qed. + +Lemma eval_addressing_weaken: + forall sp addr vl v, + eval_addressing genv sp addr vl = Some v -> + eval_addressing_total sp addr vl = v. +Proof. + intros. + unfold eval_addressing in H; destruct addr; FuncInv; + try subst v; simpl; try reflexivity. + decEq. apply Int.add_commut. + unfold offset_sp in H. destruct sp; simpl; congruence. +Qed. + +Lemma eval_condition_total_is_bool: + forall cond vl, Val.is_bool (eval_condition_total cond vl). +Proof. + intros; destruct cond; + destruct vl; try apply Val.undef_is_bool; + destruct vl; try apply Val.undef_is_bool; + try (destruct vl; try apply Val.undef_is_bool); simpl. + apply Val.cmp_is_bool. + apply Val.cmpu_is_bool. + apply Val.cmp_is_bool. + apply Val.cmpu_is_bool. + apply Val.cmp_is_bool. + apply Val.cmpu_is_bool. + apply Val.cmpf_is_bool. + apply Val.notbool_is_bool. +Qed. + +End EVAL_OP_TOTAL. + +(** Compatibility of the evaluation functions with the + ``is less defined'' relation over values and memory states. *) + +Section EVAL_LESSDEF. + +Variable F: Set. +Variable genv: Genv.t F. +Variables m1 m2: mem. +Hypothesis MEM: Mem.lessdef m1 m2. + +Ltac InvLessdef := + match goal with + | [ H: Val.lessdef (Vint _) _ |- _ ] => + inv H; InvLessdef + | [ H: Val.lessdef (Vfloat _) _ |- _ ] => + inv H; InvLessdef + | [ H: Val.lessdef (Vptr _ _) _ |- _ ] => + inv H; InvLessdef + | [ H: Val.lessdef_list nil _ |- _ ] => + inv H; InvLessdef + | [ H: Val.lessdef_list (_ :: _) _ |- _ ] => + inv H; InvLessdef + | _ => idtac + end. + +Lemma eval_condition_lessdef: + forall cond vl1 vl2 b, + Val.lessdef_list vl1 vl2 -> + eval_condition cond vl1 m1 = Some b -> + eval_condition cond vl2 m2 = Some b. +Proof. + intros. destruct cond; simpl in *; FuncInv; InvLessdef; auto. + generalize H0. + caseEq (valid_pointer m1 b0 (Int.signed i)); intro; simpl; try congruence. + caseEq (valid_pointer m1 b1 (Int.signed i0)); intro; simpl; try congruence. + rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H1). + rewrite (Mem.valid_pointer_lessdef _ _ _ _ MEM H). simpl. auto. +Qed. + +Ltac TrivialExists := + match goal with + | [ |- exists v2, Some ?v1 = Some v2 /\ Val.lessdef ?v1 v2 ] => + exists v1; split; [auto | constructor] + | _ => idtac + end. + +Lemma eval_operation_lessdef: + forall sp op vl1 vl2 v1, + Val.lessdef_list vl1 vl2 -> + eval_operation genv sp op vl1 m1 = Some v1 -> + exists v2, eval_operation genv sp op vl2 m2 = Some v2 /\ Val.lessdef v1 v2. +Proof. + intros. destruct op; simpl in *; FuncInv; InvLessdef; TrivialExists. + exists v2; auto. + destruct (Genv.find_symbol genv i); inv H0. TrivialExists. + exists v1; auto. + exists (Val.sign_ext 8 v2); split. auto. apply Val.sign_ext_lessdef; auto. + exists (Val.zero_ext 8 v2); split. auto. apply Val.zero_ext_lessdef; auto. + exists (Val.sign_ext 16 v2); split. auto. apply Val.sign_ext_lessdef; auto. + exists (Val.zero_ext 16 v2); split. auto. apply Val.zero_ext_lessdef; auto. + destruct (eq_block b b0); inv H0. TrivialExists. + destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. + destruct (Int.eq i0 Int.zero); inv H0; TrivialExists. + destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. + destruct (Int.ltu i0 (Int.repr 32)); inv H0; TrivialExists. + destruct (Int.ltu i (Int.repr 32)); inv H0; TrivialExists. + destruct (Int.ltu i0 (Int.repr 32)); inv H1; TrivialExists. + destruct (Int.ltu i0 (Int.repr 32)); inv H1; TrivialExists. + destruct (Int.ltu i (Int.repr 31)); inv H0; TrivialExists. + exists (Val.singleoffloat v2); split. auto. apply Val.singleoffloat_lessdef; auto. + caseEq (eval_condition c vl1 m1); intros. rewrite H1 in H0. + rewrite (eval_condition_lessdef c H H1). + destruct b; inv H0; TrivialExists. + rewrite H1 in H0. discriminate. +Qed. + +Lemma eval_addressing_lessdef: + forall sp addr vl1 vl2 v1, + Val.lessdef_list vl1 vl2 -> + eval_addressing genv sp addr vl1 = Some v1 -> + exists v2, eval_addressing genv sp addr vl2 = Some v2 /\ Val.lessdef v1 v2. +Proof. + intros. destruct addr; simpl in *; FuncInv; InvLessdef; TrivialExists. + exists v1; auto. +Qed. + +End EVAL_LESSDEF. + +(** Recognition of integers that are valid shift amounts. *) + +Definition is_shift_amount_aux (n: int) : + { Int.ltu n (Int.repr 32) = true } + + { Int.ltu n (Int.repr 32) = false }. +Proof. + intro. case (Int.ltu n (Int.repr 32)). left; auto. right; auto. +Defined. + +Definition is_shift_amount (n: int) : option shift_amount := + match is_shift_amount_aux n with + | left H => Some(mk_shift_amount n H) + | right _ => None + end. + +Lemma is_shift_amount_Some: + forall n s, is_shift_amount n = Some s -> s_amount s = n. +Proof. + intros until s. unfold is_shift_amount. + destruct (is_shift_amount_aux n). + simpl. intros. inv H. reflexivity. + congruence. +Qed. + +Lemma is_shift_amount_None: + forall n, is_shift_amount n = None -> Int.ltu n (Int.repr 32) = true -> False. +Proof. + intro n. unfold is_shift_amount. + destruct (is_shift_amount_aux n). + congruence. + congruence. +Qed. + +(** Transformation of addressing modes with two operands or more + into an equivalent arithmetic operation. This is used in the [Reload] + pass when a store instruction cannot be reloaded directly because + it runs out of temporary registers. *) + +(** For the ARM, there are only two binary addressing mode: [Aindexed2] + and [Aindexed2shift]. The corresponding operations are [Oadd] + and [Oaddshift]. *) + +Definition op_for_binary_addressing (addr: addressing) : operation := + match addr with + | Aindexed2 => Oadd + | Aindexed2shift s => Oaddshift s + | _ => Ointconst Int.zero (* never happens *) + end. + +Lemma eval_op_for_binary_addressing: + forall (F: Set) (ge: Genv.t F) sp addr args m v, + (length args >= 2)%nat -> + eval_addressing ge sp addr args = Some v -> + eval_operation ge sp (op_for_binary_addressing addr) args m = Some v. +Proof. + intros. + unfold eval_addressing in H0; destruct addr; FuncInv; simpl in H; try omegaContradiction; simpl. + rewrite Int.add_commut. congruence. + congruence. + congruence. +Qed. + +Lemma type_op_for_binary_addressing: + forall addr, + (length (type_of_addressing addr) >= 2)%nat -> + type_of_operation (op_for_binary_addressing addr) = (type_of_addressing addr, Tint). +Proof. + intros. destruct addr; simpl in H; reflexivity || omegaContradiction. +Qed. -- cgit