From be4d6e42dfa287b93b1a35ec820ab2a5aaf8c7ec Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 19 May 2013 09:54:40 +0000 Subject: Merge of the float32 branch: - added RTL type "Tsingle" - ABI-compatible passing of single-precision floats on ARM and x86 git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2260 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/AST.v | 73 ++++- common/Events.v | 76 +++-- common/Memdata.v | 2 +- common/PrintAST.ml | 6 +- common/Subtyping.v | 808 +++++++++++++++++++++++++++++++++++++++++++++++++++++ common/Values.v | 45 ++- 6 files changed, 967 insertions(+), 43 deletions(-) create mode 100644 common/Subtyping.v (limited to 'common') diff --git a/common/AST.v b/common/AST.v index fba5354..1b1e872 100644 --- a/common/AST.v +++ b/common/AST.v @@ -35,17 +35,19 @@ Definition ident_eq := peq. Parameter ident_of_string : String.string -> ident. -(** The intermediate languages are weakly typed, using only three +(** The intermediate languages are weakly typed, using only four types: [Tint] for 32-bit integers and pointers, [Tfloat] for 64-bit - floating-point numbers, [Tlong] for 64-bit integers. *) + floating-point numbers, [Tlong] for 64-bit integers, [Tsingle] + for 32-bit floating-point numbers. *) Inductive typ : Type := | Tint | Tfloat - | Tlong. + | Tlong + | Tsingle. Definition typesize (ty: typ) : Z := - match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 end. + match ty with Tint => 4 | Tfloat => 8 | Tlong => 8 | Tsingle => 4 end. Lemma typesize_pos: forall ty, typesize ty > 0. Proof. destruct ty; simpl; omega. Qed. @@ -60,6 +62,26 @@ Definition opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2} Definition list_typ_eq: forall (l1 l2: list typ), {l1=l2} + {l1<>l2} := list_eq_dec typ_eq. +(** All values of type [Tsingle] are also of type [Tfloat]. This + corresponds to the following subtyping relation over types. *) + +Definition subtype (ty1 ty2: typ) : bool := + match ty1, ty2 with + | Tint, Tint => true + | Tlong, Tlong => true + | Tfloat, Tfloat => true + | Tsingle, Tsingle => true + | Tsingle, Tfloat => true + | _, _ => false + end. + +Fixpoint subtype_list (tyl1 tyl2: list typ) : bool := + match tyl1, tyl2 with + | nil, nil => true + | ty1::tys1, ty2::tys2 => subtype ty1 ty2 && subtype_list tys1 tys2 + | _, _ => false + end. + (** Additionally, function definitions and function calls are annotated by function signatures indicating the number and types of arguments, as well as the type of the returned value if any. These signatures @@ -103,6 +125,19 @@ Global Opaque chunk_eq. (** The type (integer/pointer or float) of a chunk. *) Definition type_of_chunk (c: memory_chunk) : typ := + match c with + | Mint8signed => Tint + | Mint8unsigned => Tint + | Mint16signed => Tint + | Mint16unsigned => Tint + | Mint32 => Tint + | Mint64 => Tlong + | Mfloat32 => Tsingle + | Mfloat64 => Tfloat + | Mfloat64al32 => Tfloat + end. + +Definition type_of_chunk_use (c: memory_chunk) : typ := match c with | Mint8signed => Tint | Mint8unsigned => Tint @@ -123,6 +158,7 @@ Definition chunk_of_type (ty: typ) := | Tint => Mint32 | Tfloat => Mfloat64al32 | Tlong => Mint64 + | Tsingle => Mfloat32 end. (** Initialization data for global variables. *) @@ -283,6 +319,25 @@ Proof. exploit IHl; eauto. intros [v' [P Q]]; exists v'; auto. Qed. +Lemma transform_partial_program2_succeeds: + forall p tp i g, + transform_partial_program2 p = OK tp -> + In (i, g) p.(prog_defs) -> + match g with + | Gfun fd => exists tfd, transf_fun fd = OK tfd + | Gvar gv => exists tv, transf_var gv.(gvar_info) = OK tv + end. +Proof. + intros. monadInv H. + revert x EQ H0. induction (prog_defs p); simpl; intros. + contradiction. + destruct a as [id1 g1]. destruct g1. + destruct (transf_fun f) eqn:TF; try discriminate. monadInv EQ. + destruct H0. inv H. econstructor; eauto. eapply IHl; eauto. + destruct (transf_globvar v) eqn:TV; try discriminate. monadInv EQ. + destruct H0. inv H. monadInv TV. econstructor; eauto. eapply IHl; eauto. +Qed. + Lemma transform_partial_program2_main: forall p tp, transform_partial_program2 p = OK tp -> @@ -353,6 +408,16 @@ Proof. apply transform_partial_program2_function. Qed. +Lemma transform_partial_program_succeeds: + forall p tp i fd, + transform_partial_program p = OK tp -> + In (i, Gfun fd) p.(prog_defs) -> + exists tfd, transf_partial fd = OK tfd. +Proof. + unfold transform_partial_program; intros. + exploit transform_partial_program2_succeeds; eauto. +Qed. + End TRANSF_PARTIAL_PROGRAM. Lemma transform_program_partial_program: diff --git a/common/Events.v b/common/Events.v index f342799..be1915a 100644 --- a/common/Events.v +++ b/common/Events.v @@ -57,6 +57,7 @@ Inductive eventval: Type := | EVint: int -> eventval | EVlong: int64 -> eventval | EVfloat: float -> eventval + | EVfloatsingle: float -> eventval | EVptr_global: ident -> int -> eventval. Inductive event: Type := @@ -272,6 +273,9 @@ Inductive eventval_match: eventval -> typ -> val -> Prop := eventval_match (EVlong i) Tlong (Vlong i) | ev_match_float: forall f, eventval_match (EVfloat f) Tfloat (Vfloat f) + | ev_match_single: forall f, + Float.is_single f -> + eventval_match (EVfloatsingle f) Tsingle (Vfloat f) | ev_match_ptr: forall id b ofs, Genv.find_symbol ge id = Some b -> eventval_match (EVptr_global id ofs) Tint (Vptr b ofs). @@ -291,7 +295,7 @@ Lemma eventval_match_type: forall ev ty v, eventval_match ev ty v -> Val.has_type v ty. Proof. - intros. inv H; constructor. + intros. inv H; simpl; auto. Qed. Lemma eventval_list_match_length: @@ -330,7 +334,7 @@ Lemma eventval_match_inject: forall ev ty v1 v2, eventval_match ev ty v1 -> val_inject f v1 v2 -> eventval_match ev ty v2. Proof. - intros. inv H; inv H0; try constructor. + intros. inv H; inv H0; try constructor; auto. destruct glob_pres as [A [B C]]. exploit A; eauto. intro EQ; rewrite H3 in EQ; inv EQ. rewrite Int.add_zero. econstructor; eauto. @@ -384,6 +388,7 @@ Definition eventval_valid (ev: eventval) : Prop := | EVint _ => True | EVlong _ => True | EVfloat _ => True + | EVfloatsingle f => Float.is_single f | EVptr_global id ofs => exists b, Genv.find_symbol ge id = Some b end. @@ -392,25 +397,37 @@ Definition eventval_type (ev: eventval) : typ := | EVint _ => Tint | EVlong _ => Tlong | EVfloat _ => Tfloat + | EVfloatsingle _ => Tsingle | EVptr_global id ofs => Tint end. -Lemma eventval_valid_match: - forall ev ty, - eventval_valid ev -> eventval_type ev = ty -> exists v, eventval_match ev ty v. -Proof. - intros. subst ty. destruct ev; simpl in *. +Lemma eventval_match_receptive: + forall ev1 ty v1 ev2, + eventval_match ev1 ty v1 -> + eventval_valid ev1 -> eventval_valid ev2 -> eventval_type ev1 = eventval_type ev2 -> + exists v2, eventval_match ev2 ty v2. +Proof. + intros. inv H; destruct ev2; simpl in H2; try discriminate. + exists (Vint i0); constructor. + destruct H1 as [b EQ]. exists (Vptr b i1); constructor; auto. + exists (Vlong i0); constructor. + exists (Vfloat f1); constructor. + exists (Vfloat f1); constructor; auto. exists (Vint i); constructor. - exists (Vlong i); constructor. - exists (Vfloat f0); constructor. - destruct H as [b A]. exists (Vptr b i0); constructor; auto. + destruct H1 as [b' EQ]. exists (Vptr b' i0); constructor; auto. Qed. Lemma eventval_match_valid: - forall ev ty v, - eventval_match ev ty v -> eventval_valid ev /\ eventval_type ev = ty. + forall ev ty v, eventval_match ev ty v -> eventval_valid ev. Proof. - induction 1; simpl; auto. split; auto. exists b; auto. + destruct 1; simpl; auto. exists b; auto. +Qed. + +Lemma eventval_match_same_type: + forall ev1 ty v1 ev2 v2, + eventval_match ev1 ty v1 -> eventval_match ev2 ty v2 -> eventval_type ev1 = eventval_type ev2. +Proof. + destruct 1; intros EV; inv EV; auto. Qed. End EVENTVAL. @@ -430,7 +447,7 @@ Lemma eventval_match_preserved: forall ev ty v, eventval_match ge1 ev ty v -> eventval_match ge2 ev ty v. Proof. - induction 1; constructor. rewrite symbols_preserved; auto. + induction 1; constructor; auto. rewrite symbols_preserved; auto. Qed. Lemma eventval_list_match_preserved: @@ -753,9 +770,8 @@ Lemma volatile_load_receptive: exists v2, volatile_load ge chunk m b ofs t2 v2. Proof. intros. inv H; inv H0. - exploit eventval_match_valid; eauto. intros [A B]. - exploit eventval_valid_match. eexact H9. rewrite <- H10; eauto. - intros [v' EVM]. exists (Val.load_result chunk v'). constructor; auto. + exploit eventval_match_receptive; eauto. intros [v' EM]. + exists (Val.load_result chunk v'). constructor; auto. exists v1; constructor; auto. Qed. @@ -766,8 +782,7 @@ Lemma volatile_load_ok: Proof. intros; constructor; intros. (* well typed *) - unfold proj_sig_res; simpl. inv H. inv H0. - destruct chunk; destruct v; simpl; constructor. + unfold proj_sig_res; simpl. inv H. inv H0. apply Val.load_result_type. eapply Mem.load_type; eauto. (* arity *) inv H; inv H0; auto. @@ -796,15 +811,17 @@ Proof. (* determ *) inv H; inv H0. inv H1; inv H7; try congruence. assert (id = id0) by (eapply Genv.genv_vars_inj; eauto). subst id0. - exploit eventval_match_valid. eexact H2. intros [V1 T1]. - exploit eventval_match_valid. eexact H4. intros [V2 T2]. - split. constructor; auto. congruence. + split. constructor. + eapply eventval_match_valid; eauto. + eapply eventval_match_valid; eauto. + eapply eventval_match_same_type; eauto. intros EQ; inv EQ. assert (v = v0) by (eapply eventval_match_determ_1; eauto). subst v0. auto. split. constructor. intuition congruence. Qed. + Inductive volatile_load_global_sem (chunk: memory_chunk) (id: ident) (ofs: int) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := @@ -830,8 +847,7 @@ Lemma volatile_load_global_ok: Proof. intros; constructor; intros. (* well typed *) - unfold proj_sig_res; simpl. inv H. inv H1. - destruct chunk; destruct v; simpl; constructor. + unfold proj_sig_res; simpl. inv H. inv H1. apply Val.load_result_type. eapply Mem.load_type; eauto. (* arity *) inv H; inv H1; auto. @@ -1450,15 +1466,15 @@ Proof. inv H; simpl; omega. (* receptive *) inv H; inv H0. - exploit eventval_match_valid; eauto. intros [A B]. - exploit eventval_valid_match. eexact H7. rewrite <- H8; eauto. - intros [v' EVM]. exists v'; exists m1. econstructor; eauto. + exploit eventval_match_receptive; eauto. intros [v' EVM]. + exists v'; exists m1. econstructor; eauto. (* determ *) inv H; inv H0. assert (args = args0). eapply eventval_list_match_determ_2; eauto. subst args0. - exploit eventval_match_valid. eexact H2. intros [V1 T1]. - exploit eventval_match_valid. eexact H3. intros [V2 T2]. - split. constructor; auto. congruence. + split. constructor. + eapply eventval_match_valid; eauto. + eapply eventval_match_valid; eauto. + eapply eventval_match_same_type; eauto. intros EQ; inv EQ. split; auto. eapply eventval_match_determ_1; eauto. Qed. diff --git a/common/Memdata.v b/common/Memdata.v index c62ba99..47f8471 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -473,7 +473,7 @@ Lemma decode_val_type: Proof. intros. unfold decode_val. destruct (proj_bytes cl). - destruct chunk; simpl; auto. + destruct chunk; simpl; auto. apply Float.single_of_bits_is_single. destruct chunk; simpl; auto. unfold proj_pointer. destruct cl; try (exact I). destruct m; try (exact I). diff --git a/common/PrintAST.ml b/common/PrintAST.ml index c18b09d..9768447 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -16,7 +16,11 @@ open Printf open Camlcoq open AST -let name_of_type = function Tint -> "int" | Tfloat -> "float" | Tlong -> "long" +let name_of_type = function + | Tint -> "int" + | Tfloat -> "float" + | Tlong -> "long" + | Tsingle -> "single" let name_of_chunk = function | Mint8signed -> "int8signed" diff --git a/common/Subtyping.v b/common/Subtyping.v new file mode 100644 index 0000000..e1bf61a --- /dev/null +++ b/common/Subtyping.v @@ -0,0 +1,808 @@ +(* *********************************************************************) +(* *) +(* 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 GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* A solver for subtyping constraints. *) + +Require Import Recdef Coqlib Maps Errors. + +Local Open Scope nat_scope. +Local Open Scope error_monad_scope. + +(** This module provides a solver for sets of subtyping constraints of the + following kinds: [base-type <: T(x)] or [T(x) <: base-type] or [T(x) <: T(y)]. + The unknowns are the types [T(x)] of every identifier [x]. *) + +(** The interface for base types and the subtyping relation. *) + +Module Type TYPE_ALGEBRA. + +(** Type expressions *) + +Variable t: Type. +Variable eq: forall (x y: t), {x=y} + {x<>y}. +Variable default: t. + +(** Subtyping *) + +Variable sub: t -> t -> Prop. +Hypothesis sub_refl: forall x, sub x x. +Hypothesis sub_trans: forall x y z, sub x y -> sub y z -> sub x z. +Variable sub_dec: forall x y, {sub x y} + {~sub x y}. + +(** Least upper bounds. [lub x y] is specified only when [x] and [y] have + a common supertype; it can be arbitrary otherwise. *) + +Variable lub: t -> t -> t. +Hypothesis lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y). +Hypothesis lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y). +Hypothesis lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z. + +(** Greater lower bounds. [glb x y] is specified only when [x] and [y] have + a common subtype; it can be arbitrary otherwise.*) + +Variable glb: t -> t -> t. +Hypothesis glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x. +Hypothesis glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y. +Hypothesis glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y). + +(** Low and high bounds for a given type. *) +Variable low_bound: t -> t. +Variable high_bound: t -> t. +Hypothesis low_bound_sub: forall t, sub (low_bound t) t. +Hypothesis low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x. +Hypothesis high_bound_sub: forall t, sub t (high_bound t). +Hypothesis high_bound_majorant: forall x y, sub x y -> sub y (high_bound x). + +(** Measure over types *) + +Variable weight: t -> nat. +Variable max_weight: nat. +Hypothesis weight_range: forall t, weight t <= max_weight. +Hypothesis weight_sub: forall x y, sub x y -> weight x <= weight y. +Hypothesis weight_sub_strict: forall x y, sub x y -> x <> y -> weight x < weight y. + +End TYPE_ALGEBRA. + +(** The constraint solver. *) + +Module SubSolver (T: TYPE_ALGEBRA). + +(* The current set of constraints is represented by a record with two components: +- [te_typ]: a partial map from variables to pairs [tlo, thi] + of types, representing the low and high bounds for this variable. +- [te_sub]: a list of pairs [(x,y)] of variables, indicating that + the type of [x] must be a subtype of the type of [y]. +*) + +Inductive bounds : Type := B (lo: T.t) (hi: T.t) (SUB: T.sub lo hi). + +Definition constraint : Type := (positive * positive)%type. + +Record typenv : Type := Typenv { + te_typ: PTree.t bounds; (**r mapping var -> low & high bounds *) + te_sub: list constraint (**r additional subtyping constraints *) +}. + +Definition initial : typenv := {| te_typ := PTree.empty _; te_sub := nil |}. + +(** Add the constraint [ty <: T(x)]. *) + +Definition type_def (e: typenv) (x: positive) (ty: T.t) : res typenv := + match e.(te_typ)!x with + | None => + let b := B ty (T.high_bound ty) (T.high_bound_sub ty) in + OK {| te_typ := PTree.set x b e.(te_typ); + te_sub := e.(te_sub) |} + | Some(B lo hi s1) => + match T.sub_dec ty hi with + | left s2 => + let lo' := T.lub lo ty in + if T.eq lo lo' then OK e else + let b := B lo' hi (T.lub_min lo ty hi s1 s2) in + OK {| te_typ := PTree.set x b e.(te_typ); + te_sub := e.(te_sub) |} + | right _ => + Error (MSG "bad definition of variable " :: POS x :: nil) + end + end. + +Fixpoint type_defs (e: typenv) (rl: list positive) (tyl: list T.t) {struct rl}: res typenv := + match rl, tyl with + | nil, nil => OK e + | r1::rs, ty1::tys => do e1 <- type_def e r1 ty1; type_defs e1 rs tys + | _, _ => Error (msg "arity mismatch") + end. + +(** Add the constraint [T(x) <: ty]. *) + +Definition type_use (e: typenv) (x: positive) (ty: T.t) : res typenv := + match e.(te_typ)!x with + | None => + let b := B (T.low_bound ty) ty (T.low_bound_sub ty) in + OK {| te_typ := PTree.set x b e.(te_typ); + te_sub := e.(te_sub) |} + | Some(B lo hi s1) => + match T.sub_dec lo ty with + | left s2 => + let hi' := T.glb hi ty in + if T.eq hi hi' then OK e else + let b := B lo hi' (T.glb_max hi ty lo s1 s2) in + OK {| te_typ := PTree.set x b e.(te_typ); + te_sub := e.(te_sub) |} + | right _ => + Error (MSG "bad use of variable " :: POS x :: nil) + end + end. + +Fixpoint type_uses (e: typenv) (rl: list positive) (tyl: list T.t) {struct rl}: res typenv := + match rl, tyl with + | nil, nil => OK e + | r1::rs, ty1::tys => do e1 <- type_use e r1 ty1; type_uses e1 rs tys + | _, _ => Error (msg "arity mismatch") + end. + +(** Add the constraint [T(x) <: T(y)]. + The boolean result is [true] if the types of [r1] and [r2] could be + made more precise. Otherwise, [te_typ] does not change and + [false] is returned. *) + +Definition type_move (e: typenv) (r1 r2: positive) : res (bool * typenv) := + if peq r1 r2 then OK (false, e) else + match e.(te_typ)!r1, e.(te_typ)!r2 with + | None, None => + OK (false, {| te_typ := e.(te_typ); te_sub := (r1, r2) :: e.(te_sub) |}) + | Some(B lo1 hi1 s1), None => + let b2 := B lo1 (T.high_bound lo1) (T.high_bound_sub lo1) in + OK (true, {| te_typ := PTree.set r2 b2 e.(te_typ); + te_sub := if T.sub_dec hi1 lo1 then e.(te_sub) + else (r1, r2) :: e.(te_sub) |}) + | None, Some(B lo2 hi2 s2) => + let b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2) in + OK (true, {| te_typ := PTree.set r1 b1 e.(te_typ); + te_sub := if T.sub_dec hi2 lo2 then e.(te_sub) + else (r1, r2) :: e.(te_sub) |}) + | Some(B lo1 hi1 s1), Some(B lo2 hi2 s2) => + if T.sub_dec hi1 lo2 then + (* The constraint is always true, don't record it *) + OK (false, e) + else match T.sub_dec lo1 hi2 with + | left s => + (* Tighten the bounds on [r1] and [r2] when possible and record + the constraint. *) + let lo2' := T.lub lo1 lo2 in + let hi1' := T.glb hi1 hi2 in + let b1 := B lo1 hi1' (T.glb_max hi1 hi2 lo1 s1 s) in + let b2 := B lo2' hi2 (T.lub_min lo1 lo2 hi2 s s2) in + if T.eq lo2 lo2' then + if T.eq hi1 hi1' then + OK (false, {| te_typ := e.(te_typ); + te_sub := (r1, r2) :: e.(te_sub) |}) + else + OK (true, {| te_typ := PTree.set r1 b1 e.(te_typ); + te_sub := (r1, r2) :: e.(te_sub) |}) + else + if T.eq hi1 hi1' then + OK (true, {| te_typ := PTree.set r2 b2 e.(te_typ); + te_sub := (r1, r2) :: e.(te_sub) |}) + else + OK (true, {| te_typ := PTree.set r2 b2 (PTree.set r1 b1 e.(te_typ)); + te_sub := (r1, r2) :: e.(te_sub) |}) + | right _ => + Error(MSG "ill-typed move from " :: POS r1 :: MSG " to " :: POS r2 :: nil) + end + end. + +(** Solve the remaining subtyping constraints by iteration. *) + +Fixpoint solve_rec (e: typenv) (changed: bool) (q: list constraint) : res (typenv * bool) := + match q with + | nil => + OK (e, changed) + | (r1, r2) :: q' => + do (changed1, e1) <- type_move e r1 r2; solve_rec e1 (changed || changed1) q' + end. + +(** Measuring the state *) + +Definition weight_bounds (ob: option bounds) : nat := + match ob with None => T.max_weight + 1 | Some(B lo hi s) => T.weight hi - T.weight lo end. + +Lemma weight_bounds_1: + forall lo hi s, weight_bounds (Some (B lo hi s)) < weight_bounds None. +Proof. + intros; simpl. generalize (T.weight_range hi); omega. +Qed. + +Lemma weight_bounds_2: + forall lo1 hi1 s1 lo2 hi2 s2, + T.sub lo2 lo1 -> T.sub hi1 hi2 -> lo1 <> lo2 \/ hi1 <> hi2 -> + weight_bounds (Some (B lo1 hi1 s1)) < weight_bounds (Some (B lo2 hi2 s2)). +Proof. + intros; simpl. + generalize (T.weight_sub _ _ s1) (T.weight_sub _ _ s2) (T.weight_sub _ _ H) (T.weight_sub _ _ H0); intros. + destruct H1. + assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). omega. + assert (T.weight hi1 < T.weight hi2) by (apply T.weight_sub_strict; auto). omega. +Qed. + +Hint Resolve T.sub_refl: ty. + +Lemma weight_type_move: + forall e r1 r2 changed e', + type_move e r1 r2 = OK(changed, e') -> + (e'.(te_sub) = e.(te_sub) \/ e'.(te_sub) = (r1, r2) :: e.(te_sub)) + /\ (forall r, weight_bounds e'.(te_typ)!r <= weight_bounds e.(te_typ)!r) + /\ (changed = true -> + weight_bounds e'.(te_typ)!r1 + weight_bounds e'.(te_typ)!r2 + < weight_bounds e.(te_typ)!r1 + weight_bounds e.(te_typ)!r2). +Proof. + unfold type_move; intros. + destruct (peq r1 r2). + inv H. split; auto. split; intros. omega. discriminate. + destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; + destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. +- destruct (T.sub_dec hi1 lo2). + inv H. split; auto. split; intros. omega. discriminate. + destruct (T.sub_dec lo1 hi2); try discriminate. + set (lo2' := T.lub lo1 lo2) in *. + set (hi1' := T.glb hi1 hi2) in *. + assert (S1': T.sub hi1' hi1) by (eapply T.glb_left; eauto). + assert (S2': T.sub lo2 lo2') by (eapply T.lub_right; eauto). + set (b1 := B lo1 hi1' (T.glb_max hi1 hi2 lo1 s1 s)) in *. + set (b2 := B lo2' hi2 (T.lub_min lo1 lo2 hi2 s s2)) in *. +Local Opaque weight_bounds. + destruct (T.eq lo2 lo2'); destruct (T.eq hi1 hi1'); inversion H; clear H; subst changed e'; simpl. ++ split; auto. split; intros. omega. discriminate. ++ assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1))) + by (apply weight_bounds_2; auto with ty). + split; auto. split; intros. + rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. omega. omega. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. ++ assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2))) + by (apply weight_bounds_2; auto with ty). + split; auto. split; intros. + rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. omega. omega. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. ++ assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1))) + by (apply weight_bounds_2; auto with ty). + assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2))) + by (apply weight_bounds_2; auto with ty). + split; auto. split; intros. + rewrite ! PTree.gsspec. + destruct (peq r r2). subst r. rewrite E2. omega. + destruct (peq r r1). subst r. rewrite E1. omega. + omega. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. omega. + +- set (b2 := B lo1 (T.high_bound lo1) (T.high_bound_sub lo1)) in *. + assert (weight_bounds (Some b2) < weight_bounds None) by (apply weight_bounds_1). + inv H; simpl. + split. destruct (T.sub_dec hi1 lo1); auto. + split; intros. + rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; omega. omega. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. + +- set (b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2)) in *. + assert (weight_bounds (Some b1) < weight_bounds None) by (apply weight_bounds_1). + inv H; simpl. + split. destruct (T.sub_dec hi2 lo2); auto. + split; intros. + rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; omega. omega. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. + +- inv H. split; auto. simpl; split; intros. omega. congruence. +Qed. + +Definition weight_constraints (b: PTree.t bounds) (cstr: list constraint) : nat := + List.fold_right (fun xy n => n + weight_bounds b!(fst xy) + weight_bounds b!(snd xy)) 0 cstr. + +Remark weight_constraints_tighter: + forall b1 b2, (forall r, weight_bounds b1!r <= weight_bounds b2!r) -> + forall q, weight_constraints b1 q <= weight_constraints b2 q. +Proof. + induction q; simpl. omega. generalize (H (fst a)) (H (snd a)); omega. +Qed. + +Lemma weight_solve_rec: + forall q e changed e' changed', + solve_rec e changed q = OK(e', changed') -> + (forall r, weight_bounds e'.(te_typ)!r <= weight_bounds e.(te_typ)!r) /\ + weight_constraints e'.(te_typ) e'.(te_sub) + (if changed' && negb changed then 1 else 0) + <= weight_constraints e.(te_typ) e.(te_sub) + weight_constraints e.(te_typ) q. +Proof. + induction q; simpl; intros. +- inv H. split. intros; omega. replace (changed' && negb changed') with false. + omega. destruct changed'; auto. +- destruct a as [r1 r2]; monadInv H; simpl. + rename x into changed1. rename x0 into e1. + exploit weight_type_move; eauto. intros [A [B C]]. + exploit IHq; eauto. intros [D E]. + split. intros. eapply le_trans. eapply D. eapply B. + assert (P: weight_constraints (te_typ e1) (te_sub e) <= + weight_constraints (te_typ e) (te_sub e)) + by (apply weight_constraints_tighter; auto). + assert (Q: weight_constraints (te_typ e1) (te_sub e1) <= + weight_constraints (te_typ e1) (te_sub e) + + weight_bounds (te_typ e1)!r1 + weight_bounds (te_typ e1)!r2). + { destruct A as [Q|Q]; rewrite Q. omega. simpl. omega. } + assert (R: weight_constraints (te_typ e1) q <= weight_constraints (te_typ e) q) + by (apply weight_constraints_tighter; auto). + set (ch1 := if changed' && negb (changed || changed1) then 1 else 0) in *. + set (ch2 := if changed' && negb changed then 1 else 0) in *. + destruct changed1. + assert (ch2 <= ch1 + 1). + { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r. + destruct (changed' && negb changed); omega. } + exploit C; eauto. omega. + assert (ch2 <= ch1). + { unfold ch2, ch1. rewrite orb_false_r. omega. } + generalize (B r1) (B r2); omega. +Qed. + +Definition weight_typenv (e: typenv) : nat := + weight_constraints e.(te_typ) e.(te_sub). + +(** Iterative solving of the remaining constraints *) + +Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv := + match solve_rec {| te_typ := e.(te_typ); te_sub := nil |} false e.(te_sub) with + | OK(e', false) => OK e (**r no more changes, fixpoint reached *) + | OK(e', true) => solve_constraints e' (**r one more iteration *) + | Error msg => Error msg + end. +Proof. + intros. exploit weight_solve_rec; eauto. simpl. intros [A B]. + unfold weight_typenv. omega. +Qed. + +Definition typassign := positive -> T.t. + +Definition makeassign (e: typenv) : typassign := + fun x => match e.(te_typ)!x with Some(B lo hi s) => lo | None => T.default end. + +Definition solve (e: typenv) : res typassign := + do e' <- solve_constraints e; OK(makeassign e'). + +(** What it means to be a solution *) + +Definition satisf (te: typassign) (e: typenv) : Prop := + (forall x lo hi s, e.(te_typ)!x = Some(B lo hi s) -> T.sub lo (te x) /\ T.sub (te x) hi) +/\ (forall x y, In (x, y) e.(te_sub) -> T.sub (te x) (te y)). + +Lemma satisf_initial: forall te, satisf te initial. +Proof. + unfold initial; intros; split; simpl; intros. + rewrite PTree.gempty in H; discriminate. + contradiction. +Qed. + +(** Soundness proof *) + +Lemma type_def_incr: + forall te x ty e e', type_def e x ty = OK e' -> satisf te e' -> satisf te e. +Proof. + unfold type_def; intros. destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. +- destruct (T.sub_dec ty hi); try discriminate. + destruct (T.eq lo (T.lub lo ty)); monadInv H. + subst e'; auto. + destruct H0 as [P Q]; split; auto; intros. + destruct (peq x x0). + + subst x0. rewrite E in H; inv H. + exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. + apply T.sub_trans with (T.lub lo0 ty); auto. eapply T.lub_left; eauto. + + eapply P; simpl. rewrite PTree.gso; eauto. +- inv H. destruct H0 as [P Q]; split; auto; intros. + eapply P; simpl. rewrite PTree.gso; eauto. congruence. +Qed. + +Hint Resolve type_def_incr: ty. + +Lemma type_def_sound: + forall te x ty e e', type_def e x ty = OK e' -> satisf te e' -> T.sub ty (te x). +Proof. + unfold type_def; intros. destruct H0 as [P Q]. + destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. +- destruct (T.sub_dec ty hi); try discriminate. + destruct (T.eq lo (T.lub lo ty)); monadInv H. + + subst e'. apply T.sub_trans with lo. + rewrite e0. eapply T.lub_right; eauto. eapply P; eauto. + + apply T.sub_trans with (T.lub lo ty). + eapply T.lub_right; eauto. + eapply (P x). simpl. rewrite PTree.gss; eauto. +- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. +Qed. + +Lemma type_defs_incr: + forall te xl tyl e e', type_defs e xl tyl = OK e' -> satisf te e' -> satisf te e. +Proof. + induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty. +Qed. + +Hint Resolve type_defs_incr: ty. + +Lemma type_defs_sound: + forall te xl tyl e e', type_defs e xl tyl = OK e' -> satisf te e' -> list_forall2 T.sub tyl (map te xl). +Proof. + induction xl; destruct tyl; simpl; intros; monadInv H. + constructor. + constructor; eauto. eapply type_def_sound; eauto with ty. +Qed. + +Lemma type_use_incr: + forall te x ty e e', type_use e x ty = OK e' -> satisf te e' -> satisf te e. +Proof. + unfold type_use; intros. destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. +- destruct (T.sub_dec lo ty); try discriminate. + destruct (T.eq hi (T.glb hi ty)); monadInv H. + subst e'; auto. + destruct H0 as [P Q]; split; auto; intros. + destruct (peq x x0). + + subst x0. rewrite E in H; inv H. + exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. + apply T.sub_trans with (T.glb hi0 ty); auto. eapply T.glb_left; eauto. + + eapply P; simpl. rewrite PTree.gso; eauto. +- inv H. destruct H0 as [P Q]; split; auto; intros. + eapply P; simpl. rewrite PTree.gso; eauto. congruence. +Qed. + +Hint Resolve type_use_incr: ty. + +Lemma type_use_sound: + forall te x ty e e', type_use e x ty = OK e' -> satisf te e' -> T.sub (te x) ty. +Proof. + unfold type_use; intros. destruct H0 as [P Q]. + destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. +- destruct (T.sub_dec lo ty); try discriminate. + destruct (T.eq hi (T.glb hi ty)); monadInv H. + + subst e'. apply T.sub_trans with hi. + eapply P; eauto. rewrite e0. eapply T.glb_right; eauto. + + apply T.sub_trans with (T.glb hi ty). + eapply (P x). simpl. rewrite PTree.gss; eauto. + eapply T.glb_right; eauto. +- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. +Qed. + +Lemma type_uses_incr: + forall te xl tyl e e', type_uses e xl tyl = OK e' -> satisf te e' -> satisf te e. +Proof. + induction xl; destruct tyl; simpl; intros; monadInv H; eauto with ty. +Qed. + +Hint Resolve type_uses_incr: ty. + +Lemma type_uses_sound: + forall te xl tyl e e', type_uses e xl tyl = OK e' -> satisf te e' -> list_forall2 T.sub (map te xl) tyl. +Proof. + induction xl; destruct tyl; simpl; intros; monadInv H. + constructor. + constructor; eauto. eapply type_use_sound; eauto with ty. +Qed. + +Lemma type_move_incr: + forall te e r1 r2 e' changed, + type_move e r1 r2 = OK(changed, e') -> satisf te e' -> satisf te e. +Proof. + unfold type_move; intros. destruct H0 as [P Q]. + destruct (peq r1 r2). inv H; split; auto. + destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; + destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. +- destruct (T.sub_dec hi1 lo2). inv H; split; auto. + destruct (T.sub_dec lo1 hi2); try discriminate. + set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *. + destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); monadInv H; simpl in *. + + subst e'; simpl in *. split; auto. + + subst e'; simpl in *. split; auto. intros. destruct (peq x r1). + subst x. + rewrite E1 in H. injection H; intros; subst lo0 hi0. + exploit (P r1). rewrite PTree.gss; eauto. intuition. + apply T.sub_trans with (T.glb hi1 hi2); auto. eapply T.glb_left; eauto. + eapply P. rewrite PTree.gso; eauto. + + subst e'; simpl in *. split; auto. intros. destruct (peq x r2). + subst x. + rewrite E2 in H. injection H; intros; subst lo0 hi0. + exploit (P r2). rewrite PTree.gss; eauto. intuition. + apply T.sub_trans with (T.lub lo1 lo2); auto. eapply T.lub_right; eauto. + eapply P. rewrite PTree.gso; eauto. + + split; auto. intros. + destruct (peq x r1). subst x. + rewrite E1 in H. injection H; intros; subst lo0 hi0. + exploit (P r1). rewrite PTree.gso; eauto. rewrite PTree.gss; eauto. intuition. + apply T.sub_trans with (T.glb hi1 hi2); auto. eapply T.glb_left; eauto. + destruct (peq x r2). subst x. + rewrite E2 in H. injection H; intros; subst lo0 hi0. + exploit (P r2). rewrite PTree.gss; eauto. intuition. + apply T.sub_trans with (T.lub lo1 lo2); auto. eapply T.lub_right; eauto. + eapply P. rewrite ! PTree.gso; eauto. +- inv H; simpl in *. split; intros. + eapply P. rewrite PTree.gso; eauto. congruence. + apply Q. destruct (T.sub_dec hi1 lo1); auto with coqlib. +- inv H; simpl in *. split; intros. + eapply P. rewrite PTree.gso; eauto. congruence. + apply Q. destruct (T.sub_dec hi2 lo2); auto with coqlib. +- inv H; simpl in *. split; auto. +Qed. + +Hint Resolve type_move_incr: ty. + +Lemma type_move_sound: + forall te e r1 r2 e' changed, + type_move e r1 r2 = OK(changed, e') -> satisf te e' -> T.sub (te r1) (te r2). +Proof. + unfold type_move; intros. destruct H0 as [P Q]. + destruct (peq r1 r2). subst r2. apply T.sub_refl. + destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; + destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. +- destruct (T.sub_dec hi1 lo2). + inv H. apply T.sub_trans with hi1. eapply P; eauto. apply T.sub_trans with lo2; auto. eapply P; eauto. + destruct (T.sub_dec lo1 hi2); try discriminate. + set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *. + destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); monadInv H; simpl in *. + + subst e'; simpl in *. apply Q; auto. + + subst e'; simpl in *. apply Q; auto. + + subst e'; simpl in *. apply Q; auto. + + apply Q; auto. +- inv H; simpl in *. destruct (T.sub_dec hi1 lo1). + + apply T.sub_trans with hi1. eapply P; eauto. rewrite PTree.gso; eauto. + apply T.sub_trans with lo1; auto. eapply P. rewrite PTree.gss; eauto. + + auto with coqlib. +- inv H; simpl in *. destruct (T.sub_dec hi2 lo2). + + apply T.sub_trans with hi2. eapply P. rewrite PTree.gss; eauto. + apply T.sub_trans with lo2; auto. eapply P. rewrite PTree.gso; eauto. + + auto with coqlib. +- inv H. simpl in Q; auto. +Qed. + +Lemma solve_rec_incr: + forall te q e changed e' changed', + solve_rec e changed q = OK(e', changed') -> satisf te e' -> satisf te e. +Proof. + induction q; simpl; intros. +- inv H. auto. +- destruct a as [r1 r2]; monadInv H. eauto with ty. +Qed. + +Lemma solve_rec_sound: + forall te r1 r2 q e changed e' changed', + solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' -> + T.sub (te r1) (te r2). +Proof. + induction q; simpl; intros. +- contradiction. +- destruct a as [r3 r4]; monadInv H. destruct H0. + + inv H. eapply type_move_sound; eauto. eapply solve_rec_incr; eauto. + + eapply IHq; eauto with ty. +Qed. + +Lemma type_move_false: + forall e r1 r2 e', + type_move e r1 r2 = OK(false, e') -> + te_typ e' = te_typ e /\ T.sub (makeassign e r1) (makeassign e r2). +Proof. + unfold type_move; intros. + destruct (peq r1 r2). inv H. split; auto. apply T.sub_refl. + unfold makeassign; + destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; + destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. +- destruct (T.sub_dec hi1 lo2). + inv H. split; auto. eapply T.sub_trans; eauto. + destruct (T.sub_dec lo1 hi2); try discriminate. + set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *. + destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); try discriminate. + monadInv H. split; auto. rewrite e0. unfold lo. eapply T.lub_left; eauto. +- discriminate. +- discriminate. +- inv H. split; auto. apply T.sub_refl. +Qed. + +Lemma solve_rec_false: + forall r1 r2 q e changed e', + solve_rec e changed q = OK(e', false) -> + changed = false /\ + (In (r1, r2) q -> T.sub (makeassign e r1) (makeassign e r2)). +Proof. + induction q; simpl; intros. +- inv H. tauto. +- destruct a as [r3 r4]; monadInv H. + exploit IHq; eauto. intros [P Q]. + destruct changed; try discriminate. destruct x; try discriminate. + exploit type_move_false; eauto. intros [U V]. + split. auto. intros [A|A]. inv A. auto. exploit Q; auto. + unfold makeassign; rewrite U; auto. +Qed. + +Lemma solve_constraints_incr: + forall te e e', solve_constraints e = OK e' -> satisf te e' -> satisf te e. +Proof. + intros te e; functional induction (solve_constraints e); intros. +- inv H. auto. +- exploit solve_rec_incr; eauto. intros [A B]. + split; auto. intros; eapply solve_rec_sound; eauto. +- discriminate. +Qed. + +Lemma solve_constraints_sound: + forall e e', solve_constraints e = OK e' -> satisf (makeassign e') e'. +Proof. + intros e0; functional induction (solve_constraints e0); intros. +- inv H. split; intros. + unfold makeassign; rewrite H. split; auto with ty. + exploit solve_rec_false. eauto. intros [A B]. eapply B; eauto. +- eauto. +- discriminate. +Qed. + +Theorem solve_sound: + forall e te, solve e = OK te -> satisf te e. +Proof. + unfold solve; intros. monadInv H. + eapply solve_constraints_incr. eauto. eapply solve_constraints_sound; eauto. +Qed. + +(** Completeness proof *) + +Lemma type_def_complete: + forall te e x ty, + satisf te e -> T.sub ty (te x) -> exists e', type_def e x ty = OK e' /\ satisf te e'. +Proof. + unfold type_def; intros. destruct H as [P Q]. + destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. +- destruct (T.sub_dec ty hi). + destruct (T.eq lo (T.lub lo ty)). + exists e; split; auto. split; auto. + econstructor; split; eauto. split; simpl; auto; intros. + rewrite PTree.gsspec in H. destruct (peq x0 x). + inv H. exploit P; eauto. intuition. eapply T.lub_min; eauto. + eapply P; eauto. + elim n. apply T.sub_trans with (te x); auto. eapply P; eauto. +- econstructor; split; eauto. split; simpl; auto; intros. + rewrite PTree.gsspec in H. destruct (peq x0 x). + inv H. split; auto. apply T.high_bound_majorant; auto. + eapply P; eauto. +Qed. + +Lemma type_defs_complete: + forall te xl tyl e, + satisf te e -> list_forall2 T.sub tyl (map te xl) -> + exists e', type_defs e xl tyl = OK e' /\ satisf te e'. +Proof. + induction xl; intros; inv H0; simpl. + econstructor; eauto. + exploit (type_def_complete te e a a1); auto. intros (e1 & P & Q). + exploit (IHxl al e1); auto. intros (e2 & U & V). + exists e2; split; auto. rewrite P; auto. +Qed. + +Lemma type_use_complete: + forall te e x ty, + satisf te e -> T.sub (te x) ty -> exists e', type_use e x ty = OK e' /\ satisf te e'. +Proof. + unfold type_use; intros. destruct H as [P Q]. + destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. +- destruct (T.sub_dec lo ty). + destruct (T.eq hi (T.glb hi ty)). + exists e; split; auto. split; auto. + econstructor; split; eauto. split; simpl; auto; intros. + rewrite PTree.gsspec in H. destruct (peq x0 x). + inv H. exploit P; eauto. intuition. eapply T.glb_max; eauto. + eapply P; eauto. + elim n. apply T.sub_trans with (te x); auto. eapply P; eauto. +- econstructor; split; eauto. split; simpl; auto; intros. + rewrite PTree.gsspec in H. destruct (peq x0 x). + inv H. split; auto. apply T.low_bound_minorant; auto. + eapply P; eauto. +Qed. + +Lemma type_uses_complete: + forall te xl tyl e, + satisf te e -> list_forall2 T.sub (map te xl) tyl -> + exists e', type_uses e xl tyl = OK e' /\ satisf te e'. +Proof. + induction xl; intros; inv H0; simpl. + econstructor; eauto. + exploit (type_use_complete te e a b1); auto. intros (e1 & P & Q). + exploit (IHxl bl e1); auto. intros (e2 & U & V). + exists e2; split; auto. rewrite P; auto. +Qed. + +Lemma type_move_complete: + forall te e r1 r2, + satisf te e -> T.sub (te r1) (te r2) -> + exists changed e', type_move e r1 r2 = OK(changed, e') /\ satisf te e'. +Proof. + unfold type_move; intros. elim H; intros P Q. + assert (Q': forall x y, In (x, y) ((r1, r2) :: te_sub e) -> T.sub (te x) (te y)). + { intros. destruct H1; auto. congruence. } + destruct (peq r1 r2). econstructor; econstructor; eauto. + destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; + destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. +- exploit (P r1); eauto. intros [L1 U1]. + exploit (P r2); eauto. intros [L2 U2]. + destruct (T.sub_dec hi1 lo2). econstructor; econstructor; eauto. + destruct (T.sub_dec lo1 hi2). + destruct (T.eq lo2 (T.lub lo1 lo2)); destruct (T.eq hi1 (T.glb hi1 hi2)); + econstructor; econstructor; split; eauto; split; auto; simpl; intros. + + rewrite PTree.gsspec in H1. destruct (peq x r1). + clear e0. inv H1. split; auto. + apply T.glb_max. auto. apply T.sub_trans with (te r2); auto. + eapply P; eauto. + + rewrite PTree.gsspec in H1. destruct (peq x r2). + clear e0. inv H1. split; auto. + apply T.lub_min. apply T.sub_trans with (te r1); auto. auto. + eapply P; eauto. + + rewrite ! PTree.gsspec in H1. destruct (peq x r2). + inv H1. split; auto. apply T.lub_min; auto. apply T.sub_trans with (te r1); auto. + destruct (peq x r1). + inv H1. split; auto. apply T.glb_max; auto. apply T.sub_trans with (te r2); auto. + eapply P; eauto. + + elim n1. apply T.sub_trans with (te r1); auto. + apply T.sub_trans with (te r2); auto. +- econstructor; econstructor; split; eauto; split. + + simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x r2). + inv H1. exploit P; eauto. intuition. + apply T.sub_trans with (te r1); auto. + apply T.high_bound_majorant. apply T.sub_trans with (te r1); auto. + eapply P; eauto. + + destruct (T.sub_dec hi1 lo1); auto. +- econstructor; econstructor; split; eauto; split. + + simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x r1). + inv H1. exploit P; eauto. intuition. + apply T.low_bound_minorant. apply T.sub_trans with (te r2); auto. + apply T.sub_trans with (te r2); auto. + eapply P; eauto. + + destruct (T.sub_dec hi2 lo2); auto. +- econstructor; econstructor; split; eauto; split; auto. +Qed. + +Lemma solve_rec_complete: + forall te q e changed, + satisf te e -> + (forall r1 r2, In (r1, r2) q -> T.sub (te r1) (te r2)) -> + exists e' changed', solve_rec e changed q = OK(e', changed') /\ satisf te e'. +Proof. + induction q; simpl; intros. +- econstructor; econstructor; eauto. +- destruct a as [r1 r2]. + exploit (type_move_complete te e r1 r2); auto. intros (changed1 & e1 & A & B). + exploit (IHq e1 (changed || changed1)); auto. intros (e' & changed' & C & D). + exists e'; exists changed'. rewrite A; simpl; rewrite C; auto. +Qed. + +Lemma solve_constraints_complete: + forall te e, satisf te e -> exists e', solve_constraints e = OK e' /\ satisf te e'. +Proof. + intros te e. functional induction (solve_constraints e); intros. +- exists e; auto. +- exploit (solve_rec_complete te (te_sub e) {| te_typ := te_typ e; te_sub := nil |} false). + destruct H; split; auto. simpl; tauto. + destruct H; auto. + intros (e1 & changed1 & P & Q). + apply IHr. congruence. +- exploit (solve_rec_complete te (te_sub e) {| te_typ := te_typ e; te_sub := nil |} false). + destruct H; split; auto. simpl; tauto. + destruct H; auto. + intros (e1 & changed1 & P & Q). + congruence. +Qed. + +Lemma solve_complete: + forall te e, satisf te e -> exists te', solve e = OK te'. +Proof. + intros. unfold solve. + destruct (solve_constraints_complete te e H) as (e' & P & Q). + econstructor. rewrite P. simpl. eauto. +Qed. + +End SubSolver. + diff --git a/common/Values.v b/common/Values.v index 76fb230..bb97cdc 100644 --- a/common/Values.v +++ b/common/Values.v @@ -61,6 +61,7 @@ Definition has_type (v: val) (t: typ) : Prop := | Vint _, Tint => True | Vlong _, Tlong => True | Vfloat _, Tfloat => True + | Vfloat f, Tsingle => Float.is_single f | Vptr _ _, Tint => True | _, _ => False end. @@ -78,6 +79,23 @@ Definition has_opttype (v: val) (ot: option typ) : Prop := | Some t => has_type v t end. +Lemma has_subtype: + forall ty1 ty2 v, + subtype ty1 ty2 = true -> has_type v ty1 -> has_type v ty2. +Proof. + intros. destruct ty1; destruct ty2; simpl in H; discriminate || assumption || idtac. + unfold has_type in *. destruct v; auto. +Qed. + +Lemma has_subtype_list: + forall tyl1 tyl2 vl, + subtype_list tyl1 tyl2 = true -> has_type_list vl tyl1 -> has_type_list vl tyl2. +Proof. + induction tyl1; intros; destruct tyl2; try discriminate; destruct vl; try contradiction. + red; auto. + simpl in *. InvBooleans. destruct H0. split; auto. eapply has_subtype; eauto. +Qed. + (** Truth values. Pointers and non-zero integers are treated as [True]. The integer 0 (also used to represent the null pointer) is [False]. [Vundef] and floats are neither true nor false. *) @@ -603,14 +621,14 @@ Definition cmplu (c: comparison) (v1 v2: val): option val := End COMPARISONS. -(** [load_result] is used in the memory model (library [Mem]) - to post-process the results of a memory read. For instance, - consider storing the integer value [0xFFF] on 1 byte at a - given address, and reading it back. If it is read back with +(** [load_result] reflects the effect of storing a value with a given + memory chunk, then reading it back with the same chunk. Depending + on the chunk and the type of the value, some normalization occurs. + For instance, consider storing the integer value [0xFFF] on 1 byte + at a given address, and reading it back. If it is read back with chunk [Mint8unsigned], zero-extension must be performed, resulting - in [0xFF]. If it is read back as a [Mint8signed], sign-extension - is performed and [0xFFFFFFFF] is returned. Type mismatches - (e.g. reading back a float as a [Mint32]) read back as [Vundef]. *) + in [0xFF]. If it is read back as a [Mint8signed], sign-extension is + performed and [0xFFFFFFFF] is returned. *) Definition load_result (chunk: memory_chunk) (v: val) := match chunk, v with @@ -626,6 +644,19 @@ Definition load_result (chunk: memory_chunk) (v: val) := | _, _ => Vundef end. +Lemma load_result_type: + forall chunk v, has_type (load_result chunk v) (type_of_chunk chunk). +Proof. + intros. destruct chunk; destruct v; simpl; auto. apply Float.singleoffloat_is_single. +Qed. + +Lemma load_result_same: + forall v ty, has_type v ty -> load_result (chunk_of_type ty) v = v. +Proof. + unfold has_type; intros. destruct v; destruct ty; try contradiction; auto. + simpl. rewrite Float.singleoffloat_of_single; auto. +Qed. + (** Theorems on arithmetic operations. *) Theorem cast8unsigned_and: -- cgit v1.2.3