Library Asmgenproof1
Correctness proof for PPC generation: auxiliary results.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Mem.
Require Import Globalenvs.
Require Import Op.
Require Import Locations.
Require Import Mach.
Require Import Machconcr.
Require Import Machtyping.
Require Import Asm.
Require Import Asmgen.
Require Conventions.
Lemma high_half_zero:
forall v, Val.add (high_half v) Vzero = high_half v.
Lemma low_high_u:
forall n, Int.or (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n.
Lemma low_high_u_xor:
forall n, Int.xor (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n.
Lemma low_high_s:
forall n, Int.add (Int.shl (high_s n) (Int.repr 16)) (low_s n) = n.
Hint Extern 2 (_ <> _) => discriminate: ppcgen.
Mapping from Mach registers to PPC registers.
Lemma preg_of_injective:
forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2.
Characterization of PPC registers that correspond to Mach registers.
Definition is_data_reg (r: preg) : Prop :=
match r with
| IR GPR12 => False
| FR FPR13 => False
| PC => False | LR => False | CTR => False
| CR0_0 => False | CR0_1 => False | CR0_2 => False | CR0_3 => False
| CARRY => False
| _ => True
end.
Lemma ireg_of_is_data_reg:
forall (r: mreg), is_data_reg (ireg_of r).
Lemma freg_of_is_data_reg:
forall (r: mreg), is_data_reg (ireg_of r).
Lemma preg_of_is_data_reg:
forall (r: mreg), is_data_reg (preg_of r).
Lemma ireg_of_not_GPR1:
forall r, ireg_of r <> GPR1.
Lemma ireg_of_not_GPR12:
forall r, ireg_of r <> GPR12.
Lemma freg_of_not_FPR13:
forall r, freg_of r <> FPR13.
Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR12 freg_of_not_FPR13: ppcgen.
Lemma preg_of_not:
forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2.
Hint Resolve preg_of_not: ppcgen.
Lemma preg_of_not_GPR1:
forall r, preg_of r <> GPR1.
Hint Resolve preg_of_not_GPR1: ppcgen.
Agreement between Mach register sets and PPC register sets.
Definition agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) :=
rs#GPR1 = sp /\ forall r: mreg, ms r = rs#(preg_of r).
Lemma preg_val:
forall ms sp rs r,
agree ms sp rs -> ms r = rs#(preg_of r).
Lemma ireg_val:
forall ms sp rs r,
agree ms sp rs ->
mreg_type r = Tint ->
ms r = rs#(ireg_of r).
Lemma freg_val:
forall ms sp rs r,
agree ms sp rs ->
mreg_type r = Tfloat ->
ms r = rs#(freg_of r).
Lemma sp_val:
forall ms sp rs,
agree ms sp rs ->
sp = rs#GPR1.
Lemma agree_exten_1:
forall ms sp rs rs',
agree ms sp rs ->
(forall r, is_data_reg r -> rs'#r = rs#r) ->
agree ms sp rs'.
Lemma agree_exten_2:
forall ms sp rs rs',
agree ms sp rs ->
(forall r,
r <> IR GPR12 -> r <> FR FPR13 ->
r <> PC -> r <> LR -> r <> CTR ->
r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 ->
r <> CARRY ->
rs'#r = rs#r) ->
agree ms sp rs'.
Preservation of register agreement under various assignments.
Lemma agree_set_mreg:
forall ms sp rs r v,
agree ms sp rs ->
agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v).
Hint Resolve agree_set_mreg: ppcgen.
Lemma agree_set_mireg:
forall ms sp rs r v,
agree ms sp (rs#(preg_of r) <- v) ->
mreg_type r = Tint ->
agree ms sp (rs#(ireg_of r) <- v).
Hint Resolve agree_set_mireg: ppcgen.
Lemma agree_set_mfreg:
forall ms sp rs r v,
agree ms sp (rs#(preg_of r) <- v) ->
mreg_type r = Tfloat ->
agree ms sp (rs#(freg_of r) <- v).
Hint Resolve agree_set_mfreg: ppcgen.
Lemma agree_set_other:
forall ms sp rs r v,
agree ms sp rs ->
~(is_data_reg r) ->
agree ms sp (rs#r <- v).
Hint Resolve agree_set_other: ppcgen.
Lemma agree_nextinstr:
forall ms sp rs,
agree ms sp rs -> agree ms sp (nextinstr rs).
Hint Resolve agree_nextinstr: ppcgen.
Lemma agree_set_mireg_twice:
forall ms sp rs r v v',
agree ms sp rs ->
mreg_type r = Tint ->
agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v).
Hint Resolve agree_set_mireg_twice: ppcgen.
Lemma agree_set_twice_mireg:
forall ms sp rs r v v',
agree (Regmap.set r v' ms) sp rs ->
mreg_type r = Tint ->
agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v).
Hint Resolve agree_set_twice_mireg: ppcgen.
Lemma agree_set_commut:
forall ms sp rs r1 r2 v1 v2,
r1 <> r2 ->
agree ms sp ((rs#r2 <- v2)#r1 <- v1) ->
agree ms sp ((rs#r1 <- v1)#r2 <- v2).
Hint Resolve agree_set_commut: ppcgen.
Lemma agree_nextinstr_commut:
forall ms sp rs r v,
agree ms sp (rs#r <- v) ->
r <> PC ->
agree ms sp ((nextinstr rs)#r <- v).
Hint Resolve agree_nextinstr_commut: ppcgen.
Lemma agree_set_mireg_exten:
forall ms sp rs r v (rs': regset),
agree ms sp rs ->
mreg_type r = Tint ->
rs'#(ireg_of r) = v ->
(forall r',
r' <> IR GPR12 -> r' <> FR FPR13 ->
r' <> PC -> r' <> LR -> r' <> CTR ->
r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 ->
r' <> CARRY ->
r' <> IR (ireg_of r) -> rs'#r' = rs#r') ->
agree (Regmap.set r v ms) sp rs'.
Useful properties of the PC and GPR0 registers.
Lemma nextinstr_inv:
forall r rs, r <> PC -> (nextinstr rs)#r = rs#r.
Hint Resolve nextinstr_inv: ppcgen.
Lemma nextinstr_set_preg:
forall rs m v,
(nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone.
Hint Resolve nextinstr_set_preg: ppcgen.
Lemma gpr_or_zero_not_zero:
forall rs r, r <> GPR0 -> gpr_or_zero rs r = rs#r.
Lemma gpr_or_zero_zero:
forall rs, gpr_or_zero rs GPR0 = Vzero.
Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen.
Connection between Mach and Asm calling conventions for external
functions.
Lemma extcall_arg_match:
forall ms sp rs m l v,
agree ms sp rs ->
Machconcr.extcall_arg ms m sp l v ->
Asm.extcall_arg rs m l v.
Lemma extcall_args_match:
forall ms sp rs m, agree ms sp rs ->
forall ll vl,
Machconcr.extcall_args ms m sp ll vl ->
Asm.extcall_args rs m ll vl.
Lemma extcall_arguments_match:
forall ms m sp rs sg args,
agree ms sp rs ->
Machconcr.extcall_arguments ms m sp sg args ->
Asm.extcall_arguments rs m sg args.
Section STRAIGHTLINE.
Variable ge: genv.
Variable fn: code.
Straight-line code is composed of PPC instructions that execute
in sequence (no branches, no function calls and returns).
The following inductive predicate relates the machine states
before and after executing a straight-line sequence of instructions.
Instructions are taken from the first list instead of being fetched
from memory.
Inductive exec_straight: code -> regset -> mem ->
code -> regset -> mem -> Prop :=
| exec_straight_one:
forall i1 c rs1 m1 rs2 m2,
exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
rs2#PC = Val.add rs1#PC Vone ->
exec_straight (i1 :: c) rs1 m1 c rs2 m2
| exec_straight_step:
forall i c rs1 m1 rs2 m2 c' rs3 m3,
exec_instr ge fn i rs1 m1 = OK rs2 m2 ->
rs2#PC = Val.add rs1#PC Vone ->
exec_straight c rs2 m2 c' rs3 m3 ->
exec_straight (i :: c) rs1 m1 c' rs3 m3.
Lemma exec_straight_trans:
forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3,
exec_straight c1 rs1 m1 c2 rs2 m2 ->
exec_straight c2 rs2 m2 c3 rs3 m3 ->
exec_straight c1 rs1 m1 c3 rs3 m3.
Lemma exec_straight_two:
forall i1 i2 c rs1 m1 rs2 m2 rs3 m3,
exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
rs2#PC = Val.add rs1#PC Vone ->
rs3#PC = Val.add rs2#PC Vone ->
exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3.
Lemma exec_straight_three:
forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4,
exec_instr ge fn i1 rs1 m1 = OK rs2 m2 ->
exec_instr ge fn i2 rs2 m2 = OK rs3 m3 ->
exec_instr ge fn i3 rs3 m3 = OK rs4 m4 ->
rs2#PC = Val.add rs1#PC Vone ->
rs3#PC = Val.add rs2#PC Vone ->
rs4#PC = Val.add rs3#PC Vone ->
exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4.
Properties of comparisons.
Lemma compare_float_spec:
forall rs v1 v2,
let rs1 := nextinstr (compare_float rs v1 v2) in
rs1#CR0_0 = Val.cmpf Clt v1 v2
/\ rs1#CR0_1 = Val.cmpf Cgt v1 v2
/\ rs1#CR0_2 = Val.cmpf Ceq v1 v2
/\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
Lemma compare_sint_spec:
forall rs v1 v2,
let rs1 := nextinstr (compare_sint rs v1 v2) in
rs1#CR0_0 = Val.cmp Clt v1 v2
/\ rs1#CR0_1 = Val.cmp Cgt v1 v2
/\ rs1#CR0_2 = Val.cmp Ceq v1 v2
/\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
Lemma compare_uint_spec:
forall rs v1 v2,
let rs1 := nextinstr (compare_uint rs v1 v2) in
rs1#CR0_0 = Val.cmpu Clt v1 v2
/\ rs1#CR0_1 = Val.cmpu Cgt v1 v2
/\ rs1#CR0_2 = Val.cmpu Ceq v1 v2
/\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'.
Loading a constant.
Lemma loadimm_correct:
forall r n k rs m,
exists rs',
exec_straight (loadimm r n k) rs m k rs' m
/\ rs'#r = Vint n
/\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'.
Add integer immediate.
Lemma addimm_1_correct:
forall r1 r2 n k rs m,
r1 <> GPR0 ->
r2 <> GPR0 ->
exists rs',
exec_straight (addimm_1 r1 r2 n k) rs m k rs' m
/\ rs'#r1 = Val.add rs#r2 (Vint n)
/\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
Lemma addimm_2_correct:
forall r1 r2 n k rs m,
r2 <> GPR12 ->
exists rs',
exec_straight (addimm_2 r1 r2 n k) rs m k rs' m
/\ rs'#r1 = Val.add rs#r2 (Vint n)
/\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'.
Lemma addimm_correct:
forall r1 r2 n k rs m,
r2 <> GPR12 ->
exists rs',
exec_straight (addimm r1 r2 n k) rs m k rs' m
/\ rs'#r1 = Val.add rs#r2 (Vint n)
/\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'.
And integer immediate.
Lemma andimm_correct:
forall r1 r2 n k (rs : regset) m,
r2 <> GPR12 ->
let v := Val.and rs#r2 (Vint n) in
exists rs',
exec_straight (andimm r1 r2 n k) rs m k rs' m
/\ rs'#r1 = v
/\ rs'#CR0_2 = Val.cmp Ceq v Vzero
/\ forall r': preg,
r' <> r1 -> r' <> GPR12 -> r' <> PC ->
r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 ->
rs'#r' = rs#r'.
Or integer immediate.
Lemma orimm_correct:
forall r1 (r2: ireg) n k (rs : regset) m,
let v := Val.or rs#r2 (Vint n) in
exists rs',
exec_straight (orimm r1 r2 n k) rs m k rs' m
/\ rs'#r1 = v
/\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
Xor integer immediate.
Lemma xorimm_correct:
forall r1 (r2: ireg) n k (rs : regset) m,
let v := Val.xor rs#r2 (Vint n) in
exists rs',
exec_straight (xorimm r1 r2 n k) rs m k rs' m
/\ rs'#r1 = v
/\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'.
Indexed memory loads.
Lemma loadind_aux_correct:
forall (base: ireg) ofs ty dst (rs: regset) m v,
Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
mreg_type dst = ty ->
base <> GPR0 ->
exec_instr ge fn (loadind_aux base ofs ty dst) rs m =
OK (nextinstr (rs#(preg_of dst) <- v)) m.
Lemma loadind_correct:
forall (base: ireg) ofs ty dst k (rs: regset) m v,
Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v ->
mreg_type dst = ty ->
base <> GPR0 ->
exists rs',
exec_straight (loadind base ofs ty dst k) rs m k rs' m
/\ rs'#(preg_of dst) = v
/\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs'#r = rs#r.
Indexed memory stores.
Lemma storeind_aux_correct:
forall (base: ireg) ofs ty src (rs: regset) m m',
Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
mreg_type src = ty ->
base <> GPR0 ->
exec_instr ge fn (storeind_aux src base ofs ty) rs m =
OK (nextinstr rs) m'.
Lemma storeind_correct:
forall (base: ireg) ofs ty src k (rs: regset) m m',
Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' ->
mreg_type src = ty ->
base <> GPR0 ->
exists rs',
exec_straight (storeind src base ofs ty k) rs m k rs' m'
/\ forall r, r <> PC -> r <> GPR12 -> rs'#r = rs#r.
Float comparisons.
Lemma floatcomp_correct:
forall cmp (r1 r2: freg) k rs m,
exists rs',
exec_straight (floatcomp cmp r1 r2 k) rs m k rs' m
/\ rs'#(reg_of_crbit (fst (crbit_for_fcmp cmp))) =
(if snd (crbit_for_fcmp cmp)
then Val.cmpf cmp rs#r1 rs#r2
else Val.notbool (Val.cmpf cmp rs#r1 rs#r2))
/\ forall r',
r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 ->
r' <> CR0_2 -> r' <> CR0_3 -> rs'#r' = rs#r'.
Ltac TypeInv :=
match goal with
| H: (List.map ?f ?x = nil) |- _ =>
destruct x; [clear H | simpl in H; discriminate]
| H: (List.map ?f ?x = ?hd :: ?tl) |- _ =>
destruct x; simpl in H;
[ discriminate |
injection H; clear H; let T := fresh "T" in (
intros H T; TypeInv) ]
| _ => idtac
end.
Translation of conditions.
Lemma transl_cond_correct_aux:
forall cond args k ms sp rs m,
map mreg_type args = type_of_condition cond ->
agree ms sp rs ->
exists rs',
exec_straight (transl_cond cond args k) rs m k rs' m
/\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) =
(if snd (crbit_for_cond cond)
then eval_condition_total cond (map ms args)
else Val.notbool (eval_condition_total cond (map ms args)))
/\ agree ms sp rs'.
Lemma transl_cond_correct:
forall cond args k ms sp rs m b,
map mreg_type args = type_of_condition cond ->
agree ms sp rs ->
eval_condition cond (map ms args) = Some b ->
exists rs',
exec_straight (transl_cond cond args k) rs m k rs' m
/\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) =
(if snd (crbit_for_cond cond)
then Val.of_bool b
else Val.notbool (Val.of_bool b))
/\ agree ms sp rs'.
Translation of arithmetic operations.
Ltac TranslOpSimpl :=
match goal with
| |- exists rs' : regset,
exec_straight ?c ?rs ?m ?k rs' ?m /\
agree (Regmap.set ?res ?v ?ms) ?sp rs' =>
(exists (nextinstr (rs#(ireg_of res) <- v));
split;
[ apply exec_straight_one;
[ repeat (rewrite (ireg_val ms sp rs); auto); reflexivity
| reflexivity ]
| auto with ppcgen ])
||
(exists (nextinstr (rs#(freg_of res) <- v));
split;
[ apply exec_straight_one;
[ repeat (rewrite (freg_val ms sp rs); auto); reflexivity
| reflexivity ]
| auto with ppcgen ])
end.
Lemma transl_op_correct:
forall op args res k ms sp rs m v,
wt_instr (Mop op args res) ->
agree ms sp rs ->
eval_operation ge sp op (map ms args) = Some v ->
exists rs',
exec_straight (transl_op op args res k) rs m k rs' m
/\ agree (Regmap.set res v ms) sp rs'.
Lemma transl_load_store_correct:
forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
addr args k ms sp rs m ms' m',
(forall cst (r1: ireg) (rs1: regset) k,
eval_addressing_total ge sp addr (map ms args) =
Val.add (gpr_or_zero rs1 r1) (const_low ge cst) ->
agree ms sp rs1 ->
exists rs',
exec_straight (mk1 cst r1 :: k) rs1 m k rs' m' /\
agree ms' sp rs') ->
(forall (r1 r2: ireg) (rs1: regset) k,
eval_addressing_total ge sp addr (map ms args) = Val.add rs1#r1 rs1#r2 ->
agree ms sp rs1 ->
exists rs',
exec_straight (mk2 r1 r2 :: k) rs1 m k rs' m' /\
agree ms' sp rs') ->
agree ms sp rs ->
map mreg_type args = type_of_addressing addr ->
exists rs',
exec_straight (transl_load_store mk1 mk2 addr args k) rs m
k rs' m'
/\ agree ms' sp rs'.
Translation of memory loads.
Lemma transl_load_correct:
forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
chunk addr args k ms sp rs m dst a v,
(forall cst (r1: ireg) (rs1: regset),
exec_instr ge fn (mk1 cst r1) rs1 m =
load1 ge chunk (preg_of dst) cst r1 rs1 m) ->
(forall (r1 r2: ireg) (rs1: regset),
exec_instr ge fn (mk2 r1 r2) rs1 m =
load2 chunk (preg_of dst) r1 r2 rs1 m) ->
agree ms sp rs ->
map mreg_type args = type_of_addressing addr ->
eval_addressing ge sp addr (map ms args) = Some a ->
Mem.loadv chunk m a = Some v ->
exists rs',
exec_straight (transl_load_store mk1 mk2 addr args k) rs m
k rs' m
/\ agree (Regmap.set dst v ms) sp rs'.
Translation of memory stores.
Lemma transl_store_correct:
forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction)
chunk addr args k ms sp rs m src a m',
(forall cst (r1: ireg) (rs1: regset),
exists rs2,
exec_instr ge fn (mk1 cst r1) rs1 m =
store1 ge chunk (preg_of src) cst r1 rs2 m
/\ (forall (r: preg), r <> FPR13 -> rs2 r = rs1 r)) ->
(forall (r1 r2: ireg) (rs1: regset),
exists rs2,
exec_instr ge fn (mk2 r1 r2) rs1 m =
store2 chunk (preg_of src) r1 r2 rs2 m
/\ (forall (r: preg), r <> FPR13 -> rs2 r = rs1 r)) ->
agree ms sp rs ->
map mreg_type args = type_of_addressing addr ->
eval_addressing ge sp addr (map ms args) = Some a ->
Mem.storev chunk m a (ms src) = Some m' ->
exists rs',
exec_straight (transl_load_store mk1 mk2 addr args k) rs m
k rs' m'
/\ agree ms sp rs'.
End STRAIGHTLINE.