summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checklink/Asm_printers.ml8
-rw-r--r--checklink/Check.ml12
-rw-r--r--ia32/Asm.v55
-rw-r--r--ia32/Asmgen.v21
-rw-r--r--ia32/Asmgenproof.v34
-rw-r--r--ia32/Asmgenproof1.v2
-rw-r--r--ia32/PrintAsm.ml12
-rw-r--r--ia32/Unusedglob1.ml6
-rw-r--r--powerpc/Asm.v53
-rw-r--r--powerpc/Asmgen.v25
-rw-r--r--powerpc/Asmgenproof.v36
-rw-r--r--powerpc/Asmgenproof1.v2
-rw-r--r--powerpc/PrintAsm.ml15
-rw-r--r--powerpc/Unusedglob1.ml6
14 files changed, 146 insertions, 141 deletions
diff --git a/checklink/Asm_printers.ml b/checklink/Asm_printers.ml
index 5b3abe8..c84bd55 100644
--- a/checklink/Asm_printers.ml
+++ b/checklink/Asm_printers.ml
@@ -137,11 +137,11 @@ let string_of_instruction = function
| Pandi_ (i0, i1, c2) -> "Pandi_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")"
| Pandis_ (i0, i1, c2) -> "Pandis_(" ^ string_of_ireg i0 ^ ", " ^ string_of_ireg i1 ^ ", " ^ string_of_constant c2 ^ ")"
| Pb (l0) -> "Pb(" ^ string_of_label l0 ^ ")"
-| Pbctr -> "Pbctr"
-| Pbctrl -> "Pbctrl"
+| Pbctr sg -> "Pbctr"
+| Pbctrl sg -> "Pbctrl"
| Pbf (c0, l1) -> "Pbf(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")"
-| Pbl (i0) -> "Pbl(" ^ string_of_ident i0 ^ ")"
-| Pbs (i0) -> "Pbs(" ^ string_of_ident i0 ^ ")"
+| Pbl (i0, sg) -> "Pbl(" ^ string_of_ident i0 ^ ")"
+| Pbs (i0, sg) -> "Pbs(" ^ string_of_ident i0 ^ ")"
| Pblr -> "Pblr"
| Pbt (c0, l1) -> "Pbt(" ^ string_of_crbit c0 ^ ", " ^ string_of_label l1 ^ ")"
| Pbtbl (i0, l1) -> "Pbtbl(" ^ string_of_ireg i0 ^ ", " ^ string_of_list string_of_label ", " l1 ^ ")"
diff --git a/checklink/Check.ml b/checklink/Check.ml
index 50928d2..c51e090 100644
--- a/checklink/Check.ml
+++ b/checklink/Check.ml
@@ -38,7 +38,7 @@ let exhaustivity = ref true
let list_missing = ref false
(** CompCert Asm *)
-type ccode = Asm.instruction list
+type ccode = Asm.coq_function
let print_debug s =
if !debug then print_endline (string_of_log_entry true (DEBUG(s)))
@@ -1021,7 +1021,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
>>= recur_simpl
| _ -> error
end
- | Pbctr ->
+ | Pbctr sg ->
begin match ecode with
| BCCTRx(bo, bi, lk) :: es ->
OK(fw)
@@ -1031,7 +1031,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
>>= recur_simpl
| _ -> error
end
- | Pbctrl ->
+ | Pbctrl sg ->
begin match ecode with
| BCCTRx(bo, bi, lk) :: es ->
OK(fw)
@@ -1069,7 +1069,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
>>= compare_code cs es (Int32.add 8l pc)
| _ -> error
end
- | Pbl(ident) ->
+ | Pbl(ident, sg) ->
begin match ecode with
| Bx(li, aa, lk) :: es ->
let dest = Int32.(add pc (mul 4l (exts li))) in
@@ -1090,7 +1090,7 @@ let rec compare_code ccode ecode pc: checker = fun fw ->
>>= recur_simpl
| _ -> error
end
- | Pbs(ident) ->
+ | Pbs(ident, sg) ->
begin match ecode with
| Bx(li, aa, lk) :: es ->
let dest = Int32.(add pc (mul 4l (exts li))) in
@@ -2637,7 +2637,7 @@ let rec worklist_process (wl: worklist) sfw: s_framework =
label_list = [];
}
)
- >>> compare_code ccode ecode pc
+ >>> compare_code ccode.fn_code ecode pc
>>^ mark_covered_fun_sym_ndx ndx
) in
begin match candidates with
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 78c4c3b..7bd1755 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -181,13 +181,13 @@ Inductive instruction: Type :=
| Pxorpd_f (rd: freg) (**r [xor] with self = set to zero *)
(** Branches and calls *)
| Pjmp_l (l: label)
- | Pjmp_s (symb: ident)
- | Pjmp_r (r: ireg)
+ | Pjmp_s (symb: ident) (sg: signature)
+ | Pjmp_r (r: ireg) (sg: signature)
| Pjcc (c: testcond)(l: label)
| Pjcc2 (c1 c2: testcond)(l: label) (**r pseudo *)
| Pjmptbl (r: ireg) (tbl: list label) (**r pseudo *)
- | Pcall_s (symb: ident)
- | Pcall_r (r: ireg)
+ | Pcall_s (symb: ident) (sg: signature)
+ | Pcall_r (r: ireg) (sg: signature)
| Pret
(** Pseudo-instructions *)
| Plabel(l: label)
@@ -201,9 +201,8 @@ with annot_param : Type :=
| APstack: memory_chunk -> Z -> annot_param.
Definition code := list instruction.
-Definition function := code.
-Definition fn_code (f: function) : code := f.
-Definition fundef := AST.fundef code.
+Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
+Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.
(** * Operational semantics *)
@@ -423,8 +422,8 @@ Definition nextinstr (rs: regset) :=
Definition nextinstr_nf (rs: regset) : regset :=
nextinstr (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil) rs).
-Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) :=
- match label_pos lbl 0 c with
+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
@@ -469,7 +468,7 @@ Definition exec_store (chunk: memory_chunk) (m: mem)
but we do not need to model this precisely.
*)
-Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome :=
+Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
match i with
(** Moves *)
| Pmov_rr rd r1 =>
@@ -627,20 +626,20 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
Next (nextinstr_nf (rs#rd <- (Vfloat Float.zero))) m
(** Branches and calls *)
| Pjmp_l lbl =>
- goto_label c lbl rs m
- | Pjmp_s id =>
+ goto_label f lbl rs m
+ | Pjmp_s id sg =>
Next (rs#PC <- (symbol_offset id Int.zero)) m
- | Pjmp_r r =>
+ | Pjmp_r r sg =>
Next (rs#PC <- (rs r)) m
| Pjcc cond lbl =>
match eval_testcond cond rs with
- | Some true => goto_label c lbl rs m
+ | Some true => goto_label f lbl rs m
| Some false => Next (nextinstr rs) m
| None => Stuck
end
| Pjcc2 cond1 cond2 lbl =>
match eval_testcond cond1 rs, eval_testcond cond2 rs with
- | Some true, Some true => goto_label c lbl rs m
+ | Some true, Some true => goto_label f lbl rs m
| Some _, Some _ => Next (nextinstr rs) m
| _, _ => Stuck
end
@@ -649,13 +648,13 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Vint n =>
match list_nth_z tbl (Int.unsigned n) with
| None => Stuck
- | Some lbl => goto_label c lbl rs m
+ | Some lbl => goto_label f lbl rs m
end
| _ => Stuck
end
- | Pcall_s id =>
+ | Pcall_s id sg =>
Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (symbol_offset id Int.zero)) m
- | Pcall_r r =>
+ | Pcall_r r sg =>
Next (rs#RA <- (Val.add rs#PC Vone) #PC <- (rs r)) m
| Pret =>
Next (rs#PC <- (rs#RA)) m
@@ -760,27 +759,27 @@ Inductive state: Type :=
Inductive step: state -> trace -> state -> Prop :=
| exec_step_internal:
- forall b ofs c i rs m rs' m',
+ forall b ofs f i rs m rs' m',
rs PC = Vptr b ofs ->
- Genv.find_funct_ptr ge b = Some (Internal c) ->
- find_instr (Int.unsigned ofs) c = Some i ->
- exec_instr c i rs m = Next rs' m' ->
+ Genv.find_funct_ptr ge b = Some (Internal f) ->
+ find_instr (Int.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 c ef args res rs m t vl rs' m',
+ forall b ofs f ef args res rs m t vl rs' m',
rs PC = Vptr b ofs ->
- Genv.find_funct_ptr ge b = Some (Internal c) ->
- find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) ->
+ Genv.find_funct_ptr ge b = Some (Internal f) ->
+ find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
external_call' ef ge (map rs args) m t vl m' ->
rs' = nextinstr_nf
(set_regs res vl
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
step (State rs m) t (State rs' m')
| exec_step_annot:
- forall b ofs c ef args rs m vargs t v m',
+ forall b ofs f ef args rs m vargs t v m',
rs PC = Vptr b ofs ->
- Genv.find_funct_ptr ge b = Some (Internal c) ->
- find_instr (Int.unsigned ofs) c = Some (Pannot ef args) ->
+ Genv.find_funct_ptr ge b = Some (Internal f) ->
+ find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) ->
annot_arguments rs m args vargs ->
external_call' ef ge vargs m t v m' ->
step (State rs m) t
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 0410057..740dff8 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -496,16 +496,16 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
| Mstore chunk addr args src =>
transl_store chunk addr args src k
| Mcall sig (inl reg) =>
- do r <- ireg_of reg; OK (Pcall_r r :: k)
+ do r <- ireg_of reg; OK (Pcall_r r sig :: k)
| Mcall sig (inr symb) =>
- OK (Pcall_s symb :: k)
+ OK (Pcall_s symb sig :: k)
| Mtailcall sig (inl reg) =>
do r <- ireg_of reg;
OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) ::
- Pjmp_r r :: k)
+ Pjmp_r r sig :: k)
| Mtailcall sig (inr symb) =>
OK (Pfreeframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) ::
- Pjmp_s symb :: k)
+ Pjmp_s symb sig :: k)
| Mlabel lbl =>
OK(Plabel lbl :: k)
| Mgoto lbl =>
@@ -563,11 +563,16 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo
otherwise the offset part of the [PC] code pointer could wrap
around, leading to incorrect executions. *)
-Definition transf_function (f: Mach.function) : res Asm.code :=
+Definition transl_function (f: Mach.function) :=
do c <- transl_code' f f.(Mach.fn_code) true;
- if zlt (list_length_z c) Int.max_unsigned
- then OK (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_ofs) :: c)
- else Error (msg "code size exceeded").
+ OK (mkfunction f.(Mach.fn_sig)
+ (Pallocframe f.(fn_stacksize) f.(fn_retaddr_ofs) f.(fn_link_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))
+ then Error (msg "code size exceeded")
+ else OK tf.
Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
transf_partial_fundef transf_function f.
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index df09ca7..fa8ce6c 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -77,10 +77,10 @@ Qed.
Lemma transf_function_no_overflow:
forall f tf,
- transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned.
+ transf_function f = OK tf -> list_length_z (fn_code tf) <= Int.max_unsigned.
Proof.
- intros. monadInv H. destruct (zlt (list_length_z x) Int.max_unsigned); monadInv EQ0.
- rewrite list_length_z_cons. omega.
+ intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); monadInv EQ0.
+ omega.
Qed.
Lemma exec_straight_exec:
@@ -299,12 +299,12 @@ Lemma transl_find_label:
forall lbl f tf,
transf_function f = OK tf ->
match Mach.find_label lbl f.(Mach.fn_code) with
- | None => find_label lbl tf = None
- | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc
+ | None => find_label lbl tf.(fn_code) = None
+ | 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 (list_length_z x) Int.max_unsigned); inv EQ0.
- simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ; eauto.
+ intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0.
+ monadInv EQ. simpl. eapply transl_code_label; eauto. rewrite transl_code'_transl_code in EQ0; eauto.
Qed.
End TRANSL_LABEL.
@@ -346,8 +346,8 @@ 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 (list_length_z x) Int.max_unsigned); inv EQ0.
- rewrite transl_code'_transl_code in EQ.
+ destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0.
+ monadInv EQ. rewrite transl_code'_transl_code in EQ0.
exists x; exists true; split; auto. unfold fn_code. repeat constructor.
- exact transf_function_no_overflow.
Qed.
@@ -583,7 +583,7 @@ Opaque loadind.
- (* Mcall *)
assert (f0 = f) by congruence. subst f0.
inv AT.
- assert (NOOV: list_length_z tf <= Int.max_unsigned).
+ assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned).
eapply transf_function_no_overflow; eauto.
destruct ros as [rf|fid]; simpl in H; monadInv H5.
+ (* Indirect call *)
@@ -623,7 +623,7 @@ Opaque loadind.
- (* Mtailcall *)
assert (f0 = f) by congruence. subst f0.
inv AT.
- assert (NOOV: list_length_z tf <= Int.max_unsigned).
+ assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned).
eapply transf_function_no_overflow; eauto.
rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *.
exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]].
@@ -820,7 +820,7 @@ Transparent destroyed_by_jumptable.
- (* Mreturn *)
assert (f0 = f) by congruence. subst f0.
inv AT.
- assert (NOOV: list_length_z tf <= Int.max_unsigned).
+ assert (NOOV: list_length_z tf.(fn_code) <= Int.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]].
@@ -844,8 +844,9 @@ Transparent destroyed_by_jumptable.
- (* internal function *)
exploit functions_translated; eauto. intros [tf [A B]]. monadInv B.
- generalize EQ; intros EQ'. monadInv EQ'. rewrite transl_code'_transl_code in EQ0.
- destruct (zlt (list_length_z x0) Int.max_unsigned); inversion EQ1. clear EQ1.
+ generalize EQ; intros EQ'. monadInv EQ'.
+ destruct (zlt Int.max_unsigned (list_length_z (fn_code x0))); inv EQ1.
+ monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
unfold store_stack in *.
exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
intros [m1' [C D]].
@@ -855,14 +856,13 @@ Transparent destroyed_by_jumptable.
intros [m3' [P Q]].
left; econstructor; split.
apply plus_one. econstructor; eauto.
- subst x; simpl.
- rewrite Int.unsigned_zero. simpl. eauto.
+ simpl. rewrite Int.unsigned_zero. simpl. eauto.
simpl. rewrite C. simpl in F. rewrite (sp_val _ _ _ AG) in F. rewrite F.
simpl in P. rewrite ATLR. rewrite P. eauto.
econstructor; eauto.
unfold nextinstr. rewrite Pregmap.gss. repeat rewrite Pregmap.gso; auto with asmgen.
rewrite ATPC. simpl. constructor; eauto.
- subst x. unfold fn_code. eapply code_tail_next_int. rewrite list_length_z_cons. omega.
+ unfold fn_code. eapply code_tail_next_int. simpl in g. omega.
constructor.
apply agree_nextinstr. eapply agree_change_sp; eauto.
Transparent destroyed_at_function_entry.
diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v
index 9ddc463..5d3df67 100644
--- a/ia32/Asmgenproof1.v
+++ b/ia32/Asmgenproof1.v
@@ -97,7 +97,7 @@ Ltac Simplifs := repeat Simplif.
Section CONSTRUCTORS.
Variable ge: genv.
-Variable fn: code.
+Variable fn: function.
(** Smart constructor for moves. *)
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 4480f91..3badbfc 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -681,9 +681,9 @@ let print_instruction oc = function
(** Branches and calls *)
| Pjmp_l(l) ->
fprintf oc " jmp %a\n" label (transl_label l)
- | Pjmp_s(f) ->
+ | Pjmp_s(f, sg) ->
fprintf oc " jmp %a\n" symbol f
- | Pjmp_r(r) ->
+ | Pjmp_r(r, sg) ->
fprintf oc " jmp *%a\n" ireg r
| Pjcc(c, l) ->
let l = transl_label l in
@@ -698,9 +698,9 @@ let print_instruction oc = function
let l = new_label() in
fprintf oc " jmp *%a(, %a, 4)\n" label l ireg r;
jumptables := (l, tbl) :: !jumptables
- | Pcall_s(f) ->
+ | Pcall_s(f, sg) ->
fprintf oc " call %a\n" symbol f
- | Pcall_r(r) ->
+ | Pcall_r(r, sg) ->
fprintf oc " call *%a\n" ireg r
| Pret ->
fprintf oc " ret\n"
@@ -758,7 +758,7 @@ let print_jumptable oc (lbl, tbl) =
(fun l -> fprintf oc " .long %a\n" label (transl_label l))
tbl
-let print_function oc name code =
+let print_function oc name fn =
Hashtbl.clear current_function_labels;
float_literals := [];
jumptables := [];
@@ -775,7 +775,7 @@ let print_function oc name code =
fprintf oc "%a:\n" symbol name;
print_location oc (C2C.atom_location name);
cfi_startproc oc;
- List.iter (print_instruction oc) code;
+ List.iter (print_instruction oc) fn.fn_code;
cfi_endproc oc;
if target = ELF then begin
fprintf oc " .type %a, @function\n" symbol name;
diff --git a/ia32/Unusedglob1.ml b/ia32/Unusedglob1.ml
index fe962e2..8332a30 100644
--- a/ia32/Unusedglob1.ml
+++ b/ia32/Unusedglob1.ml
@@ -35,10 +35,10 @@ let referenced_instr = function
| Pmovzb_rm (_, a) | Pmovsb_rm (_, a)
| Pmovzw_rm (_, a) | Pmovsw_rm (_, a)
| Pcvtss2sd_fm (_, a) | Pcvtsd2ss_mf (a, _) | Plea (_, a) -> referenced_addr a
- | Pjmp_s s -> [s]
- | Pcall_s s -> [s]
+ | Pjmp_s(s, _) -> [s]
+ | Pcall_s(s, _) -> [s]
| Pbuiltin(ef, args, res) -> referenced_builtin ef
| _ -> []
-let code_of_function f = f
+let code_of_function f = f.fn_code
diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 1441929..4499f01 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -145,11 +145,11 @@ Inductive instruction : Type :=
| Pandi_: ireg -> ireg -> constant -> instruction (**r and immediate and set conditions *)
| Pandis_: ireg -> ireg -> constant -> instruction (**r and immediate high and set conditions *)
| Pb: label -> instruction (**r unconditional branch *)
- | Pbctr: instruction (**r branch to contents of register CTR *)
- | Pbctrl: instruction (**r branch to contents of CTR and link *)
+ | Pbctr: signature -> instruction (**r branch to contents of register CTR *)
+ | Pbctrl: signature -> instruction (**r branch to contents of CTR and link *)
| Pbf: crbit -> label -> instruction (**r branch if false *)
- | Pbl: ident -> instruction (**r branch and link *)
- | Pbs: ident -> instruction (**r branch to symbol *)
+ | Pbl: ident -> signature -> instruction (**r branch and link *)
+ | Pbs: ident -> signature -> instruction (**r branch to symbol *)
| Pblr: instruction (**r branch to contents of register LR *)
| Pbt: crbit -> label -> instruction (**r branch if true *)
| Pbtbl: ireg -> list label -> instruction (**r N-way branch through a jump table *)
@@ -300,8 +300,7 @@ lbl: .long table[0], table[1], ...
*)
Definition code := list instruction.
-Definition function := code.
-Definition fn_code (f: function) : code := f.
+Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
Definition fundef := AST.fundef function.
Definition program := AST.program fundef unit.
@@ -470,8 +469,8 @@ Inductive outcome: Type :=
Definition nextinstr (rs: regset) :=
rs#PC <- (Val.add rs#PC Vone).
-Definition goto_label (c: code) (lbl: label) (rs: regset) (m: mem) :=
- match label_pos lbl 0 c with
+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
@@ -551,7 +550,7 @@ Definition compare_float (rs: regset) (v1 v2: val) :=
must survive the execution of the pseudo-instruction.
*)
-Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome :=
+Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : outcome :=
match i with
| Padd rd r1 r2 =>
Next (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m
@@ -587,25 +586,25 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
let v := Val.and rs#r1 (const_high cst) in
Next (nextinstr (compare_sint (rs#rd <- v) v Vzero)) m
| Pb lbl =>
- goto_label c lbl rs m
- | Pbctr =>
+ goto_label f lbl rs m
+ | Pbctr sg =>
Next (rs#PC <- (rs#CTR)) m
- | Pbctrl =>
+ | Pbctrl sg =>
Next (rs#LR <- (Val.add rs#PC Vone) #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 c lbl rs m else Next (nextinstr rs) m
+ | Vint n => if Int.eq n Int.zero then goto_label f lbl rs m else Next (nextinstr rs) m
| _ => Stuck
end
- | Pbl ident =>
+ | Pbl ident sg =>
Next (rs#LR <- (Val.add rs#PC Vone) #PC <- (symbol_offset ident Int.zero)) m
- | Pbs ident =>
+ | Pbs ident sg =>
Next (rs#PC <- (symbol_offset ident Int.zero)) m
| Pblr =>
Next (rs#PC <- (rs#LR)) m
| Pbt bit lbl =>
match rs#(reg_of_crbit bit) with
- | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label c lbl rs m
+ | Vint n => if Int.eq n Int.zero then Next (nextinstr rs) m else goto_label f lbl rs m
| _ => Stuck
end
| Pbtbl r tbl =>
@@ -613,7 +612,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome
| Vint n =>
match list_nth_z tbl (Int.unsigned n) with
| None => Stuck
- | Some lbl => goto_label c lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
+ | Some lbl => goto_label f lbl (rs #GPR12 <- Vundef #CTR <- Vundef) m
end
| _ => Stuck
end
@@ -857,27 +856,27 @@ Inductive state: Type :=
Inductive step: state -> trace -> state -> Prop :=
| exec_step_internal:
- forall b ofs c i rs m rs' m',
+ forall b ofs f i rs m rs' m',
rs PC = Vptr b ofs ->
- Genv.find_funct_ptr ge b = Some (Internal c) ->
- find_instr (Int.unsigned ofs) c = Some i ->
- exec_instr c i rs m = Next rs' m' ->
+ Genv.find_funct_ptr ge b = Some (Internal f) ->
+ find_instr (Int.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 c ef args res rs m t vl rs' m',
+ forall b ofs f ef args res rs m t vl rs' m',
rs PC = Vptr b ofs ->
- Genv.find_funct_ptr ge b = Some (Internal c) ->
- find_instr (Int.unsigned ofs) c = Some (Pbuiltin ef args res) ->
+ Genv.find_funct_ptr ge b = Some (Internal f) ->
+ find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
external_call' ef ge (map rs args) m t vl m' ->
rs' = nextinstr
(set_regs res vl
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
step (State rs m) t (State rs' m')
| exec_step_annot:
- forall b ofs c ef args rs m vargs t v m',
+ forall b ofs f ef args rs m vargs t v m',
rs PC = Vptr b ofs ->
- Genv.find_funct_ptr ge b = Some (Internal c) ->
- find_instr (Int.unsigned ofs) c = Some (Pannot ef args) ->
+ Genv.find_funct_ptr ge b = Some (Internal f) ->
+ find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) ->
annot_arguments rs m args vargs ->
external_call' ef ge vargs m t v m' ->
step (State rs m) t
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index b3f0722..39c0d1b 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -623,21 +623,21 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
| Mstore chunk addr args src =>
transl_store chunk addr args src k
| Mcall sig (inl r) =>
- do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl :: k)
+ do r1 <- ireg_of r; OK (Pmtctr r1 :: Pbctrl sig :: k)
| Mcall sig (inr symb) =>
- OK (Pbl symb :: k)
+ OK (Pbl symb sig :: k)
| Mtailcall sig (inl r) =>
do r1 <- ireg_of r;
OK (Pmtctr r1 ::
Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
Pmtlr GPR0 ::
Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
- Pbctr :: k)
+ Pbctr sig :: k)
| Mtailcall sig (inr symb) =>
OK (Plwz GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 ::
Pmtlr GPR0 ::
Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) ::
- Pbs symb :: k)
+ Pbs symb sig :: k)
| Mbuiltin ef args res =>
OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k)
| Mannot ef args =>
@@ -703,15 +703,16 @@ Definition transl_code' (f: Mach.function) (il: list Mach.instruction) (it1p: bo
Definition transl_function (f: Mach.function) :=
do c <- transl_code' f f.(Mach.fn_code) false;
- OK (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
- Pmflr GPR0 ::
- Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: c).
-
-Definition transf_function (f: Mach.function) : res Asm.code :=
- do c <- transl_function f;
- if zlt Int.max_unsigned (list_length_z c)
+ OK (mkfunction f.(Mach.fn_sig)
+ (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
+ Pmflr GPR0 ::
+ Pstw GPR0 (Cint f.(fn_retaddr_ofs)) GPR1 :: 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))
then Error (msg "code size exceeded")
- else OK c.
+ else OK tf.
Definition transf_fundef (f: Mach.fundef) : res Asm.fundef :=
transf_partial_fundef transf_function f.
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 990d35d..5c99231 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -79,9 +79,9 @@ Qed.
Lemma transf_function_no_overflow:
forall f tf,
- transf_function f = OK tf -> list_length_z tf <= Int.max_unsigned.
+ transf_function f = OK tf -> list_length_z tf.(fn_code) <= Int.max_unsigned.
Proof.
- intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0.
+ intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x.(fn_code))); inv EQ0.
omega.
Qed.
@@ -316,11 +316,11 @@ Lemma transl_find_label:
forall lbl f tf,
transf_function f = OK tf ->
match Mach.find_label lbl f.(Mach.fn_code) with
- | None => find_label lbl tf = None
- | Some c => exists tc, find_label lbl tf = Some tc /\ transl_code f c false = OK tc
+ | None => find_label lbl tf.(fn_code) = None
+ | 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)); inv EQ0.
+ intros. monadInv H. destruct (zlt Int.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.
@@ -364,7 +364,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)); inv EQ0. monadInv EQ.
+ destruct (zlt Int.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.
@@ -607,7 +607,7 @@ Opaque loadind.
- (* Mcall *)
assert (f0 = f) by congruence. subst f0.
inv AT.
- assert (NOOV: list_length_z tf <= Int.max_unsigned).
+ assert (NOOV: list_length_z tf.(fn_code) <= Int.max_unsigned).
eapply transf_function_no_overflow; eauto.
destruct ros as [rf|fid]; simpl in H; monadInv H5.
+ (* Indirect call *)
@@ -652,7 +652,7 @@ Opaque loadind.
- (* Mtailcall *)
assert (f0 = f) by congruence. subst f0.
inversion AT; subst.
- assert (NOOV: list_length_z tf <= Int.max_unsigned).
+ assert (NOOV: list_length_z tf.(fn_code) <= Int.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.
@@ -672,9 +672,9 @@ Opaque loadind.
set (rs6 := rs5#PC <- (rs5 CTR)).
assert (exec_straight tge tf
(Pmtctr x0 :: Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0
- :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr :: x)
+ :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbctr sig :: x)
rs0 m'0
- (Pbctr :: x) rs5 m2').
+ (Pbctr sig :: x) rs5 m2').
apply exec_straight_step with rs2 m'0.
simpl. rewrite H9. auto. auto.
apply exec_straight_step with rs3 m'0.
@@ -713,9 +713,9 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
set (rs5 := rs4#PC <- (Vptr f' Int.zero)).
assert (exec_straight tge tf
(Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0
- :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid :: x)
+ :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid sig :: x)
rs0 m'0
- (Pbs fid :: x) rs4 m2').
+ (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.
@@ -851,7 +851,7 @@ Local Transparent destroyed_by_jumptable.
- (* Mreturn *)
assert (f0 = f) by congruence. subst f0.
inversion AT; subst.
- assert (NOOV: list_length_z tf <= Int.max_unsigned).
+ assert (NOOV: list_length_z tf.(fn_code) <= Int.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]].
@@ -900,7 +900,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)); inversion EQ1. clear EQ1.
+ destruct (zlt Int.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]].
@@ -916,9 +916,9 @@ Local Transparent destroyed_by_jumptable.
set (rs4 := nextinstr rs3).
assert (EXEC_PROLOGUE:
exec_straight tge x
- x rs0 m'
+ x.(fn_code) rs0 m'
x1 rs4 m3').
- rewrite <- H5 at 2.
+ rewrite <- H5 at 2. simpl.
apply exec_straight_three with rs2 m2' rs3 m2'.
unfold exec_instr. rewrite C. fold sp.
rewrite <- (sp_val _ _ _ AG). rewrite F. auto.
@@ -928,11 +928,11 @@ Local Transparent destroyed_by_jumptable.
rewrite Int.add_zero_l. simpl in P. rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. congruence.
auto. auto. auto.
left; exists (State rs4 m3'); split.
- eapply exec_straight_steps_1; eauto. unfold fn_code; omega. constructor.
+ eapply exec_straight_steps_1; eauto. omega. constructor.
econstructor; eauto.
change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone).
rewrite ATPC. simpl. constructor; eauto.
- subst x. unfold fn_code. eapply code_tail_next_int. omega.
+ subst x; simpl in g. unfold fn_code. eapply code_tail_next_int. omega.
eapply code_tail_next_int. omega.
eapply code_tail_next_int. omega.
constructor.
diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index d9b6cf3..e637ef8 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -183,7 +183,7 @@ Ltac Simpl := repeat Simplif.
Section CONSTRUCTORS.
Variable ge: genv.
-Variable fn: code.
+Variable fn: function.
(** Properties of comparisons. *)
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 764020a..87d22f2 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -668,9 +668,9 @@ let print_instruction oc tbl pc fallthrough = function
fprintf oc " andis. %a, %a, %a\n" ireg r1 ireg r2 constant c
| Pb lbl ->
fprintf oc " b %a\n" label (transl_label lbl)
- | Pbctr ->
+ | Pbctr sg ->
fprintf oc " bctr\n"
- | Pbctrl ->
+ | Pbctrl sg ->
fprintf oc " bctrl\n"
| Pbf(bit, lbl) ->
if !Clflags.option_faligncondbranchs > 0 then
@@ -683,9 +683,9 @@ let print_instruction oc tbl pc fallthrough = function
fprintf oc " b %a\n" label (transl_label lbl);
fprintf oc "%a:\n" label next
end
- | Pbl s ->
+ | Pbl(s, sg) ->
fprintf oc " bl %a\n" symbol s
- | Pbs s ->
+ | Pbs(s, sg) ->
fprintf oc " b %a\n" symbol s
| Pblr ->
fprintf oc " blr\n"
@@ -930,7 +930,7 @@ let print_instruction oc tbl pc fallthrough = function
let instr_fall_through = function
| Pb _ -> false
- | Pbctr -> false
+ | Pbctr _ -> false
| Pbs _ -> false
| Pblr -> false
| _ -> true
@@ -1008,7 +1008,7 @@ let print_jumptable oc (lbl, tbl) =
(fun l -> fprintf oc " .long %a\n" label (transl_label l))
tbl
-let print_function oc name code =
+let print_function oc name fn =
Hashtbl.clear current_function_labels;
float_literals := [];
jumptables := [];
@@ -1025,7 +1025,8 @@ let print_function oc name code =
fprintf oc "%a:\n" symbol name;
print_location oc (C2C.atom_location name);
cfi_startproc oc;
- print_instructions oc (label_positions PTree.empty 0 code) 0 true code;
+ print_instructions oc (label_positions PTree.empty 0 fn.fn_code)
+ 0 true fn.fn_code;
cfi_endproc oc;
fprintf oc " .type %a, @function\n" symbol name;
fprintf oc " .size %a, . - %a\n" symbol name symbol name;
diff --git a/powerpc/Unusedglob1.ml b/powerpc/Unusedglob1.ml
index fabac33..49c0774 100644
--- a/powerpc/Unusedglob1.ml
+++ b/powerpc/Unusedglob1.ml
@@ -31,8 +31,8 @@ let referenced_builtin ef =
| _ -> []
let referenced_instr = function
- | Pbl s -> [s]
- | Pbs s -> [s]
+ | Pbl(s, _) -> [s]
+ | Pbs(s, _) -> [s]
| Paddi(_, _, c)
| Paddic(_, _, c)
| Paddis(_, _, c)
@@ -60,4 +60,4 @@ let referenced_instr = function
| Pbuiltin(ef, _, _) -> referenced_builtin ef
| _ -> []
-let code_of_function f = f
+let code_of_function f = f.fn_code
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 18:04:45 +0000