Generate CFI directives for AArch64 and for RISC-V

SJTU-PLV · Mar 15, 2024 · 545bffb · 545bffb
1 parent 1c4dcdd
commit 545bffb
Show file tree

Hide file tree

Showing 9 changed files with 54 additions and 28 deletions.
diff --git a/aarch64/Asm.v b/aarch64/Asm.v
@@ -1102,6 +1102,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
           end
       | _ => Stuck
       end
+  | Pcfi_rel_offset _ =>
+      Next (nextinstr rs) m
   | Pbuiltin ef args res => Stuck    (**r treated specially below *)
   (** The following instructions and directives are not generated directly
       by Asmgen, so we do not model them. *)
@@ -1120,8 +1122,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfmax _ _ _ _
   | Pfmin _ _ _ _
   | Pnop
-  | Pcfi_adjust _ 
-  | Pcfi_rel_offset _ =>
+  | Pcfi_adjust _ =>
       Stuck
   end.
 

diff --git a/aarch64/Asmexpand.ml b/aarch64/Asmexpand.ml
@@ -423,6 +423,7 @@ let expand_instruction instr =
         current_function_stacksize := Z.to_int64 sz
       end;
       expand_addimm64 XSP XSP (Ptrofs.repr (Z.neg sz));
+      emit (Pcfi_adjust sz);
       expand_storeptr X15 XSP ofs
   | Pfreeframe (sz, ofs) ->
       expand_addimm64 XSP XSP (coqint_of_camlint64 !current_function_stacksize)

diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v
@@ -1148,7 +1148,8 @@ Definition transl_function (f: Mach.function) :=
   do c <- transl_code' f f.(Mach.fn_code) true;
   OK (mkfunction f.(Mach.fn_sig)
         (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
-         storeptr RA XSP f.(fn_retaddr_ofs) c)).
+         storeptr RA XSP f.(fn_retaddr_ofs)
+          (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;

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
@@ -395,8 +395,8 @@ Lemma transl_find_label:
   end.
 Proof.
   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. unfold fn_code. 
-  simpl. destruct (storeptr_label X30 XSP (fn_retaddr_ofs f) x) as [A B]; rewrite B. 
+  monadInv EQ. simpl. rewrite transl_code'_transl_code in EQ0.
+  erewrite tail_nolabel_find_label by (apply storeptr_label). simpl.
   eapply transl_code_label; eauto.
 Qed.
 
@@ -442,7 +442,9 @@ Proof.
   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 true; split; auto. unfold fn_code.
-  constructor. apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) x).
+  constructor. eapply is_tail_trans.
+  2: apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) (Pcfi_rel_offset (Ptrofs.to_int (fn_retaddr_ofs f0)) :: x)).
+  repeat constructor.
 - exact transf_function_no_overflow.
 Qed.
 
@@ -930,28 +932,32 @@ Local Transparent destroyed_by_op.
   change (chunk_of_type Tptr) with Mint64 in *.
   (* Execution of function prologue *)
   monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
+  set (x1 := Pcfi_rel_offset (Ptrofs.to_int (fn_retaddr_ofs f)) :: x0) in *.
   set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::
-                 storeptr RA XSP (fn_retaddr_ofs f) x0) in *.
+                 storeptr RA XSP (fn_retaddr_ofs f) x1) in *.
   set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
   set (rs2 := nextinstr (rs0#X15 <- (parent_sp s) #SP <- sp #X16 <- Vundef)).
-  exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2).
+  exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x1 m2' m3' rs2).
     simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. 
     change (rs2 X2) with sp. eexact P. 
     simpl; congruence. congruence.
   intros (rs3 & U & V).
+  set (rs4 := nextinstr rs3).
   assert (EXEC_PROLOGUE:
             exec_straight tge tf
               tf.(fn_code) rs0 m'
-              x0 rs3 m3').
+              x0 rs4 m3').
   { change (fn_code tf) with tfbody; unfold tfbody.
     apply exec_straight_step with rs2 m2'.
     unfold exec_instr. rewrite C. fold sp.
     rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity.
-    reflexivity. 
-    eexact U. }
+    reflexivity.
+    eapply exec_straight_trans with (rs2 := rs3) (m2 := m3').
+    eexact U. eapply exec_straight_one; eauto.
+  }
   exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor.
   intros (ofs' & X & Y).                    
-  left; exists (State rs3 m3'); split.
+  left; exists (State rs4 m3'); split.
   eapply exec_straight_steps_1; eauto. lia. constructor.
   econstructor; eauto.
   rewrite X; econstructor; eauto. 
@@ -963,8 +969,9 @@ Local Transparent destroyed_by_op.
 Local Transparent destroyed_at_function_entry. simpl.
   simpl; intros; Simpl.
   unfold sp; congruence.
-  intros. rewrite V by auto with asmgen. reflexivity.
-
+  intros. unfold rs4. rewrite  <- V by eauto with asmgen; Simpl.
+  unfold rs4 in * ; intros.
+  rewrite nextinstr_inv; try apply V; eauto with asmgen.
 - (* external function *)
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B.

diff --git a/aarch64/TargetPrinter.ml b/aarch64/TargetPrinter.ml
@@ -605,7 +605,7 @@ module Target(System: SYSTEM): TARGET =
     | Pcfi_adjust sz ->
         cfi_adjust oc (camlint_of_coqint sz)
     | Pcfi_rel_offset ofs ->
-        cfi_rel_offset oc "lr" (camlint_of_coqint ofs)
+        cfi_rel_offset oc "x30" (camlint_of_coqint ofs)
     | Pbuiltin(ef, args, res) ->
         begin match ef with
           | EF_annot(kind,txt, targs) ->

diff --git a/riscV/Asm.v b/riscV/Asm.v
@@ -348,7 +348,10 @@ Inductive instruction : Type :=
   | Pbtbl   (r: ireg)  (tbl: list label)            (**r N-way branch through a jump table *)
   | Pbuiltin: external_function -> list (builtin_arg preg)
               -> builtin_res preg -> instruction    (**r built-in function (pseudo) *)
-  | Pnop : instruction.                             (**r nop instruction *)
+  | Pnop : instruction                             (**r nop instruction *)
+  | Pcfi_rel_offset (ofs: int)                      (**r .cfi_rel_offset debug directive *)
+  | Pcfi_adjust (ofs: int).                         (**r .cfi_adjust debug directive *)
+
 
 
 (** The pseudo-instructions are the following:
@@ -964,11 +967,14 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
           end
       | _ => Stuck
       end
+  | Pcfi_rel_offset _ =>
+      Next (nextinstr rs) m
   | Pbuiltin ef args res =>
       Stuck (**r treated specially below *)
 
   (** The following instructions and directives are not generated directly by Asmgen,
       so we do not model them. *)
+  | Pcfi_adjust _
   | Pfence
 
   | Pfmvxs _ _

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
@@ -921,7 +921,7 @@ Definition transl_function (f: Mach.function) :=
   do c <- transl_code' f f.(Mach.fn_code) true;
   OK (mkfunction f.(Mach.fn_sig)
         (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::
-         storeind_ptr RA SP f.(fn_retaddr_ofs) c)).
+         storeind_ptr RA SP f.(fn_retaddr_ofs) (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;

diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
@@ -403,8 +403,8 @@ Lemma transl_find_label:
   end.
 Proof.
   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. unfold fn_code. 
-  simpl. destruct (storeind_ptr_label X1 X2 (fn_retaddr_ofs f) x) as [A B]; rewrite B. 
+  monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code.
+  simpl. erewrite tail_nolabel_find_label by (apply storeind_ptr_label). simpl.
   eapply transl_code_label; eauto.
 Qed.
 
@@ -450,7 +450,9 @@ Proof.
   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 true; split; auto. unfold fn_code.
-  constructor. apply (storeind_ptr_label X1 X2 (fn_retaddr_ofs f0) x).
+  constructor.  eapply is_tail_trans.
+  2: apply (storeind_ptr_label X1 X2 (fn_retaddr_ofs f0) (Pcfi_rel_offset (Ptrofs.to_int (fn_retaddr_ofs f0)) :: x)).
+  repeat constructor.
 - exact transf_function_no_overflow.
 Qed.
 
@@ -932,28 +934,32 @@ Local Transparent destroyed_by_op.
   intros [m3' [P Q]].
   (* Execution of function prologue *)
   monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
+  set (x1 := Pcfi_rel_offset (Ptrofs.to_int (fn_retaddr_ofs f)) :: x0) in *.
   set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) ::
-                 storeind_ptr RA SP (fn_retaddr_ofs f) x0) in *.
+                 storeind_ptr RA SP (fn_retaddr_ofs f) x1) in *.
   set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *.
   set (rs2 := nextinstr (rs0#X30 <- (parent_sp s) #SP <- sp #X31 <- Vundef)).
-  exploit (storeind_ptr_correct tge tf SP (fn_retaddr_ofs f) RA x0 rs2 m2').
+  exploit (storeind_ptr_correct tge tf SP (fn_retaddr_ofs f) RA x1 rs2 m2').
     rewrite chunk_of_Tptr in P. change (rs2 X1) with (rs0 X1). rewrite ATLR. 
     change (rs2 X2) with sp. eexact P. 
     congruence. congruence.
   intros (rs3 & U & V).
+  set (rs4 := nextinstr rs3).
   assert (EXEC_PROLOGUE:
             exec_straight tge tf
               tf.(fn_code) rs0 m'
-              x0 rs3 m3').
+              x0 rs4 m3').
   { change (fn_code tf) with tfbody; unfold tfbody.
     apply exec_straight_step with rs2 m2'.
     unfold exec_instr. rewrite C. fold sp.
     rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. rewrite F. reflexivity.
-    reflexivity. 
-    eexact U. }
+    reflexivity.
+    eapply exec_straight_trans with (rs2 := rs3) (m2 := m3').
+    eexact U. eapply exec_straight_one; eauto.
+  }
   exploit exec_straight_steps_2; eauto using functions_transl. lia. constructor.
   intros (ofs' & X & Y).                    
-  left; exists (State rs3 m3'); split.
+  left; exists (State rs4 m3'); split.
   eapply exec_straight_steps_1; eauto. lia. constructor.
   econstructor; eauto.
   rewrite X; econstructor; eauto. 
@@ -965,8 +971,9 @@ Local Transparent destroyed_by_op.
 Local Transparent destroyed_at_function_entry.
   simpl; intros; Simpl.
   unfold sp; congruence.
-  intros. rewrite V by auto with asmgen. reflexivity.
-
+  intros. unfold rs4; Simpl. unfold rs4; intros.
+  unfold rs4 in * ; intros.
+  rewrite nextinstr_inv; try apply V; eauto with asmgen.
 - (* external function *)
   exploit functions_translated; eauto.
   intros [tf [A B]]. simpl in B. inv B.

diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
@@ -525,6 +525,9 @@ module Target : TARGET =
          fprintf oc "%s end pseudoinstr btbl\n" comment
       | Pnop ->
         fprintf oc "	nop\n"
+      | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz)
+      | Pcfi_rel_offset ofs ->
+        cfi_rel_offset oc "x1" (camlint_of_coqint ofs)
       | Pbuiltin(ef, args, res) ->
          begin match ef with
            | EF_annot(kind,txt, targs) ->