diff options
| -rw-r--r-- | driver/Ctydescr.ml | 456 | ||||
| -rw-r--r-- | powerpc/Archi.v | 15 | ||||
| -rw-r--r-- | powerpc/Asm.v | 58 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 22 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 83 | ||||
| -rw-r--r-- | powerpc/Asmgenproof1.v | 125 | ||||
| -rw-r--r-- | powerpc/ConstpropOp.vp | 38 | ||||
| -rw-r--r-- | powerpc/ConstpropOpproof.v | 133 | ||||
| -rw-r--r-- | powerpc/Conventions1.v | 26 | ||||
| -rw-r--r-- | powerpc/NeedOp.v | 6 | ||||
| -rw-r--r-- | powerpc/Op.v | 163 | ||||
| -rw-r--r-- | powerpc/SelectLong.vp | 21 | ||||
| -rw-r--r-- | powerpc/SelectLongproof.v | 22 | ||||
| -rw-r--r-- | powerpc/SelectOp.vp | 20 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 34 | ||||
| -rw-r--r-- | powerpc/ValueAOp.v | 8 |
16 files changed, 478 insertions, 752 deletions
diff --git a/driver/Ctydescr.ml b/driver/Ctydescr.ml deleted file mode 100644 index 8091257b..00000000 --- a/driver/Ctydescr.ml +++ /dev/null @@ -1,456 +0,0 @@ -open Printf -open Camlcoq -open Tydesc - -let check ty x = TyIO.check x ty; true - -(* From stdlib *) - -let list t = List t -let pair t1 t2 = Tuple [t1;t2] - -let rec repr_nat = Sum("nat", [ - "O", []; - "S", [repr_nat] -]) - -let nat = Base { - base_name = "nat"; - base_check = check repr_nat; - base_parse = (fun synt s -> assert false); - base_print = (fun synt x -> - let s = string_of_int (Nat.to_int x) in - match synt with - | `Coq -> s ^ "%nat" - | _ -> s) -} - -let rec repr_positive = Sum("positive", [ - "xI", [repr_positive]; - "xO", [repr_positive]; - "xH", [] -]) - -let positive = Base { - base_name = "positive"; - base_check = check repr_positive; - base_parse = (fun synt s -> assert false); - base_print = (fun synt x -> Z.to_string (Z.Zpos x)) -} - -let repr_N = Sum("N", [ - "N0", []; - "Npos", [repr_positive] -]) - -let _N = Base { - base_name = "N"; - base_check = check repr_N; - base_parse = (fun synt s -> assert false); - base_print = (fun synt x -> - let y = match x with N.N0 -> Z.Z0 | N.Npos p -> Z.Zpos p in - let s = Z.to_string y in - match synt with - | `Coq -> s ^ "%N" - | _ -> s) -} - -let repr_Z = Sum("Z", [ - "Z0", []; - "Zpos", [repr_positive]; - "Zneg", [repr_positive] -]) - -let _Z = Base { - base_name = "Z"; - base_check = check repr_Z; - base_parse = (fun synt s -> assert false); - base_print = (fun synt x -> - let s = Z.to_string x in - match synt with - | `Coq -> s ^ "%Z" - | _ -> s) -} - -(* From Integers *) - -let int = Base { - base_name = "int"; - base_check = check repr_Z; - base_parse = (fun synt s -> - let (n, s') = get_number s in - try (coqint_of_camlint (Int32.of_string n), s') - with Failure _ -> - raise (Parsing_failure(get_position s, sprintf "bad 'int' literal %S" n))); - base_print = (fun synt x -> - let s = Z.to_string x in - match synt with - | `Coq -> "(mkint " ^ s ^ "%Z)" - | _ -> s) -} - -let int64 = Base { - base_name = "int64"; - base_check = check repr_Z; - base_parse = (fun synt s -> - let (n, s') = get_number s in - try (coqint_of_camlint64 (Int64.of_string n), s') - with Failure _ -> - raise (Parsing_failure(get_position s, sprintf "bad 'int64' literal %S" n))); - base_print = (fun synt x -> - let s = Z.to_string x in - match synt with - | `Coq -> "(mkint64 " ^ s ^ "%Z)" - | _ -> s) -} - -(* From Floats *) - -let nan_pl = positive - -let binary_float = Sum("binary_float", [ - "B754_zero", [bool]; - "B754_infinity", [bool]; - "B754_nan", [bool; nan_pl]; - "B754_finite", [bool; positive; _Z] -]) - -let float = Base { - base_name = "float"; - base_check = check binary_float; - base_parse = (fun synt s -> - let (n, s') = get_number s in - try (Floats.Float.of_bits (coqint_of_camlint64 (Int64.of_string n)), s') - with Failure _ -> - raise (Parsing_failure(get_position s, sprintf "bad 'float' literal %S" n))); - base_print = (fun synt x -> - let s = Z.to_string (Floats.Float.to_bits x) in - match synt with - | `Coq -> "(mkfloat " ^ s ^ "%Z)" - | _ -> s) -} - -let float32 = Base { - base_name = "float32"; - base_check = check binary_float; - base_parse = (fun synt s -> - let (n, s') = get_number s in - try (Floats.Float32.of_bits (coqint_of_camlint (Int32.of_string n)), s') - with Failure _ -> - raise (Parsing_failure(get_position s, sprintf "bad 'float32' literal %S" n))); - base_print = (fun synt x -> - let s = Z.to_string (Floats.Float.to_bits x) in - match synt with - | `Coq -> "(mkfloat32 " ^ s ^ "%Z)" - | _ -> s) -} - -(* From Maps *) - -let ptree a = - let rec t = Sum(sprintf "PTree.t[%s]" (describe_ty a), [ - "Leaf", []; - "Node", [t; option a; t] - ]) in t - -(* From AST *) - -let ident = positive - -let typ = Sum("typ", [ - "AST.Tint", []; - "AST.Tfloat", []; - "AST.Tlong", []; - "AST.Tsingle", []; - "AST.Tany32", []; - "AST.Tany64", []; -]) - -let calling_convention = Record("calling_convention", [ - "cc_vararg", bool; - "cc_structret", bool; -]) - -let default_calling_convention = { - dfl_val = AST.cc_default; - dfl_print = (function `Coq -> Some "cc_default" | _ -> None) -} - -let calling_convention_d = - Default(calling_convention, default_calling_convention) - -let signature = Record("signature", [ - "sig_args", list typ; - "sig_res", option typ; - "sig_cc", calling_convention_d; -]) - -let memory_chunk = Sum("memory_chunk", [ - "Mint8signed", []; - "Mint8unsigned", []; - "Mint16signed", []; - "Mint16unsigned", []; - "Mint32", []; - "Mint64", []; - "Mfloat32", []; - "Mfloat64", []; - "Many32", []; - "Many64", []; -]) - -let init_data = Sum("init_data", [ - "Init_int8", [int]; - "Init_int16", [int]; - "Init_int32", [int]; - "Init_int64", [int64]; - "Init_float32", [float32]; - "Init_float64", [float]; - "Init_space", [_Z]; - "Init_addrof", [ident; int]; -]) - -let globvar v = Record(sprintf "globvar[%s]" (describe_ty v), [ - "gvar_info", v; - "gvar_init", list init_data; - "gvar_readonly", bool; - "gvar_volatile", bool; -]) - -let globdef f v = Sum(sprintf "globdef[%s][%s]" (describe_ty f) (describe_ty v), [ - "Gfun", [f]; - "Gvar", [globvar v]; -]) - -let external_function = Sum("external_function", [ - "EF_external", [ident; signature]; - "EF_builtin", [ident; signature]; - "EF_vload", [memory_chunk]; - "EF_vstore", [memory_chunk]; - "EF_vload_global", [memory_chunk; ident; int]; - "EF_vstore_global", [memory_chunk; ident; int]; - "EF_malloc", []; - "EF_free", []; - "EF_memcpy", [_Z; _Z]; - "EF_annot", [ident; list typ]; - "EF_annot_val", [ident; typ]; - "EF_inline_asm", [ident; signature; list string]; -]) - -(* From Values *) - -let block = positive - -let val_ = Sum("val", [ - "Vundef", []; - "Vint", [int]; - "Vlong", [int64]; - "Vfloat", [float]; - "Vsingle", [float32]; - "Vptr", [block; int]; -]) - -(* From Ctypes *) - -let signedness = Sum("signedness", [ - "Signed", []; - "Unsigned", []; -]) - -let intsize = Sum("intsize", [ - "I8", []; - "I16", []; - "I32", []; - "IBool", []; -]) - -let floatsize = Sum("floatsize", [ - "F32", []; - "F64", []; -]) - -let attr = Record("attr", [ - "attr_volatile", bool; - "attr_alignas", option _N; -]) - -let attr_default = { - dfl_val = Ctypes.noattr; - dfl_print = (function `Coq -> Some "noattr" | _ -> None) -} - -let attr_d = Default(attr, attr_default) - -let rec type_ = Sum("type", [ - "Tvoid", []; - "Tint", [intsize; signedness; attr_d]; - "Tlong", [signedness; attr_d]; - "Tfloat", [floatsize; attr_d]; - "Tpointer", [type_; attr_d]; - "Tarray", [type_; _Z; attr_d]; - "Tfunction", [typelist; type_; calling_convention_d]; - "Tstruct", [ident; attr_d]; - "Tunion", [ident; attr_d]; -]) -and typelist = Sum("typelist", [ - "Tnil", []; - "Tcons", [type_; typelist]; -]) - -let struct_or_union = Sum("struct_or_union", [ - "Struct", []; - "Union", []; -]) - -let members = list (pair ident type_) - -let composite_definition = Sum("composite_definition", [ - "Composite", [ident; struct_or_union; members; attr_d]; -]) - -let composite = Record("composite",[ - "co_su", struct_or_union; - "co_members", members; - "co_attr", attr; - "co_sizeof", _Z; - "co_alignof", _Z; - "co_rank", nat -]) - -let composite_env = ptree composite - -(* From Cop *) - -let unary_operation = Sum("unary_operation", [ - "Onotbool", []; - "Onotint", []; - "Oneg", []; - "Oabsfloat", []; -]) - -let binary_operation = Sum("binary_operation", [ - "Oadd", []; - "Osub", []; - "Omul", []; - "Odiv", []; - "Omod", []; - "Oand", []; - "Oor", []; - "Oxor", []; - "Oshl", []; - "Oshr", []; - "Oeq", []; - "One", []; - "Olt", []; - "Ogt", []; - "Ole", []; - "Oge", []; -]) - -let incr_or_decr = Sum("incr_or_decr", [ - "Incr", []; - "Decr", []; -]) - -(* From Csyntax *) - -let rec expr = Sum("expr", [ - "Eval", [val_; type_]; - "Evar", [ident; type_]; - "Efield", [expr; ident; type_]; - "Evalof", [expr; type_]; - "Ederef", [expr; type_]; - "Eaddrof", [expr; type_]; - "Eunop", [unary_operation; expr; type_]; - "Ebinop", [binary_operation; expr; expr; type_]; - "Ecast", [expr; type_]; - "Eseqand", [expr; expr; type_]; - "Eseqor", [expr; expr; type_]; - "Econdition", [expr; expr; expr; type_]; - "Esizeof", [type_; type_]; - "Ealignof", [type_; type_]; - "Eassign", [expr; expr; type_]; - "Eassignop", [binary_operation; expr; expr; type_; type_]; - "Epostincr", [incr_or_decr; expr; type_]; - "Ecomma", [expr; expr; type_]; - "Ecall", [expr; exprlist; type_]; - "Ebuiltin", [external_function; typelist; exprlist; type_]; - "Eloc", [block; int; type_]; - "Eparen", [expr; type_; type_]; -]) -and exprlist = Sum("exprlist", [ - "Enil", []; - "Econs", [expr; exprlist]; -]) - -let label = ident - -let rec statement = Sum("statement", [ - "Sskip", []; - "Sdo", [expr]; - "Ssequence", [statement; statement]; - "Sifthenelse", [expr; statement; statement]; - "Swhile", [expr; statement]; - "Sdowhile", [expr; statement]; - "Sfor", [statement; expr; statement; statement]; - "Sbreak", []; - "Scontinue", []; - "Sreturn", [option expr]; - "Sswitch", [expr; labeled_statements]; - "Slabel", [label; statement]; - "Sgoto", [label]; -]) -and labeled_statements = Sum("labeled_statements", [ - "LSnil", []; - "LScons", [option _Z; statement; labeled_statements]; -]) - -let function_ = Record("function", [ - "fn_return", type_; - "fn_callconv", calling_convention_d; - "fn_params", list (pair ident type_); - "fn_vars", list (pair ident type_); - "fn_body", statement; -]) - -let fundef = Sum("fundef", [ - "Internal", [function_]; - "External", [external_function; typelist; type_; calling_convention_d]; -]) - -let repr_program = Record("program", [ - "prog_defs", list (pair ident (globdef fundef type_)); - "prog_public", list ident; - "prog_main", ident; - "prog_types", list composite_definition; - "prog_comp_env", composite_env -]) - -type program2 = Program of - (AST.ident * (Csyntax.fundef, Ctypes.coq_type) AST.globdef) list - * AST.ident list - * AST.ident - * Ctypes.composite_definition list - -let program2 = Sum("program2", [ - "mkprogram", [list (pair ident (globdef fundef type_)); - list ident; - ident; - list composite_definition] -]) - -let program2_of_program p = - Csyntax.(Program(p.prog_defs, p.prog_public, p.prog_main, p.prog_types)) -let program_of_program2 (Program(d,p,m,t)) = - Csyntax.( - match Ctypes.build_composite_env t with - | Errors.Error _ -> assert false - | Errors.OK e -> {prog_defs = d; prog_public = p; prog_main = m; - prog_types = t; prog_comp_env = e}) - -let program = As(program2, { - conv_name = "program"; - conv_check = check repr_program; - conv_out = program2_of_program; - conv_in = program_of_program2 -}) - diff --git a/powerpc/Archi.v b/powerpc/Archi.v index 89f53ffd..10dc5534 100644 --- a/powerpc/Archi.v +++ b/powerpc/Archi.v @@ -20,10 +20,19 @@ Require Import ZArith. Require Import Fappli_IEEE. Require Import Fappli_IEEE_bits. +Definition ptr64 := false. + Definition big_endian := true. -Notation align_int64 := 8%Z (only parsing). -Notation align_float64 := 8%Z (only parsing). +Definition align_int64 := 8%Z. +Definition align_float64 := 8%Z. + +Definition splitlong := true. + +Lemma splitlong_ptr32: splitlong = true -> ptr64 = false. +Proof. + unfold splitlong, ptr64; congruence. +Qed. Program Definition default_pl_64 : bool * nan_pl 53 := (false, iter_nat 51 _ xO xH). @@ -39,7 +48,7 @@ Definition choose_binop_pl_32 (s1: bool) (pl1: nan_pl 24) (s2: bool) (pl2: nan_p Definition float_of_single_preserves_sNaN := true. -Global Opaque big_endian +Global Opaque ptr64 big_endian splitlong default_pl_64 choose_binop_pl_64 default_pl_32 choose_binop_pl_32 float_of_single_preserves_sNaN. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 9f8231e0..3c269083 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -100,11 +100,11 @@ Notation "'RA'" := LR (only parsing). Inductive constant: Type := | Cint: int -> constant - | Csymbol_low: ident -> int -> constant - | Csymbol_high: ident -> int -> constant - | Csymbol_sda: ident -> int -> constant - | Csymbol_rel_low: ident -> int -> constant - | Csymbol_rel_high: ident -> int -> constant. + | Csymbol_low: ident -> ptrofs -> constant + | Csymbol_high: ident -> ptrofs -> constant + | Csymbol_sda: ident -> ptrofs -> constant + | Csymbol_rel_low: ident -> ptrofs -> constant + | Csymbol_rel_high: ident -> ptrofs -> constant. (** A note on constants: while immediate operands to PowerPC instructions must be representable in 16 bits (with @@ -142,7 +142,7 @@ Inductive instruction : Type := | Paddic: ireg -> ireg -> constant -> instruction (**r add immediate and set carry *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) | Paddze: ireg -> ireg -> instruction (**r add carry *) - | Pallocframe: Z -> int -> int -> instruction (**r allocate new stack frame (pseudo) *) + | Pallocframe: Z -> ptrofs -> ptrofs -> instruction (**r allocate new stack frame (pseudo) *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) | Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *) @@ -179,7 +179,7 @@ Inductive instruction : Type := | Pextsb: ireg -> ireg -> instruction (**r 8-bit sign extension *) | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) | Pextsw: ireg -> ireg -> instruction (**r 64-bit sign extension (PPC64) *) - | Pfreeframe: Z -> int -> instruction (**r deallocate stack frame and restore previous frame (pseudo) *) + | Pfreeframe: Z -> ptrofs -> instruction (**r deallocate stack frame and restore previous frame (pseudo) *) | Pfabs: freg -> freg -> instruction (**r float absolute value *) | Pfabss: freg -> freg -> instruction (**r float absolute value *) | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) @@ -458,8 +458,8 @@ Variable ge: genv. symbolic references [symbol + offset] and splits their actual values into two 16-bit halves. *) -Parameter low_half: genv -> ident -> int -> val. -Parameter high_half: genv -> ident -> int -> val. +Parameter low_half: genv -> ident -> ptrofs -> val. +Parameter high_half: genv -> ident -> ptrofs -> val. (** The fundamental property of these operations is that, when applied to the address of a symbol, their results can be recombined by @@ -477,15 +477,15 @@ Axiom low_high_half: register pointing to the base of the small data area containing symbol [symb]. We leave this transformation up to the linker. *) -Parameter symbol_is_small_data: ident -> int -> bool. -Parameter small_data_area_offset: genv -> ident -> int -> val. +Parameter symbol_is_small_data: ident -> ptrofs -> bool. +Parameter small_data_area_offset: genv -> ident -> ptrofs -> val. Axiom small_data_area_addressing: forall id ofs, symbol_is_small_data id ofs = true -> small_data_area_offset ge id ofs = Genv.symbol_address ge id ofs. -Parameter symbol_is_rel_data: ident -> int -> bool. +Parameter symbol_is_rel_data: ident -> ptrofs -> bool. (** Armed with the [low_half] and [high_half] functions, we can define the evaluation of a symbolic constant. @@ -529,14 +529,14 @@ Inductive outcome: Type := instruction ([nextinstr]) or branching to a label ([goto_label]). *) Definition nextinstr (rs: regset) := - rs#PC <- (Val.add rs#PC Vone). + rs#PC <- (Val.offset_ptr rs#PC Ptrofs.one). Definition goto_label (f: function) (lbl: label) (rs: regset) (m: mem) := match label_pos lbl 0 (fn_code f) with | None => Stuck | Some pos => match rs#PC with - | Vptr b ofs => Next (rs#PC <- (Vptr b (Int.repr pos))) m + | Vptr b ofs => Next (rs#PC <- (Vptr b (Ptrofs.repr pos))) m | _ => Stuck end end. @@ -635,8 +635,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m | Pallocframe sz ofs _ => let (m1, stk) := Mem.alloc m 0 sz in - let sp := Vptr stk Int.zero in - match Mem.storev Mint32 m1 (Val.add sp (Vint ofs)) rs#GPR1 with + let sp := Vptr stk Ptrofs.zero in + match Mem.storev Mint32 m1 (Val.offset_ptr sp ofs) rs#GPR1 with | None => Stuck | Some m2 => Next (nextinstr (rs#GPR1 <- sp #GPR0 <- Vundef)) m2 end @@ -656,16 +656,16 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pbctr sg => Next (rs#PC <- (rs#CTR)) m | Pbctrl sg => - Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (rs#CTR)) m + Next (rs#LR <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (rs#CTR)) m | Pbf bit lbl => match rs#(reg_of_crbit bit) with | Vint n => if Int.eq n Int.zero then goto_label f lbl rs m else Next (nextinstr rs) m | _ => Stuck end | Pbl ident sg => - Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (Genv.symbol_address ge ident Int.zero)) m + Next (rs#LR <- (Val.offset_ptr rs#PC Ptrofs.one) #PC <- (Genv.symbol_address ge ident Ptrofs.zero)) m | Pbs ident sg => - Next (rs#PC <- (Genv.symbol_address ge ident Int.zero)) m + Next (rs#PC <- (Genv.symbol_address ge ident Ptrofs.zero)) m | Pblr => Next (rs#PC <- (rs#LR)) m | Pbt bit lbl => @@ -703,7 +703,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out | Pextsh rd r1 => Next (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m | Pfreeframe sz ofs => - match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with + match Mem.loadv Mint32 m (Val.offset_ptr rs#GPR1 ofs) with | None => Stuck | Some v => match rs#GPR1 with @@ -977,7 +977,7 @@ Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop := | extcall_arg_stack: forall ofs ty bofs v, bofs = Stacklayout.fe_ofs_arg + 4 * ofs -> Mem.loadv (chunk_of_type ty) m - (Val.add (rs (IR GPR1)) (Vint (Int.repr bofs))) = Some v -> + (Val.offset_ptr (rs (IR GPR1)) (Ptrofs.repr bofs)) = Some v -> extcall_arg rs m (S Outgoing ofs ty) v. Inductive extcall_arg_pair (rs: regset) (m: mem): rpair loc -> val -> Prop := @@ -1006,14 +1006,14 @@ Inductive step: state -> trace -> state -> Prop := forall b ofs f i rs m rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) f.(fn_code) = Some i -> + find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some i -> exec_instr f i rs m = Next rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_builtin: forall b ofs f ef args res rs m vargs t vres rs' m', rs PC = Vptr b ofs -> Genv.find_funct_ptr ge b = Some (Internal f) -> - find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> + find_instr (Ptrofs.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) -> eval_builtin_args ge rs (rs GPR1) m args vargs -> external_call ef ge vargs m t vres m' -> rs' = nextinstr @@ -1022,7 +1022,7 @@ Inductive step: state -> trace -> state -> Prop := step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', - rs PC = Vptr b Int.zero -> + rs PC = Vptr b Ptrofs.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> external_call ef ge args m t res m' -> extcall_arguments rs m (ef_sig ef) args -> @@ -1039,14 +1039,14 @@ Inductive initial_state (p: program): state -> Prop := let ge := Genv.globalenv p in let rs0 := (Pregmap.init Vundef) - # PC <- (Genv.symbol_address ge p.(prog_main) Int.zero) - # LR <- Vzero - # GPR1 <- Vzero in + # PC <- (Genv.symbol_address ge p.(prog_main) Ptrofs.zero) + # LR <- Vnullptr + # GPR1 <- Vnullptr in initial_state p (State rs0 m0). Inductive final_state: state -> int -> Prop := | final_state_intro: forall rs m r, - rs#PC = Vzero -> + rs#PC = Vnullptr -> rs#GPR3 = Vint r -> final_state (State rs m) r. @@ -1105,7 +1105,7 @@ Ltac Equalities := (* initial states *) inv H; inv H0. f_equal. congruence. (* final no step *) - inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence. + inv H. red; intros; red; intros. inv H; rewrite H0 in *; discriminate. (* final states *) inv H; inv H0. congruence. Qed. diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 4ad5e2f9..799d208e 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -125,12 +125,13 @@ Definition rolm (r1 r2: ireg) (amount mask: int) (k: code) := Definition accessind {A: Type} (instr1: A -> constant -> ireg -> instruction) (instr2: A -> ireg -> ireg -> instruction) - (base: ireg) (ofs: int) (r: A) (k: code) := + (base: ireg) (ofs: ptrofs) (r: A) (k: code) := + let ofs := Ptrofs.to_int ofs in if Int.eq (high_s ofs) Int.zero then instr1 r (Cint ofs) base :: k else loadimm GPR0 ofs (instr2 r base GPR0 :: k). -Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := +Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: code) := match ty, preg_of dst with | Tint, IR r => OK(accessind Plwz Plwzx base ofs r k) | Tany32, IR r => OK(accessind Plwz_a Plwzx_a base ofs r k) @@ -140,7 +141,7 @@ Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := | _, _ => Error (msg "Asmgen.loadind") end. -Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := +Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: code) := match ty, preg_of src with | Tint, IR r => OK(accessind Pstw Pstwx base ofs r k) | Tany32, IR r => OK(accessind Pstw_a Pstwx_a base ofs r k) @@ -340,7 +341,7 @@ Definition transl_op Paddis r GPR0 (Csymbol_high s ofs) :: Paddi r r (Csymbol_low s ofs) :: k) | Oaddrstack n, nil => - do r <- ireg_of res; OK (addimm r GPR1 n k) + do r <- ireg_of res; OK (addimm r GPR1 (Ptrofs.to_int n) k) | Ocast8signed, a1 :: nil => do r1 <- ireg_of a1; do r <- ireg_of res; OK (Pextsb r r1 :: k) | Ocast16signed, a1 :: nil => @@ -559,6 +560,7 @@ Definition transl_memory_access Paddis temp r1 (Csymbol_high symb ofs) :: mk1 (Csymbol_low symb ofs) temp :: k) | Ainstack ofs, nil => + let ofs := Ptrofs.to_int ofs in OK (if Int.eq (high_s ofs) Int.zero then mk1 (Cint ofs) GPR1 :: k else @@ -647,12 +649,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) | Mtailcall sig (inl r) => do r1 <- ireg_of r; OK (Pmtctr r1 :: - Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 :: Pmtlr GPR0 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbctr sig :: k) | Mtailcall sig (inr symb) => - OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 :: Pmtlr GPR0 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbs symb sig :: k) @@ -670,7 +672,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) do r <- ireg_of arg; OK (Pbtbl r tbl :: k) | Mreturn => - OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: + OK (Plwz GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 :: Pmtlr GPR0 :: Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pblr :: k) @@ -722,12 +724,12 @@ Definition transl_function (f: Mach.function) := OK (mkfunction f.(Mach.fn_sig) (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) f.(fn_retaddr_ofs) :: Pmflr GPR0 :: - Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: - Pcfi_rel_offset f.(fn_retaddr_ofs) :: c)). + Pstw GPR0 (Cint (Ptrofs.to_int f.(fn_retaddr_ofs))) GPR1 :: + Pcfi_rel_offset (Ptrofs.to_int f.(fn_retaddr_ofs)) :: c)). Definition transf_function (f: Mach.function) : res Asm.function := do tf <- transl_function f; - if zlt Int.max_unsigned (list_length_z tf.(fn_code)) + if zlt Ptrofs.max_unsigned (list_length_z tf.(fn_code)) then Error (msg "code size exceeded") else OK tf. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 44c81735..447a53a0 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -18,6 +18,8 @@ Require Import Values Memory Events Globalenvs Smallstep. Require Import Op Locations Mach Conventions Asm. Require Import Asmgen Asmgenproof0 Asmgenproof1. +Local Transparent Archi.ptr64. + Definition match_prog (p: Mach.program) (tp: Asm.program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. @@ -64,9 +66,9 @@ Qed. Lemma transf_function_no_overflow: forall f tf, - transf_function f = OK tf -> list_length_z tf.(fn_code) <= Int.max_unsigned. + transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. Proof. - intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. omega. Qed. @@ -181,10 +183,10 @@ Remark loadind_label: forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c. Proof. - unfold loadind, accessind; intros. + unfold loadind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *. destruct ty; try discriminate; destruct (preg_of dst); try discriminate; - destruct (Int.eq (high_s ofs) Int.zero); + destruct (Int.eq (high_s ofs') Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. @@ -192,10 +194,10 @@ Remark storeind_label: forall base ofs ty src k c, storeind src base ofs ty k = OK c -> tail_nolabel k c. Proof. - unfold storeind, accessind; intros. + unfold storeind, accessind; intros. set (ofs' := Ptrofs.to_int ofs) in *. destruct ty; try discriminate; destruct (preg_of src); try discriminate; - destruct (Int.eq (high_s ofs) Int.zero); + destruct (Int.eq (high_s ofs') Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. @@ -250,7 +252,7 @@ Proof. destruct (Int.eq (high_s i) Int.zero); TailNoLabel. destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. destruct (symbol_is_small_data i i0). TailNoLabel. destruct (symbol_is_rel_data i i0); TailNoLabel. - destruct (Int.eq (high_s i) Int.zero); TailNoLabel. + destruct (Int.eq (high_s (Ptrofs.to_int i)) Int.zero); TailNoLabel. Qed. Lemma transl_instr_label: @@ -307,7 +309,7 @@ Lemma transl_find_label: | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc end. Proof. - intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. rewrite transl_code'_transl_code in EQ0. simpl. eapply transl_code_label; eauto. Qed. @@ -332,10 +334,10 @@ Proof. intros [tc [A B]]. exploit label_pos_code_tail; eauto. instantiate (1 := 0). intros [pos' [P [Q R]]]. - exists tc; exists (rs#PC <- (Vptr b (Int.repr pos'))). + exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))). split. unfold goto_label. rewrite P. rewrite H1. auto. split. rewrite Pregmap.gss. constructor; auto. - rewrite Int.unsigned_repr. replace (pos' - 0) with pos' in Q. + rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. auto. omega. generalize (transf_function_no_overflow _ _ H0). omega. intros. apply Pregmap.gso; auto. @@ -351,7 +353,7 @@ Proof. - intros. exploit transl_instr_label; eauto. destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. - intros. monadInv H0. - destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. + destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. rewrite transl_code'_transl_code in EQ0. exists x; exists false; split; auto. unfold fn_code. repeat constructor. - exact transf_function_no_overflow. @@ -391,7 +393,7 @@ Inductive match_states: Mach.state -> Asm.state -> Prop := (STACKS: match_stack ge s) (MEXT: Mem.extends m m') (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = Vptr fb Int.zero) + (ATPC: rs PC = Vptr fb Ptrofs.zero) (ATLR: rs RA = parent_ra s), match_states (Mach.Callstate s fb ms m) (Asm.State rs m') @@ -598,14 +600,14 @@ Opaque loadind. eapply transf_function_no_overflow; eauto. destruct ros as [rf|fid]; simpl in H; monadInv H5. + (* Indirect call *) - assert (rs rf = Vptr f' Int.zero). + assert (rs rf = Vptr f' Ptrofs.zero). destruct (rs rf); try discriminate. - revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. - assert (rs0 x0 = Vptr f' Int.zero). + revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Ptrofs.zero). exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2. - assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add (Int.add ofs Int.one) Int.one)) fb f c false tf x). + assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add (Ptrofs.add ofs Ptrofs.one) Ptrofs.one)) fb f c false tf x). econstructor; eauto. exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. @@ -623,7 +625,7 @@ Opaque loadind. Simpl. rewrite <- H2. auto. + (* Direct call *) generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). + assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). econstructor; eauto. exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. @@ -639,7 +641,7 @@ Opaque loadind. - (* Mtailcall *) assert (f0 = f) by congruence. subst f0. inversion AT; subst. - assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). + assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. @@ -647,18 +649,18 @@ Opaque loadind. exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. destruct ros as [rf|fid]; simpl in H; monadInv H7. + (* Indirect call *) - assert (rs rf = Vptr f' Int.zero). + assert (rs rf = Vptr f' Ptrofs.zero). destruct (rs rf); try discriminate. - revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. - assert (rs0 x0 = Vptr f' Int.zero). + revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Ptrofs.zero). exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. - set (rs2 := nextinstr (rs0#CTR <- (Vptr f' Int.zero))). + set (rs2 := nextinstr (rs0#CTR <- (Vptr f' Ptrofs.zero))). set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))). set (rs4 := nextinstr (rs3#LR <- (parent_ra s))). set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))). set (rs6 := rs5#PC <- (rs5 CTR)). assert (exec_straight tge tf - (Pmtctr x0 :: Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 + (Pmtctr x0 :: Plwz GPR0 (Cint (Ptrofs.to_int (fn_retaddr_ofs f))) GPR1 :: Pmtlr GPR0 :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr sig :: x) rs0 m'0 (Pbctr sig :: x) rs5 m2'). @@ -667,7 +669,7 @@ Opaque loadind. apply exec_straight_step with rs3 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. change (rs2 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). - simpl. rewrite C. auto. congruence. auto. + erewrite loadv_offset_ptr by eexact C. auto. congruence. auto. apply exec_straight_step with rs4 m'0. simpl. reflexivity. reflexivity. apply exec_straight_one. @@ -678,7 +680,7 @@ Opaque loadind. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. - change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone). + change (rs5 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one) Ptrofs.one). rewrite <- H4; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. @@ -697,15 +699,15 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))). set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). - set (rs5 := rs4#PC <- (Vptr f' Int.zero)). + set (rs5 := rs4#PC <- (Vptr f' Ptrofs.zero)). assert (exec_straight tge tf - (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 + (Plwz GPR0 (Cint (Ptrofs.to_int (fn_retaddr_ofs f))) GPR1 :: Pmtlr GPR0 :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid sig :: x) rs0 m'0 (Pbs fid sig :: x) rs4 m2'). apply exec_straight_step with rs2 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - rewrite <- (sp_val _ _ _ AG). simpl. rewrite C. auto. congruence. auto. + rewrite <- (sp_val _ _ _ AG). erewrite loadv_offset_ptr by eexact C. auto. congruence. auto. apply exec_straight_step with rs3 m'0. simpl. reflexivity. reflexivity. apply exec_straight_one. @@ -715,7 +717,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. - change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + change (rs4 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one). rewrite <- H4; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. @@ -824,7 +826,7 @@ Local Transparent destroyed_by_jumptable. - (* Mreturn *) assert (f0 = f) by congruence. subst f0. inversion AT; subst. - assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned). + assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. @@ -838,12 +840,13 @@ Local Transparent destroyed_by_jumptable. set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). set (rs5 := rs4#PC <- (parent_ra s)). assert (exec_straight tge tf - (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 + (Plwz GPR0 (Cint (Ptrofs.to_int (fn_retaddr_ofs f))) GPR1 :: Pmtlr GPR0 :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pblr :: x) rs0 m'0 (Pblr :: x) rs4 m2'). simpl. apply exec_straight_three with rs2 m'0 rs3 m'0. - simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite C. auto. congruence. + simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. + erewrite loadv_offset_ptr by eexact C. auto. congruence. simpl. auto. simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG). rewrite E. auto. @@ -853,7 +856,7 @@ Local Transparent destroyed_by_jumptable. apply plus_right' with E0 (State rs4 m2') E0. eapply exec_straight_exec; eauto. econstructor. - change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). + change (rs4 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one). rewrite <- H3. simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. @@ -873,7 +876,7 @@ Local Transparent destroyed_by_jumptable. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Int.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. + destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. @@ -900,13 +903,13 @@ Local Transparent destroyed_by_jumptable. simpl. auto. auto. apply exec_straight_two with rs4 m3'. simpl. unfold store1. rewrite gpr_or_zero_not_zero. - change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. - rewrite Int.add_zero_l. simpl in P. rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. congruence. + change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). + simpl const_low. rewrite ATLR. erewrite storev_offset_ptr by eexact P. auto. congruence. auto. auto. auto. left; exists (State rs5 m3'); split. eapply exec_straight_steps_1; eauto. omega. constructor. econstructor; eauto. - change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone). + change (rs5 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one) Ptrofs.one). rewrite ATPC. simpl. constructor; eauto. subst x; simpl in g. unfold fn_code. eapply code_tail_next_int. omega. @@ -950,12 +953,12 @@ Proof. econstructor; split. econstructor. eapply (Genv.init_mem_transf_partial TRANSF); eauto. - replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Int.zero) - with (Vptr fb Int.zero). + replace (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero) + with (Vptr fb Ptrofs.zero). econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. simpl. unfold Vzero; congruence. intros. rewrite Regmap.gi. auto. + split. auto. simpl. unfold Vnullptr; simpl; congruence. intros. rewrite Regmap.gi. auto. unfold Genv.symbol_address. rewrite (match_program_main TRANSF). rewrite symbols_preserved. diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index aa2645f3..a7dcf41e 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -29,6 +29,8 @@ Require Import Asmgen. Require Import Conventions. Require Import Asmgenproof0. +Local Transparent Archi.ptr64. + (** * Properties of low half/high half decomposition *) Lemma low_high_u: @@ -97,7 +99,7 @@ Lemma add_zero_symbol_address: Val.add Vzero (Genv.symbol_address ge id ofs) = Genv.symbol_address ge id ofs. Proof. unfold Genv.symbol_address; intros. destruct (Genv.find_symbol ge id); auto. - simpl. rewrite Int.add_zero; auto. + simpl. rewrite Ptrofs.add_zero; auto. Qed. Lemma low_high_half_zero: @@ -147,6 +149,24 @@ Ltac Simplif := Ltac Simpl := repeat Simplif. +(** Useful properties of pointer addition *) + +Lemma loadv_offset_ptr: + forall chunk m a delta v, + Mem.loadv chunk m (Val.offset_ptr a delta) = Some v -> + Mem.loadv chunk m (Val.add a (Vint (Ptrofs.to_int delta))) = Some v. +Proof. + intros. destruct a; try discriminate H. simpl. rewrite Ptrofs.of_int_to_int by auto. assumption. +Qed. + +Lemma storev_offset_ptr: + forall chunk m a delta v m', + Mem.storev chunk m (Val.offset_ptr a delta) v = Some m' -> + Mem.storev chunk m (Val.add a (Vint (Ptrofs.to_int delta))) v = Some m'. +Proof. + intros. destruct a; try discriminate H. simpl. rewrite Ptrofs.of_int_to_int by auto. assumption. +Qed. + (** * Correctness of PowerPC constructor functions *) Section CONSTRUCTORS. @@ -425,23 +445,26 @@ Lemma accessind_load_correct: exec_instr ge fn (instr1 r1 cst r2) rs m = load1 ge chunk (inj r1) cst r2 rs m) -> (forall rs m r1 r2 r3, exec_instr ge fn (instr2 r1 r2 r3) rs m = load2 chunk (inj r1) r2 r3 rs m) -> - Mem.loadv chunk m (Val.add rs#base (Vint ofs)) = Some v -> + Mem.loadv chunk m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR0 -> inj rx <> PC -> exists rs', exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m /\ rs'#(inj rx) = v /\ forall r, r <> PC -> r <> inj rx -> r <> GPR0 -> rs'#r = rs#r. Proof. - intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero). + intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *. + assert (LD: Mem.loadv chunk m (Val.add (rs base) (Vint ofs')) = Some v) + by (apply loadv_offset_ptr; auto). + destruct (Int.eq (high_s ofs') Int.zero). - econstructor; split. apply exec_straight_one. rewrite H. unfold load1. rewrite gpr_or_zero_not_zero by auto. simpl. - rewrite H1. eauto. unfold nextinstr. repeat Simplif. + rewrite LD. eauto. unfold nextinstr. repeat Simplif. split. unfold nextinstr. repeat Simplif. intros. repeat Simplif. -- exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]]. +- exploit (loadimm_correct GPR0 ofs'); eauto. intros [rs' [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. apply exec_straight_one. rewrite H0. unfold load2. rewrite Q, R by auto with asmgen. - rewrite H1. reflexivity. unfold nextinstr. repeat Simplif. + rewrite LD. reflexivity. unfold nextinstr. repeat Simplif. split. repeat Simplif. intros. repeat Simplif. Qed. @@ -449,7 +472,7 @@ Qed. Lemma loadind_correct: forall (base: ireg) ofs ty dst k (rs: regset) m v c, loadind base ofs ty dst k = OK c -> - Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v -> + Mem.loadv (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) = Some v -> base <> GPR0 -> exists rs', exec_straight ge fn c rs m k rs' m @@ -475,29 +498,32 @@ Lemma accessind_store_correct: exec_instr ge fn (instr1 r1 cst r2) rs m = store1 ge chunk (inj r1) cst r2 rs m) -> (forall rs m r1 r2 r3, exec_instr ge fn (instr2 r1 r2 r3) rs m = store2 chunk (inj r1) r2 r3 rs m) -> - Mem.storev chunk m (Val.add rs#base (Vint ofs)) (rs (inj rx)) = Some m' -> + Mem.storev chunk m (Val.offset_ptr rs#base ofs) (rs (inj rx)) = Some m' -> base <> GPR0 -> inj rx <> PC -> inj rx <> GPR0 -> exists rs', exec_straight ge fn (accessind instr1 instr2 base ofs rx k) rs m k rs' m' /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r. Proof. - intros. unfold accessind. destruct (Int.eq (high_s ofs) Int.zero). + intros. unfold accessind. set (ofs' := Ptrofs.to_int ofs) in *. + assert (ST: Mem.storev chunk m (Val.add (rs base) (Vint ofs')) (rs (inj rx)) = Some m') + by (apply storev_offset_ptr; auto). + destruct (Int.eq (high_s ofs') Int.zero). - econstructor; split. apply exec_straight_one. rewrite H. unfold store1. rewrite gpr_or_zero_not_zero by auto. simpl. - rewrite H1. eauto. unfold nextinstr. repeat Simplif. + rewrite ST. eauto. unfold nextinstr. repeat Simplif. intros. repeat Simplif. -- exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [P [Q R]]]. +- exploit (loadimm_correct GPR0 ofs'); eauto. intros [rs' [P [Q R]]]. econstructor; split. eapply exec_straight_trans. eexact P. apply exec_straight_one. rewrite H0. unfold store2. rewrite Q. rewrite R by auto with asmgen. rewrite R by auto. - rewrite H1. reflexivity. unfold nextinstr. repeat Simplif. + rewrite ST. reflexivity. unfold nextinstr. repeat Simplif. intros. repeat Simplif. Qed. Lemma storeind_correct: forall (base: ireg) ofs ty src k (rs: regset) m m' c, storeind src base ofs ty k = OK c -> - Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> + Mem.storev (chunk_of_type ty) m (Val.offset_ptr rs#base ofs) (rs#(preg_of src)) = Some m' -> base <> GPR0 -> exists rs', exec_straight ge fn c rs m k rs' m' @@ -822,7 +848,7 @@ Qed. Ltac TranslOpSimpl := econstructor; split; [ apply exec_straight_one; [simpl; eauto | reflexivity] - | split; intros; Simpl; fail ]. + | split; [ apply Val.lessdef_same; Simpl; fail | intros; Simpl; fail ] ]. Lemma transl_op_correct_aux: forall op args res k (rs: regset) m v c, @@ -830,9 +856,10 @@ Lemma transl_op_correct_aux: eval_operation ge (rs#GPR1) op (map rs (map preg_of args)) m = Some v -> exists rs', exec_straight ge fn c rs m k rs' m - /\ rs'#(preg_of res) = v + /\ Val.lessdef v rs'#(preg_of res) /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. Proof. + assert (SAME: forall v1 v2, v1 = v2 -> Val.lessdef v2 v1). { intros; subst; auto. } Opaque Int.eq. intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl. (* Omove *) @@ -841,28 +868,32 @@ Opaque Int.eq. TranslOpSimpl. (* Ointconst *) destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. - exists rs'. auto with asmgen. + exists rs'. rewrite B. auto with asmgen. (* Oaddrsymbol *) set (v' := Genv.symbol_address ge i i0). destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. (* small data *) Opaque Val.add. econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. + split. apply SAME. Simpl. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. (* relative data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. Simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. Simpl. + split. apply SAME. Simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. Simpl. apply low_high_half_zero. intros; Simpl. (* absolute data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. + split. apply SAME. Simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. apply low_high_half_zero. intros; Simpl. (* Oaddrstack *) - destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. - exists rs'; auto with asmgen. + destruct (addimm_correct x GPR1 (Ptrofs.to_int i) k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. + exists rs'; split. auto. split; auto with asmgen. + rewrite RES. destruct (rs GPR1); simpl; auto. +Transparent Val.add. + simpl. rewrite Ptrofs.of_int_to_int; auto. +Opaque Val.add. (* Oaddimm *) destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. exists rs'; auto with asmgen. @@ -870,7 +901,7 @@ Opaque Val.add. destruct (symbol_is_small_data i i0) eqn:SD; [ | destruct (symbol_is_rel_data i i0) ]. (* small data *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. Simpl. rewrite (Val.add_commut (rs x)). f_equal. + split. apply SAME. Simpl. rewrite (Val.add_commut (rs x)). f_equal. rewrite small_data_area_addressing by auto. apply add_zero_symbol_address. intros; Simpl. (* relative data *) @@ -918,7 +949,8 @@ Opaque Val.add. split. rewrite D; auto with asmgen. unfold rs1; Simpl. intros. rewrite D; auto with asmgen. unfold rs1; Simpl. (* Oandimm *) - destruct (andimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. + destruct (andimm_correct x0 x i k rs m) as [rs' [A [B C]]]. eauto with asmgen. + exists rs'; auto with asmgen. (* Oorimm *) destruct (orimm_correct x0 x i k rs m) as [rs' [A [B C]]]. exists rs'; auto with asmgen. @@ -933,10 +965,11 @@ Opaque Val.add. (* Oshrximm *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. Simpl. apply Val.shrx_carry. auto. + split. Simpl. apply SAME. apply Val.shrx_carry. auto. intros; Simpl. (* Orolm *) - destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]; eauto with asmgen. + destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]. eauto with asmgen. + exists rs'; auto. (* Ointoffloat *) replace v with (Val.maketotal (Val.intoffloat (rs x))). TranslOpSimpl. @@ -973,9 +1006,8 @@ Proof. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. intros [v' [A B]]. rewrite (sp_val _ _ _ H0) in A. exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]]. - rewrite <- Q in B. exists rs'; split. eexact P. - split. apply agree_set_undef_mreg with rs; auto. + split. apply agree_set_undef_mreg with rs; auto. eapply Val.lessdef_trans; eauto. auto. Qed. @@ -987,12 +1019,12 @@ Lemma transl_memory_access_correct: eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a -> temp <> GPR0 -> (forall cst (r1: ireg) (rs1: regset) k, - Val.add (gpr_or_zero rs1 r1) (const_low ge cst) = a -> + Val.lessdef a (Val.add (gpr_or_zero rs1 r1) (const_low ge cst)) -> (forall r, r <> PC -> r <> temp -> r <> GPR0 -> rs1 r = rs r) -> exists rs', exec_straight ge fn (mk1 cst r1 :: k) rs1 m k rs' m' /\ P rs') -> (forall (r1 r2: ireg) (rs1: regset) k, - Val.add rs1#r1 rs1#r2 = a -> + Val.lessdef a (Val.add rs1#r1 rs1#r2) -> (forall r, r <> PC -> r <> temp -> r <> GPR0 -> rs1 r = rs r) -> exists rs', exec_straight ge fn (mk2 r1 r2 :: k) rs1 m k rs' m' /\ P rs') -> @@ -1023,14 +1055,14 @@ Transparent Val.add. destruct (symbol_is_small_data i i0) eqn:SISD; [ | destruct (symbol_is_rel_data i i0) ]; inv TR. (* Aglobal from small data *) apply MK1. unfold const_low. rewrite small_data_area_addressing by auto. - apply add_zero_symbol_address. + rewrite add_zero_symbol_address. auto. auto. (* Aglobal from relative data *) set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). set (rs2 := nextinstr (rs1#temp <- (Genv.symbol_address ge i i0))). exploit (MK1 (Cint Int.zero) temp rs2). simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. - unfold rs2. Simpl. rewrite Val.add_commut. apply add_zero_symbol_address. + unfold rs2. Simpl. rewrite Val.add_commut. rewrite add_zero_symbol_address. auto. intros; unfold rs2, rs1; Simpl. intros [rs' [EX' AG']]. exists rs'; split. apply exec_straight_step with rs1 m; auto. @@ -1042,7 +1074,7 @@ Transparent Val.add. set (rs1 := nextinstr (rs#temp <- (Val.add Vzero (high_half ge i i0)))). exploit (MK1 (Csymbol_low i i0) temp rs1). simpl. rewrite gpr_or_zero_not_zero by eauto with asmgen. - unfold rs1. Simpl. apply low_high_half_zero. + unfold rs1. Simpl. rewrite low_high_half_zero. auto. intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'; split. apply exec_straight_step with rs1 m; auto. @@ -1052,7 +1084,7 @@ Transparent Val.add. (* Abased from small data *) set (rs1 := nextinstr (rs#GPR0 <- (Genv.symbol_address ge i i0))). exploit (MK2 x GPR0 rs1 k). - unfold rs1; Simpl. apply Val.add_commut. + unfold rs1; Simpl. rewrite Val.add_commut. auto. intros. unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'; split. apply exec_straight_step with rs1 m. @@ -1079,17 +1111,20 @@ Transparent Val.add. exploit (MK1 (Csymbol_low i i0) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. unfold rs1. Simpl. - rewrite Val.add_assoc. rewrite low_high_half. apply Val.add_commut. + rewrite Val.add_assoc. rewrite low_high_half. rewrite Val.add_commut. auto. intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. assumption. assumption. (* Ainstack *) - destruct (Int.eq (high_s i) Int.zero); inv TR. + set (ofs := Ptrofs.to_int i) in *. + assert (L: Val.lessdef (Val.offset_ptr (rs GPR1) i) (Val.add (rs GPR1) (Vint ofs))). + { destruct (rs GPR1); simpl; auto. unfold ofs; rewrite Ptrofs.of_int_to_int; auto. } + destruct (Int.eq (high_s ofs) Int.zero); inv TR. apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. - set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s i) (Int.repr 16)))))). - exploit (MK1 (Cint (low_s i)) temp rs1 k). + set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). + exploit (MK1 (Cint (low_s ofs)) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; auto. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. @@ -1114,6 +1149,8 @@ Lemma transl_load_correct: /\ forall r, r <> PC -> r <> GPR12 -> r <> GPR0 -> r <> preg_of dst -> rs' r = rs r. Proof. intros. + assert (LD: forall v, Val.lessdef a v -> v = a). + { intros. inv H2; auto. discriminate H1. } assert (BASE: forall mk1 mk2 k' chunk' v', transl_memory_access mk1 mk2 addr args GPR12 k' = OK c -> Mem.loadv chunk' m a = Some v' -> @@ -1130,11 +1167,11 @@ Proof. { intros. eapply transl_memory_access_correct; eauto. congruence. intros. econstructor; split. apply exec_straight_one. - rewrite H4. unfold load1. rewrite H6. rewrite H3. eauto. + rewrite H4. unfold load1. apply LD in H6. rewrite H6. rewrite H3. eauto. unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen. intuition Simpl. intros. econstructor; split. apply exec_straight_one. - rewrite H5. unfold load2. rewrite H6. rewrite H3. eauto. + rewrite H5. unfold load2. apply LD in H6. rewrite H6. rewrite H3. eauto. unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen. intuition Simpl. } @@ -1144,10 +1181,10 @@ Proof. { destruct a; simpl in *; try discriminate. rewrite Mem.load_int8_signed_unsigned in H1. - destruct (Mem.load Mint8unsigned m b (Int.unsigned i)); simpl in H1; inv H1. + destruct (Mem.load Mint8unsigned m b (Ptrofs.unsigned i)); simpl in H1; inv H1. exists v0; auto. } - destruct H as [v1 [LD SG]]. clear H1. + destruct H as [v1 [LD' SG]]. clear H1. exploit BASE; eauto; erewrite ireg_of_eq by eauto; auto. intros [rs1 [A [B C]]]. econstructor; split. @@ -1180,6 +1217,8 @@ Lemma transl_store_correct: Proof. Local Transparent destroyed_by_store. intros. + assert (LD: forall v, Val.lessdef a v -> v = a). + { intros. inv H2; auto. discriminate H1. } assert (TEMP0: int_temp_for src = GPR11 \/ int_temp_for src = GPR12). unfold int_temp_for. destruct (mreg_eq src R12); auto. assert (TEMP1: int_temp_for src <> GPR0). @@ -1204,10 +1243,10 @@ Local Transparent destroyed_by_store. { intros. eapply transl_memory_access_correct; eauto. intros. econstructor; split. apply exec_straight_one. - rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. + rewrite H4. unfold store1. apply LD in H6. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. intros. econstructor; split. apply exec_straight_one. - rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. + rewrite H5. unfold store2. apply LD in H6. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. intros; Simpl. apply H7; auto. destruct TEMP0; destruct H10; congruence. } destruct chunk; monadInv H. diff --git a/powerpc/ConstpropOp.vp b/powerpc/ConstpropOp.vp index 7265337d..e768e4a9 100644 --- a/powerpc/ConstpropOp.vp +++ b/powerpc/ConstpropOp.vp @@ -13,15 +13,25 @@ (** Strength reduction for operators and conditions. This is the machine-dependent part of [Constprop]. *) -Require Import Coqlib. -Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Op. -Require Import Registers. +Require Import Coqlib Compopts. +Require Import AST Integers Floats. +Require Import Op Registers. Require Import ValueDomain. +(** * Converting known values to constants *) + +Parameter symbol_is_external: ident -> bool. (**r See [SelectOp] *) + +Definition const_for_result (a: aval) : option operation := + match a with + | I n => Some(Ointconst n) + | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None + | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None + | Ptr(Gl id ofs) => Some (Oaddrsymbol id ofs) + | Ptr(Stk ofs) => Some(Oaddrstack ofs) + | _ => None + end. + (** * Operator strength reduction *) (** We now define auxiliary functions for strength reduction of @@ -187,13 +197,13 @@ Nondetfunction addr_strength_reduction (addr: addressing) (args: list reg) (vl: list aval) := match addr, args, vl with | Aindexed2, r1 :: r2 :: nil, Ptr(Gl symb n1) :: I n2 :: nil => - (Aglobal symb (Int.add n1 n2), nil) + (Aglobal symb (Ptrofs.add n1 (Ptrofs.of_int n2)), nil) | Aindexed2, r1 :: r2 :: nil, I n1 :: Ptr(Gl symb n2) :: nil => - (Aglobal symb (Int.add n1 n2), nil) + (Aglobal symb (Ptrofs.add (Ptrofs.of_int n1) n2), nil) | Aindexed2, r1 :: r2 :: nil, Ptr(Stk n1) :: I n2 :: nil => - (Ainstack (Int.add n1 n2), nil) + (Ainstack (Ptrofs.add n1 (Ptrofs.of_int n2)), nil) | Aindexed2, r1 :: r2 :: nil, I n1 :: Ptr(Stk n2) :: nil => - (Ainstack (Int.add n1 n2), nil) + (Ainstack (Ptrofs.add (Ptrofs.of_int n1) n2), nil) | Aindexed2, r1 :: r2 :: nil, Ptr(Gl symb n1) :: v2 :: nil => (Abased symb n1, r2 :: nil) | Aindexed2, r1 :: r2 :: nil, v1 :: Ptr(Gl symb n2) :: nil => @@ -203,11 +213,11 @@ Nondetfunction addr_strength_reduction | Aindexed2, r1 :: r2 :: nil, v1 :: I n2 :: nil => (Aindexed n2, r1 :: nil) | Abased symb ofs, r1 :: nil, I n1 :: nil => - (Aglobal symb (Int.add ofs n1), nil) + (Aglobal symb (Ptrofs.add ofs (Ptrofs.of_int n1)), nil) | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil => - (Aglobal symb (Int.add n1 n), nil) + (Aglobal symb (Ptrofs.add n1 (Ptrofs.of_int n)), nil) | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil => - (Ainstack (Int.add n1 n), nil) + (Ainstack (Ptrofs.add n1 (Ptrofs.of_int n)), nil) | _, _, _ => (addr, args) end. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index eb68f586..bb0605ee 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -12,21 +12,13 @@ (** Correctness proof for operator strength reduction. *) -Require Import Coqlib. -Require Import Compopts. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Memory. -Require Import Globalenvs. -Require Import Events. -Require Import Op. -Require Import Registers. -Require Import RTL. -Require Import ValueDomain. +Require Import Coqlib Compopts. +Require Import Integers Floats Values Memory Globalenvs Events. +Require Import Op Registers RTL ValueDomain. Require Import ConstpropOp. +Local Transparent Archi.ptr64. + (** * Correctness of strength reduction *) (** We now show that strength reduction over operators and addressing @@ -95,6 +87,28 @@ Ltac SimplVM := | _ => idtac end. +Lemma const_for_result_correct: + forall a op v, + const_for_result a = Some op -> + vmatch bc v a -> + exists v', eval_operation ge (Vptr sp Ptrofs.zero) op nil m = Some v' /\ Val.lessdef v v'. +Proof. + unfold const_for_result; intros. + destruct a; inv H; SimplVM. +- (* integer *) + exists (Vint n); auto. +- (* float *) + destruct (generate_float_constants tt); inv H2. exists (Vfloat f); auto. +- (* single *) + destruct (generate_float_constants tt); inv H2. exists (Vsingle f); auto. +- (* pointer *) + destruct p; try discriminate; SimplVM. + + (* global *) + inv H2. exists (Genv.symbol_address ge id ofs); auto. + + (* stack *) + inv H2. exists (Vptr sp ofs); split; auto. simpl. rewrite Ptrofs.add_zero_l; auto. +Qed. + Lemma cond_strength_reduction_correct: forall cond args vl, vl = map (fun r => AE.get r ae) args -> @@ -114,7 +128,7 @@ Lemma make_cmp_base_correct: forall c args vl, vl = map (fun r => AE.get r ae) args -> let (op', args') := make_cmp_base c args vl in - exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v. Proof. intros. unfold make_cmp_base. @@ -127,7 +141,7 @@ Lemma make_cmp_correct: forall c args vl, vl = map (fun r => AE.get r ae) args -> let (op', args') := make_cmp c args vl in - exists v, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some v + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some v /\ Val.lessdef (Val.of_optbool (eval_condition c rs##args m)) v. Proof. intros c args vl. @@ -159,11 +173,11 @@ Qed. Lemma make_addimm_correct: forall n r, let (op, args) := make_addimm n r in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.add rs#r (Vint n)) v. Proof. intros. unfold make_addimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. - subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto; rewrite Int.add_zero; auto. + subst. exists (rs#r); split; auto. destruct (rs#r); simpl; auto. rewrite Int.add_zero; auto. rewrite Ptrofs.add_zero; auto. exists (Val.add rs#r (Vint n)); auto. Qed. @@ -171,7 +185,7 @@ Lemma make_shlimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shlimm n r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shl rs#r1 (Vint n)) v. Proof. intros; unfold make_shlimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -185,7 +199,7 @@ Lemma make_shrimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shrimm n r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shr rs#r1 (Vint n)) v. Proof. intros; unfold make_shrimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -199,7 +213,7 @@ Lemma make_shruimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_shruimm n r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.shru rs#r1 (Vint n)) v. Proof. intros; unfold make_shruimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -213,7 +227,7 @@ Lemma make_mulimm_correct: forall n r1 r2, rs#r2 = Vint n -> let (op, args) := make_mulimm n r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mul rs#r1 (Vint n)) v. Proof. intros; unfold make_mulimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. subst. @@ -232,7 +246,7 @@ Lemma make_divimm_correct: Val.divs rs#r1 rs#r2 = Some v -> rs#r2 = Vint n -> let (op, args) := make_divimm n r1 r2 in - exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divimm. destruct (Int.is_power2 n) eqn:?. @@ -247,7 +261,7 @@ Lemma make_divuimm_correct: Val.divu rs#r1 rs#r2 = Some v -> rs#r2 = Vint n -> let (op, args) := make_divuimm n r1 r2 in - exists w, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some w /\ Val.lessdef v w. Proof. intros; unfold make_divuimm. destruct (Int.is_power2 n) eqn:?. @@ -264,7 +278,7 @@ Lemma make_andimm_correct: forall n r x, vmatch bc rs#r x -> let (op, args) := make_andimm n r x in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.and rs#r (Vint n)) v. Proof. intros; unfold make_andimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -289,7 +303,7 @@ Qed. Lemma make_orimm_correct: forall n r, let (op, args) := make_orimm n r in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.or rs#r (Vint n)) v. Proof. intros; unfold make_orimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -302,7 +316,7 @@ Qed. Lemma make_xorimm_correct: forall n r, let (op, args) := make_xorimm n r in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.xor rs#r (Vint n)) v. Proof. intros; unfold make_xorimm. predSpec Int.eq Int.eq_spec n Int.zero; intros. @@ -316,7 +330,7 @@ Lemma make_mulfimm_correct: forall n r1 r2, rs#r2 = Vfloat n -> let (op, args) := make_mulfimm n r1 r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. @@ -329,7 +343,7 @@ Lemma make_mulfimm_correct_2: forall n r1 r2, rs#r1 = Vfloat n -> let (op, args) := make_mulfimm n r2 r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulf rs#r1 rs#r2) v. Proof. intros; unfold make_mulfimm. destruct (Float.eq_dec n (Float.of_int (Int.repr 2))); intros. @@ -343,7 +357,7 @@ Lemma make_mulfsimm_correct: forall n r1 r2, rs#r2 = Vsingle n -> let (op, args) := make_mulfsimm n r1 r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. Proof. intros; unfold make_mulfsimm. destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. @@ -356,7 +370,7 @@ Lemma make_mulfsimm_correct_2: forall n r1 r2, rs#r1 = Vsingle n -> let (op, args) := make_mulfsimm n r2 r1 r2 in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.mulfs rs#r1 rs#r2) v. Proof. intros; unfold make_mulfsimm. destruct (Float32.eq_dec n (Float32.of_int (Int.repr 2))); intros. @@ -370,7 +384,7 @@ Lemma make_cast8signed_correct: forall r x, vmatch bc rs#r x -> let (op, args) := make_cast8signed r x in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 8 rs#r) v. Proof. intros; unfold make_cast8signed. destruct (vincl x (Sgn Ptop 8)) eqn:INCL. exists rs#r; split; auto. @@ -384,7 +398,7 @@ Lemma make_cast16signed_correct: forall r x, vmatch bc rs#r x -> let (op, args) := make_cast16signed r x in - exists v, eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. + exists v, eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v /\ Val.lessdef (Val.sign_ext 16 rs#r) v. Proof. intros; unfold make_cast16signed. destruct (vincl x (Sgn Ptop 16)) eqn:INCL. exists rs#r; split; auto. @@ -397,9 +411,9 @@ Qed. Lemma op_strength_reduction_correct: forall op args vl v, vl = map (fun r => AE.get r ae) args -> - eval_operation ge (Vptr sp Int.zero) op rs##args m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op rs##args m = Some v -> let (op', args') := op_strength_reduction op args vl in - exists w, eval_operation ge (Vptr sp Int.zero) op' rs##args' m = Some w /\ Val.lessdef v w. + exists w, eval_operation ge (Vptr sp Ptrofs.zero) op' rs##args' m = Some w /\ Val.lessdef v w. Proof. intros until v; unfold op_strength_reduction; case (op_strength_reduction_match op args vl); simpl; intros. @@ -408,7 +422,12 @@ Proof. (* cast8signed *) InvApproxRegs; SimplVM; inv H0. apply make_cast16signed_correct; auto. (* add *) - InvApproxRegs; SimplVM; inv H0. fold (Val.add (Vint n1) rs#r2). rewrite Val.add_commut. apply make_addimm_correct. + InvApproxRegs; SimplVM; inv H0. + change (let (op', args') := make_addimm n1 r2 in + exists w : val, + eval_operation ge (Vptr sp Ptrofs.zero) op' rs ## args' m = Some w /\ + Val.lessdef (Val.add (Vint n1) rs#r2) w). + rewrite Val.add_commut. apply make_addimm_correct. InvApproxRegs; SimplVM; inv H0. apply make_addimm_correct. InvApproxRegs; SimplVM; inv H0. econstructor; split; eauto. apply Val.add_lessdef; auto. InvApproxRegs; SimplVM; inv H0. econstructor; split; eauto. rewrite Val.add_commut. apply Val.add_lessdef; auto. @@ -454,34 +473,46 @@ Proof. exists v; auto. Qed. +Remark shift_symbol_address: + forall id ofs delta, + Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int delta)) = Val.add (Genv.symbol_address ge id ofs) (Vint delta). +Proof. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. +Qed. + Lemma addr_strength_reduction_correct: forall addr args vl res, vl = map (fun r => AE.get r ae) args -> - eval_addressing ge (Vptr sp Int.zero) addr rs##args = Some res -> + eval_addressing ge (Vptr sp Ptrofs.zero) addr rs##args = Some res -> let (addr', args') := addr_strength_reduction addr args vl in - exists res', eval_addressing ge (Vptr sp Int.zero) addr' rs##args' = Some res' /\ Val.lessdef res res'. + exists res', eval_addressing ge (Vptr sp Ptrofs.zero) addr' rs##args' = Some res' /\ Val.lessdef res res'. Proof. intros until res. unfold addr_strength_reduction. destruct (addr_strength_reduction_match addr args vl); simpl; intros VL EA; InvApproxRegs; SimplVM; try (inv EA). -- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. -- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite Val.add_commut. - econstructor; split; eauto. apply Val.add_lessdef; auto. -- rewrite Int.add_zero_l. - change (Vptr sp (Int.add n1 n2)) with (Val.add (Vptr sp n1) (Vint n2)). +- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. +- econstructor; split; eauto. + change (Val.lessdef (Val.add (Vint n1) rs#r2) (Genv.symbol_address ge symb (Ptrofs.add (Ptrofs.of_int n1) n2))). + rewrite Ptrofs.add_commut. rewrite shift_symbol_address. rewrite Val.add_commut. + apply Val.add_lessdef; auto. +- rewrite Ptrofs.add_zero_l. + change (Vptr sp (Ptrofs.add n1 (Ptrofs.of_int n2))) with (Val.add (Vptr sp n1) (Vint n2)). econstructor; split; eauto. apply Val.add_lessdef; auto. -- fold (Val.add (Vint n1) rs#r2). rewrite Int.add_zero_l. rewrite Int.add_commut. - change (Vptr sp (Int.add n2 n1)) with (Val.add (Vptr sp n2) (Vint n1)). - rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. +- econstructor; split; eauto. + change (Val.lessdef (Val.add (Vint n1) rs#r2) (Vptr sp (Ptrofs.add Ptrofs.zero (Ptrofs.add (Ptrofs.of_int n1) n2)))). + rewrite Ptrofs.add_zero_l. rewrite Ptrofs.add_commut. + change (Val.lessdef (Val.add (Vint n1) rs#r2) (Val.add (Vptr sp n2) (Vint n1))). + rewrite Val.add_commut. apply Val.add_lessdef; auto. - econstructor; split; eauto. apply Val.add_lessdef; auto. - rewrite Val.add_commut. econstructor; split; eauto. apply Val.add_lessdef; auto. -- fold (Val.add (Vint n1) rs#r2). - rewrite Val.add_commut. econstructor; split; eauto. - econstructor; split; eauto. -- rewrite Genv.shift_symbol_address. econstructor; split; eauto. -- rewrite Genv.shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. -- rewrite Int.add_zero_l. - change (Vptr sp (Int.add n1 n)) with (Val.add (Vptr sp n1) (Vint n)). + change (Val.lessdef (Val.add (Vint n1) rs#r2) (Val.add rs#r2 (Vint n1))). + rewrite Val.add_commut. auto. +- econstructor; split; eauto. +- rewrite shift_symbol_address. econstructor; split; eauto. +- rewrite shift_symbol_address. econstructor; split; eauto. apply Val.add_lessdef; auto. +- rewrite Ptrofs.add_zero_l. + change (Vptr sp (Ptrofs.add n1 (Ptrofs.of_int n))) with (Val.add (Vptr sp n1) (Vint n)). econstructor; split; eauto. apply Val.add_lessdef; auto. - exists res; auto. Qed. diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v index 1605de73..b83ab6da 100644 --- a/powerpc/Conventions1.v +++ b/powerpc/Conventions1.v @@ -61,6 +61,17 @@ Definition destroyed_at_call := Definition dummy_int_reg := R3. (**r Used in [Coloring]. *) Definition dummy_float_reg := F0. (**r Used in [Coloring]. *) +Definition is_float_reg (r: mreg): bool := + match r with + | R3 | R4 | R5 | R6 | R7 | R8 | R9 | R10 | R11 | R12 + | R14 | R15 | R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 | R24 + | R25 | R26 | R27 | R28 | R29 | R30 | R31 => false + | F0 | F1 | F2 | F3 | F4 | F5 | F6 | F7 + | F8 | F9 | F10 | F11 | F12 | F13 + | F14 | F15 | F16 | F17 | F18 | F19 | F20 | F21 | F22 | F23 + | F24 | F25 | F26 | F27 | F28 | F29 | F30 | F31 => true + end. + (** * Function calling conventions *) (** The functions in this section determine the locations (machine registers @@ -118,11 +129,22 @@ Lemma loc_result_pair: forall sg, match loc_result sg with | One _ => True - | Twolong r1 r2 => r1 <> r2 /\ sg.(sig_res) = Some Tlong /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + | Twolong r1 r2 => + r1 <> r2 /\ sg.(sig_res) = Some Tlong + /\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true + /\ Archi.splitlong = true end. Proof. intros; unfold loc_result; destruct (sig_res sg) as [[]|]; auto. - simpl; destruct Archi.ppc64; intuition congruence. + simpl; intuition congruence. +Qed. + +(** The location of the result depends only on the result part of the signature *) + +Lemma loc_result_exten: + forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2. +Proof. + intros. unfold loc_result. rewrite H; auto. Qed. (** ** Location of function arguments *) diff --git a/powerpc/NeedOp.v b/powerpc/NeedOp.v index 4d8c32bd..956b5d43 100644 --- a/powerpc/NeedOp.v +++ b/powerpc/NeedOp.v @@ -108,11 +108,11 @@ Qed. Lemma needs_of_operation_sound: forall op args v nv args', - eval_operation ge (Vptr sp Int.zero) op args m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op args m = Some v -> vagree_list args args' (needs_of_operation op nv) -> nv <> Nothing -> exists v', - eval_operation ge (Vptr sp Int.zero) op args' m' = Some v' + eval_operation ge (Vptr sp Ptrofs.zero) op args' m' = Some v' /\ vagree v v' nv. Proof. unfold needs_of_operation; intros; destruct op; try (eapply default_needs_of_operation_sound; eauto; fail); @@ -147,7 +147,7 @@ Qed. Lemma operation_is_redundant_sound: forall op nv arg1 args v arg1' args', operation_is_redundant op nv = true -> - eval_operation ge (Vptr sp Int.zero) op (arg1 :: args) m = Some v -> + eval_operation ge (Vptr sp Ptrofs.zero) op (arg1 :: args) m = Some v -> vagree_list (arg1 :: args) (arg1' :: args') (needs_of_operation op nv) -> vagree v arg1' nv. Proof. diff --git a/powerpc/Op.v b/powerpc/Op.v index c8028557..d59afd97 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -34,6 +34,7 @@ Require Import Globalenvs. Require Import Events. Set Implicit Arguments. +Local Transparent Archi.ptr64. (** Conditions (boolean-valued operators). *) @@ -55,14 +56,14 @@ Inductive operation : Type := | Ointconst: int -> operation (**r [rd] is set to the given integer constant *) | Ofloatconst: float -> operation (**r [rd] is set to the given float constant *) | Osingleconst: float32 -> 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 *) + | Oaddrsymbol: ident -> ptrofs -> operation (**r [rd] is set to the the address of the symbol plus the offset *) + | Oaddrstack: ptrofs -> 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] *) | Ocast16signed: operation (**r [rd] is 16-bit sign extension of [r1] *) | Oadd: operation (**r [rd = r1 + r2] *) | Oaddimm: int -> operation (**r [rd = r1 + n] *) - | Oaddsymbol: ident -> int -> operation (**r [rd = addr(id + ofs) + r1] *) + | Oaddsymbol: ident -> ptrofs -> operation (**r [rd = addr(id + ofs) + r1] *) | Osub: operation (**r [rd = r1 - r2] *) | Osubimm: int -> operation (**r [rd = n - r1] *) | Omul: operation (**r [rd = r1 * r2] *) @@ -124,9 +125,9 @@ Inductive operation : Type := Inductive addressing: Type := | Aindexed: int -> addressing (**r Address is [r1 + offset] *) | Aindexed2: addressing (**r Address is [r1 + r2] *) - | Aglobal: ident -> int -> addressing (**r Address is [symbol + offset] *) - | Abased: ident -> int -> addressing (**r Address is [symbol + offset + r1] *) - | Ainstack: int -> addressing. (**r Address is [stack_pointer + offset] *) + | Aglobal: ident -> ptrofs -> addressing (**r Address is [symbol + offset] *) + | Abased: ident -> ptrofs -> addressing (**r Address is [symbol + offset + r1] *) + | Ainstack: ptrofs -> addressing. (**r Address is [stack_pointer + offset] *) (** Comparison functions (used in module [CSE]). *) @@ -140,17 +141,15 @@ Defined. Definition eq_operation (x y: operation): {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. + generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intro. generalize Float.eq_dec Float32.eq_dec; intros. - assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. generalize eq_condition; intro. decide equality. Defined. Definition eq_addressing (x y: addressing) : {x=y} + {x<>y}. Proof. - generalize Int.eq_dec; intro. - assert (forall (x y: ident), {x=y}+{x<>y}). exact peq. + generalize Int.eq_dec Ptrofs.eq_dec ident_eq; intro. decide equality. Defined. @@ -185,7 +184,7 @@ Definition eval_operation | Ofloatconst n, nil => Some (Vfloat n) | Osingleconst n, nil => Some (Vsingle n) | Oaddrsymbol s ofs, nil => Some (Genv.symbol_address genv s ofs) - | Oaddrstack ofs, nil => Some (Val.add sp (Vint ofs)) + | Oaddrstack ofs, nil => Some (Val.offset_ptr sp ofs) | Ocast8signed, v1::nil => Some (Val.sign_ext 8 v1) | Ocast16signed, v1::nil => Some (Val.sign_ext 16 v1) | Oadd, v1::v2::nil => Some (Val.add v1 v2) @@ -253,10 +252,24 @@ Definition eval_addressing | Aindexed2, v1::v2::nil => Some (Val.add v1 v2) | Aglobal s ofs, nil => Some (Genv.symbol_address genv s ofs) | Abased s ofs, v1::nil => Some (Val.add (Genv.symbol_address genv s ofs) v1) - | Ainstack ofs, nil => Some(Val.add sp (Vint ofs)) + | Ainstack ofs, nil => Some(Val.offset_ptr sp ofs) | _, _ => None end. +Remark eval_addressing_Ainstack: + forall (F V: Type) (genv: Genv.t F V) sp ofs, + eval_addressing genv sp (Ainstack ofs) nil = Some (Val.offset_ptr sp ofs). +Proof. + intros. reflexivity. +Qed. + +Remark eval_addressing_Ainstack_inv: + forall (F V: Type) (genv: Genv.t F V) sp ofs vl v, + eval_addressing genv sp (Ainstack ofs) vl = Some v -> vl = nil /\ v = Val.offset_ptr sp ofs. +Proof. + unfold eval_addressing; intros; destruct vl; inv H; auto. +Qed. + Ltac FuncInv := match goal with | H: (match ?x with nil => _ | _ :: _ => _ end = Some _) |- _ => @@ -371,7 +384,7 @@ Lemma type_of_operation_sound: op <> Omove -> eval_operation genv sp op vl m = Some v -> Val.has_type v (snd (type_of_operation op)). -Proof with (try exact I). +Proof with (try exact I; try reflexivity). intros. destruct op; simpl in H0; FuncInv; subst; simpl. congruence. @@ -496,15 +509,15 @@ Qed. (** Shifting stack-relative references. This is used in [Stacking]. *) -Definition shift_stack_addressing (delta: int) (addr: addressing) := +Definition shift_stack_addressing (delta: Z) (addr: addressing) := match addr with - | Ainstack ofs => Ainstack (Int.add delta ofs) + | Ainstack ofs => Ainstack (Ptrofs.add (Ptrofs.repr delta) ofs) | _ => addr end. -Definition shift_stack_operation (delta: int) (op: operation) := +Definition shift_stack_operation (delta: Z) (op: operation) := match op with - | Oaddrstack ofs => Oaddrstack (Int.add delta ofs) + | Oaddrstack ofs => Oaddrstack (Ptrofs.add (Ptrofs.repr delta) ofs) | _ => op end. @@ -522,47 +535,50 @@ Qed. Lemma eval_shift_stack_addressing: forall F V (ge: Genv.t F V) sp addr vl delta, - eval_addressing ge sp (shift_stack_addressing delta addr) vl = - eval_addressing ge (Val.add sp (Vint delta)) addr vl. + eval_addressing ge (Vptr sp Ptrofs.zero) (shift_stack_addressing delta addr) vl = + eval_addressing ge (Vptr sp (Ptrofs.repr delta)) addr vl. Proof. intros. destruct addr; simpl; auto. - rewrite Val.add_assoc. simpl. auto. + rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_shift_stack_operation: forall F V (ge: Genv.t F V) sp op vl m delta, - eval_operation ge sp (shift_stack_operation delta op) vl m = - eval_operation ge (Val.add sp (Vint delta)) op vl m. + eval_operation ge (Vptr sp Ptrofs.zero) (shift_stack_operation delta op) vl m = + eval_operation ge (Vptr sp (Ptrofs.repr delta)) op vl m. Proof. intros. destruct op; simpl; auto. - rewrite Val.add_assoc. simpl. auto. + rewrite Ptrofs.add_zero_l; auto. Qed. (** Offset an addressing mode [addr] by a quantity [delta], so that it designates the pointer [delta] bytes past the pointer designated by [addr]. May be undefined, in which case [None] is returned. *) -Definition offset_addressing (addr: addressing) (delta: int) : option addressing := +Definition offset_addressing (addr: addressing) (delta: Z) : option addressing := match addr with - | Aindexed n => Some(Aindexed (Int.add n delta)) + | Aindexed n => Some(Aindexed (Int.add n (Int.repr delta))) | Aindexed2 => None - | Aglobal s n => Some(Aglobal s (Int.add n delta)) - | Abased s n => Some(Abased s (Int.add n delta)) - | Ainstack n => Some(Ainstack (Int.add n delta)) + | Aglobal s n => Some(Aglobal s (Ptrofs.add n (Ptrofs.repr delta))) + | Abased s n => Some(Abased s (Ptrofs.add n (Ptrofs.repr delta))) + | Ainstack n => Some(Ainstack (Ptrofs.add n (Ptrofs.repr delta))) end. Lemma eval_offset_addressing: forall (F V: Type) (ge: Genv.t F V) sp addr args delta addr' v, offset_addressing addr delta = Some addr' -> eval_addressing ge sp addr args = Some v -> - eval_addressing ge sp addr' args = Some(Val.add v (Vint delta)). + eval_addressing ge sp addr' args = Some(Val.add v (Vint (Int.repr delta))). Proof. - intros. destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. - rewrite Val.add_assoc; auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. - rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. auto. - rewrite Val.add_assoc. auto. + intros. + assert (D: Ptrofs.repr delta = Ptrofs.of_int (Int.repr delta)) by (symmetry; auto with ptrofs). + destruct addr; simpl in H; inv H; simpl in *; FuncInv; subst. +- rewrite Val.add_assoc; auto. +- unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. rewrite D; auto. +- unfold Genv.symbol_address. destruct (Genv.find_symbol ge i); auto. + rewrite Val.add_assoc. rewrite Val.add_permut. rewrite Val.add_commut. + simpl. rewrite D. auto. +- destruct sp; simpl; auto. rewrite Ptrofs.add_assoc, D. auto. Qed. (** Operations that are so cheap to recompute that CSE should not factor them out. *) @@ -662,30 +678,30 @@ Variable m2: mem. Hypothesis valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_inj: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Hypothesis weak_valid_pointer_no_overflow: forall b1 ofs b2 delta, f b1 = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Hypothesis valid_different_pointers_inj: forall b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> f b1 = Some (b1', delta1) -> f b2 = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned (Int.add ofs1 (Int.repr delta1)) <> Int.unsigned (Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned (Ptrofs.add ofs2 (Ptrofs.repr delta2)). Ltac InvInject := match goal with @@ -740,16 +756,13 @@ Lemma eval_operation_inj: Proof. intros until v1; intros GL; intros. destruct op; simpl in H1; simpl; FuncInv; InvInject; TrivialExists. apply GL; simpl; auto. - apply Values.Val.add_inject; auto. + apply Val.offset_ptr_inject; auto. inv H4; simpl; auto. inv H4; simpl; auto. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. - apply Values.Val.add_inject; auto. apply GL; simpl; auto. - inv H4; inv H2; simpl; auto. econstructor; eauto. - rewrite Int.sub_add_l. auto. - destruct (eq_block b1 b0); auto. subst. rewrite H1 in H0. inv H0. rewrite dec_eq_true. - rewrite Int.sub_shifted. auto. + apply Val.add_inject; auto. + apply Val.add_inject; auto. + apply Val.add_inject; auto. apply GL; simpl; auto. + apply Val.sub_inject; auto. inv H4; auto. inv H4; inv H2; simpl; auto. inv H4; simpl; auto. @@ -820,9 +833,9 @@ Lemma eval_addressing_inj: exists v2, eval_addressing ge2 sp2 addr vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. destruct addr; simpl in H2; simpl; FuncInv; InvInject; TrivialExists; - auto using Values.Val.add_inject. + auto using Val.add_inject, Val.offset_ptr_inject. apply H; simpl; auto. - apply Values.Val.add_inject; auto. apply H; simpl; auto. + apply Val.add_inject; auto. apply H; simpl; auto. Qed. End EVAL_COMPAT. @@ -838,40 +851,40 @@ Remark valid_pointer_extends: forall m1 m2, Mem.extends m1 m2 -> forall b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.valid_pointer_extends; eauto. + intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_extends: forall m1 m2, Mem.extends m1 m2 -> forall b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - Mem.weak_valid_pointer m2 b2 (Int.unsigned (Int.add ofs (Int.repr delta))) = true. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + Mem.weak_valid_pointer m2 b2 (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr delta))) = true. Proof. - intros. inv H0. rewrite Int.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. + intros. inv H0. rewrite Ptrofs.add_zero. eapply Mem.weak_valid_pointer_extends; eauto. Qed. Remark weak_valid_pointer_no_overflow_extends: forall m1 b1 ofs b2 delta, Some(b1, 0) = Some(b2, delta) -> - Mem.weak_valid_pointer m1 b1 (Int.unsigned ofs) = true -> - 0 <= Int.unsigned ofs + Int.unsigned (Int.repr delta) <= Int.max_unsigned. + Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true -> + 0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned. Proof. - intros. inv H. rewrite Zplus_0_r. apply Int.unsigned_range_2. + intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2. Qed. Remark valid_different_pointers_extends: forall m1 b1 ofs1 b2 ofs2 b1' delta1 b2' delta2, b1 <> b2 -> - Mem.valid_pointer m1 b1 (Int.unsigned ofs1) = true -> - Mem.valid_pointer m1 b2 (Int.unsigned ofs2) = true -> + Mem.valid_pointer m1 b1 (Ptrofs.unsigned ofs1) = true -> + Mem.valid_pointer m1 b2 (Ptrofs.unsigned ofs2) = true -> Some(b1, 0) = Some (b1', delta1) -> Some(b2, 0) = Some (b2', delta2) -> b1' <> b2' \/ - Int.unsigned(Int.add ofs1 (Int.repr delta1)) <> Int.unsigned(Int.add ofs2 (Int.repr delta2)). + Ptrofs.unsigned(Ptrofs.add ofs1 (Ptrofs.repr delta1)) <> Ptrofs.unsigned(Ptrofs.add ofs2 (Ptrofs.repr delta2)). Proof. intros. inv H2; inv H3. auto. Qed. @@ -950,7 +963,7 @@ Remark symbol_address_inject: Proof. intros. unfold Genv.symbol_address. destruct (Genv.find_symbol genv id) eqn:?; auto. exploit (proj1 globals); eauto. intros. - econstructor; eauto. rewrite Int.add_zero; auto. + econstructor; eauto. rewrite Ptrofs.add_zero; auto. Qed. Lemma eval_condition_inject: @@ -970,34 +983,36 @@ Qed. Lemma eval_addressing_inject: forall addr vl1 vl2 v1, Val.inject_list f vl1 vl2 -> - eval_addressing genv (Vptr sp1 Int.zero) addr vl1 = Some v1 -> + eval_addressing genv (Vptr sp1 Ptrofs.zero) addr vl1 = Some v1 -> exists v2, - eval_addressing genv (Vptr sp2 Int.zero) (shift_stack_addressing (Int.repr delta) addr) vl2 = Some v2 + eval_addressing genv (Vptr sp2 Ptrofs.zero) (shift_stack_addressing delta addr) vl2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. - rewrite eval_shift_stack_addressing. simpl. - eapply eval_addressing_inj with (sp1 := Vptr sp1 Int.zero); eauto. + rewrite eval_shift_stack_addressing. + eapply eval_addressing_inj with (sp1 := Vptr sp1 Ptrofs.zero); eauto. intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. Lemma eval_operation_inject: forall op vl1 vl2 v1 m1 m2, Val.inject_list f vl1 vl2 -> Mem.inject f m1 m2 -> - eval_operation genv (Vptr sp1 Int.zero) op vl1 m1 = Some v1 -> + eval_operation genv (Vptr sp1 Ptrofs.zero) op vl1 m1 = Some v1 -> exists v2, - eval_operation genv (Vptr sp2 Int.zero) (shift_stack_operation (Int.repr delta) op) vl2 m2 = Some v2 + eval_operation genv (Vptr sp2 Ptrofs.zero) (shift_stack_operation delta op) vl2 m2 = Some v2 /\ Val.inject f v1 v2. Proof. intros. rewrite eval_shift_stack_operation. simpl. - eapply eval_operation_inj with (sp1 := Vptr sp1 Int.zero) (m1 := m1); eauto. + eapply eval_operation_inj with (sp1 := Vptr sp1 Ptrofs.zero) (m1 := m1); eauto. intros; eapply Mem.valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_val; eauto. intros; eapply Mem.weak_valid_pointer_inject_no_overflow; eauto. intros; eapply Mem.different_pointers_inject; eauto. intros. apply symbol_address_inject. + econstructor; eauto. rewrite Ptrofs.add_zero_l; auto. Qed. End EVAL_INJECT. diff --git a/powerpc/SelectLong.vp b/powerpc/SelectLong.vp new file mode 100644 index 00000000..cc7a38f6 --- /dev/null +++ b/powerpc/SelectLong.vp @@ -0,0 +1,21 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for 64-bit integer operations *) + +Require Import Coqlib. +Require Import Compopts. +Require Import AST Integers Floats. +Require Import Op CminorSel. +Require Import SelectOp SplitLong. + +(** This file is empty because we use the default implementation provided in [SplitLong]. *) diff --git a/powerpc/SelectLongproof.v b/powerpc/SelectLongproof.v new file mode 100644 index 00000000..a82c082c --- /dev/null +++ b/powerpc/SelectLongproof.v @@ -0,0 +1,22 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Instruction selection for 64-bit integer operations *) + +Require Import String Coqlib Maps Integers Floats Errors. +Require Archi. +Require Import AST Values Memory Globalenvs Events. +Require Import Cminor Op CminorSel. +Require Import SelectOp SelectOpproof SplitLong SplitLongproof. +Require Import SelectLong. + +(** This file is empty because we use the default implementation provided in [SplitLong]. *) diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index a1fcecc7..79f05295 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -48,10 +48,10 @@ Open Local Scope cminorsel_scope. (** ** Constants **) -Definition addrsymbol (id: ident) (ofs: int) := +Definition addrsymbol (id: ident) (ofs: ptrofs) := Eop (Oaddrsymbol id ofs) Enil. -Definition addrstack (ofs: int) := +Definition addrstack (ofs: ptrofs) := Eop (Oaddrstack ofs) Enil. (** ** Integer logical negation *) @@ -78,17 +78,17 @@ Nondetfunction addimm (n: int) (e: expr) := if Int.eq n Int.zero then e else match e with | Eop (Ointconst m) Enil => Eop (Ointconst(Int.add n m)) Enil - | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Int.add n m)) Enil - | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Int.add n m)) Enil + | Eop (Oaddrsymbol s m) Enil => Eop (Oaddrsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) Enil + | Eop (Oaddrstack m) Enil => Eop (Oaddrstack (Ptrofs.add (Ptrofs.of_int n) m)) Enil | Eop (Oaddimm m) (t ::: Enil) => Eop (Oaddimm(Int.add n m)) (t ::: Enil) - | Eop (Oaddsymbol s m) (t ::: Enil) => Eop (Oaddsymbol s (Int.add n m)) (t ::: Enil) + | Eop (Oaddsymbol s m) (t ::: Enil) => Eop (Oaddsymbol s (Ptrofs.add (Ptrofs.of_int n) m)) (t ::: Enil) | _ => Eop (Oaddimm n) (e ::: Enil) end. -Nondetfunction addsymbol (s: ident) (ofs: int) (e: expr) := +Nondetfunction addsymbol (s: ident) (ofs: ptrofs) (e: expr) := match e with - | Eop (Ointconst n) Enil => Eop (Oaddrsymbol s (Int.add ofs n)) Enil - | Eop (Oaddimm n) (t ::: Enil) => Eop (Oaddsymbol s (Int.add ofs n)) (t ::: Enil) + | Eop (Ointconst n) Enil => Eop (Oaddrsymbol s (Ptrofs.add ofs (Ptrofs.of_int n))) Enil + | Eop (Oaddimm n) (t ::: Enil) => Eop (Oaddsymbol s (Ptrofs.add ofs (Ptrofs.of_int n))) (t ::: Enil) | _ => Eop (Oaddsymbol s ofs) (e ::: Enil) end. @@ -107,9 +107,9 @@ Nondetfunction add (e1: expr) (e2: expr) := | Eop (Oaddimm n1) (t1:::Enil), t2 => addimm n1 (Eop Oadd (t1:::t2:::Enil)) | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => - Eop Oadd (Eop (Oaddrstack (Int.add n1 n2)) Enil ::: t2 ::: Enil) + Eop Oadd (Eop (Oaddrstack (Ptrofs.add n1 (Ptrofs.of_int n2))) Enil ::: t2 ::: Enil) | Eop (Oaddsymbol s ofs) (t1:::Enil), Eop (Oaddimm n) (t2:::Enil) => - addsymbol s (Int.add ofs n) (Eop Oadd (t1:::t2:::Enil)) + addsymbol s (Ptrofs.add ofs (Ptrofs.of_int n)) (Eop Oadd (t1:::t2:::Enil)) | Eop (Oaddsymbol s ofs) (t1:::Enil), t2 => addsymbol s ofs (Eop Oadd (t1:::t2:::Enil)) | t1, Eop (Oaddimm n2) (t2:::Enil) => diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index f93b93e5..e31e847a 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -27,6 +27,7 @@ Require Import CminorSel. Require Import SelectOp. Open Local Scope cminorsel_scope. +Local Transparent Archi.ptr64. (** * Useful lemmas and tactics *) @@ -124,7 +125,7 @@ Qed. Theorem eval_addrstack: forall le ofs, - exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.add sp (Vint ofs)) v. + exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.offset_ptr sp ofs) v. Proof. intros. unfold addrstack. econstructor; split. EvalOp. simpl; eauto. @@ -154,19 +155,26 @@ Proof. TrivialExists. Qed. +Remark shift_symbol_address: + forall id ofs delta, + Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.of_int delta)) = Val.add (Genv.symbol_address ge id ofs) (Vint delta). +Proof. + intros. unfold Genv.symbol_address. destruct (Genv.find_symbol ge id); auto. +Qed. + Theorem eval_addimm: forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). Proof. red; unfold addimm; intros until x. predSpec Int.eq Int.eq_spec n Int.zero. subst n. intros. exists x; split; auto. - destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto. + destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Ptrofs.add_zero. auto. case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl. rewrite Int.add_commut. auto. - unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto. - rewrite Val.add_assoc. rewrite Int.add_commut. auto. + unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Ptrofs.add_commut; auto. + destruct sp; simpl; auto. rewrite Ptrofs.add_assoc. do 3 f_equal. apply Ptrofs.add_commut. subst. rewrite Val.add_assoc. rewrite Int.add_commut. auto. - subst. rewrite Int.add_commut. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut. + subst. rewrite Ptrofs.add_commut. rewrite shift_symbol_address. rewrite ! Val.add_assoc. f_equal. f_equal. apply Val.add_commut. Qed. Theorem eval_addsymbol: @@ -174,8 +182,8 @@ Theorem eval_addsymbol: Proof. red; unfold addsymbol; intros until x. case (addsymbol_match a); intros; InvEval; simpl; TrivialExists; simpl. - rewrite Genv.shift_symbol_address. auto. - rewrite Genv.shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal. + rewrite shift_symbol_address. auto. + rewrite shift_symbol_address. subst x. rewrite Val.add_assoc. f_equal. f_equal. apply Val.add_commut. Qed. @@ -199,12 +207,12 @@ Proof. repeat rewrite Val.add_assoc. decEq. apply Val.add_commut. - subst. TrivialExists. econstructor. EvalOp. simpl. reflexivity. econstructor. eauto. constructor. - simpl. repeat rewrite Val.add_assoc. decEq; decEq. - rewrite Val.add_commut. rewrite Val.add_permut. auto. + simpl. rewrite Val.add_permut, Val.add_commut. do 2 f_equal. + destruct sp; simpl; auto. rewrite Ptrofs.add_assoc; auto. - replace (Val.add x y) with - (Val.add (Genv.symbol_address ge s (Int.add ofs n)) (Val.add v1 v0)). + (Val.add (Genv.symbol_address ge s (Ptrofs.add ofs (Ptrofs.of_int n))) (Val.add v1 v0)). apply eval_addsymbol; auto. EvalOp. - subst. rewrite Genv.shift_symbol_address. rewrite ! Val.add_assoc. f_equal. + subst. rewrite shift_symbol_address. rewrite ! Val.add_assoc. f_equal. rewrite Val.add_permut. f_equal. apply Val.add_commut. - subst. rewrite Val.add_assoc. apply eval_addsymbol. EvalOp. - subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. @@ -1000,9 +1008,9 @@ Proof. exists (v1 :: v0 :: nil). split. eauto with evalexpr. simpl. congruence. exists (Vptr b ofs :: nil). split. constructor. EvalOp. simpl; congruence. constructor. - simpl. rewrite Int.add_zero. auto. + simpl. rewrite Ptrofs.add_zero. auto. exists (v :: nil). split. eauto with evalexpr. subst v. simpl. - rewrite Int.add_zero. auto. + rewrite Ptrofs.add_zero. auto. Qed. Theorem eval_builtin_arg: diff --git a/powerpc/ValueAOp.v b/powerpc/ValueAOp.v index fe5a0792..8081f557 100644 --- a/powerpc/ValueAOp.v +++ b/powerpc/ValueAOp.v @@ -156,18 +156,18 @@ Ltac InvHyps := Theorem eval_static_addressing_sound: forall addr vargs vres aargs, - eval_addressing ge (Vptr sp Int.zero) addr vargs = Some vres -> + eval_addressing ge (Vptr sp Ptrofs.zero) addr vargs = Some vres -> list_forall2 (vmatch bc) vargs aargs -> vmatch bc vres (eval_static_addressing addr aargs). Proof. unfold eval_addressing, eval_static_addressing; intros; destruct addr; InvHyps; eauto with va. - rewrite Int.add_zero_l; auto with va. + rewrite Ptrofs.add_zero_l; auto with va. Qed. Theorem eval_static_operation_sound: forall op vargs m vres aargs, - eval_operation ge (Vptr sp Int.zero) op vargs m = Some vres -> + eval_operation ge (Vptr sp Ptrofs.zero) op vargs m = Some vres -> list_forall2 (vmatch bc) vargs aargs -> vmatch bc vres (eval_static_operation op aargs). Proof. @@ -175,7 +175,7 @@ Proof. destruct op; InvHyps; eauto with va. destruct (propagate_float_constants tt); constructor. destruct (propagate_float_constants tt); constructor. - rewrite Int.add_zero_l; eauto with va. + rewrite Ptrofs.add_zero_l; eauto with va. fold (Val.sub (Vint i) a1). auto with va. apply floatofwords_sound; auto. apply of_optbool_sound. eapply eval_static_condition_sound; eauto. |