secure-compilation · dongjaelee1 · Mar 28, 2023 · Mar 29, 2023 · Mar 30, 2023 · Mar 30, 2023
diff --git a/Makefile b/Makefile
@@ -140,7 +140,7 @@ CFRONTEND=Ctypes.v Cop.v Csyntax.v Csem.v Ctyping.v Cstrategy.v Cexec.v \
 
 # Security proof (in security/)
 
-SECURITY=RSC.v Split.v Blame.v Recomposition.v
+SECURITY=RSC.v Split.v Blame.v Recomposition.v Tactics.v MemoryWeak.v MemoryDelta.v BtBasics.v BtInfoAsm.v BtInfoAsmBound.v Backtranslation.v BacktranslationAux.v BacktranslationProof.v
 
 # Parser
 

diff --git a/backend/Allocproof.v b/backend/Allocproof.v
@@ -52,6 +52,21 @@ Proof.
   - now inv H.
 Qed.
 
+Instance external_transf_fundef: is_external_transl_partial transf_fundef.
+Proof.
+  unfold transf_fundef, transf_partial_fundef, transf_function, check_function.
+  intros f ? ? H.
+  destruct f.
+  - destruct type_function; try easy.
+    destruct regalloc; try easy.
+    destruct analyze; try easy.
+    destruct eq_compartment as [e|?]; try easy.
+    monadInv H. monadInv EQ.
+    monadInv EQ0.
+    destruct check_entrypoints_aux; try easy.
+  - now inv H.
+Qed.
+
 Lemma transf_program_match:
   forall p tp, transf_program p = OK tp -> match_prog p tp.
 Proof.

diff --git a/backend/CSEproof.v b/backend/CSEproof.v
@@ -31,6 +31,16 @@ Proof.
   now inv H.
 Qed.
 
+Instance external_transf_function rm:
+  is_external_transl_partial (transf_fundef rm).
+Proof.
+  unfold transf_fundef, transf_function.
+  intros [f | ef] ? ? H; try now inv H.
+  simpl in *.
+  destruct analyze; try easy.
+  now inv H.
+Qed.
+
 Lemma transf_program_match:
   forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
 Proof.

diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
@@ -27,6 +27,9 @@ Definition match_prog (p tp: Linear.program) :=
 Instance comp_match_prog: has_comp_transl transf_function.
 Proof. now intros f. Qed.
 
+Instance external_transf_fundef: is_external_transl transf_fundef.
+Proof. now intros ? [f | ef]. Qed.
+
 Lemma transf_program_match:
   forall p, match_prog p (transf_program p).
 Proof.

diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
@@ -25,6 +25,9 @@ Definition match_prog (prog tprog: program) :=
 Instance comp_transf_function rm: has_comp_transl (transf_function rm).
 Proof. now intro. Qed.
 
+Instance external_transf_function rm: is_external_transl (transf_fundef rm).
+Proof. now intros ? []. Qed.
+
 Lemma transf_program_match:
   forall prog, match_prog prog (transf_program prog).
 Proof.

diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
@@ -30,6 +30,15 @@ Proof.
   now inv H.
 Qed.
 
+Instance external_transf_function rm: is_external_transl_partial (transf_fundef rm).
+Proof.
+  unfold transf_fundef, transf_function.
+  intros [f | ef] ? ? H; try now inv H.
+  simpl in *.
+  destruct analyze; try easy.
+  now inv H.
+Qed.
+
 Lemma transf_program_match:
   forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
 Proof.

diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v
@@ -30,6 +30,14 @@ Proof.
   now destruct ana_function; inv H.
 Qed.
 
+Instance external_transf_function: is_external_transl_partial transf_fundef.
+Proof.
+  unfold transf_fundef, transf_function.
+  intros [f | ef] ? ? H; simpl in *.
+  now destruct ana_function; inv H.
+  now inv H.
+Qed.
+
 Lemma transf_program_match:
   forall p tp, transf_program p = OK tp -> match_prog p tp.
 Proof.

diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
@@ -31,6 +31,17 @@ Proof.
   now inv H.
 Qed.
 
+Instance external_transl_fundef fenv: is_external_transl_partial (transf_fundef fenv).
+Proof.
+  unfold transf_fundef, transf_function.
+  intros [f | ef] tf ? H; try now inv H.
+  unfold transf_partial_fundef in H.
+  destruct (expand_function _ _ _).
+  destruct (zlt _ _); try easy.
+  simpl in *.
+  now inv H.
+Qed.
+
 Lemma transf_program_match:
   forall prog tprog, transf_program prog = OK tprog -> match_prog prog tprog.
 Proof.

diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
@@ -30,6 +30,12 @@ Proof.
   intros f ? H; now monadInv H.
 Qed.
 
+Instance external_transf_fundef: is_external_transl_partial transf_fundef.
+Proof.
+  unfold transf_fundef, transf_function.
+  intros [f | ef] ? ? H; now monadInv H.
+Qed.
+
 Lemma transf_program_match:
   forall p tp, transf_program p = OK tp -> match_prog p tp.
 Proof.

diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
@@ -358,6 +358,15 @@ Proof.
   now inv H.
 Qed.
 
+Instance external_transl_fundef: is_external_transl_partial transl_fundef.
+Proof.
+  unfold transl_fundef, transl_function.
+  intros [f | ef] tf ? H; simpl in *.
+  - destruct (transl_fun _ _) as [|[??] ? ?]; try discriminate.
+    now inv H.
+  - now inv H.
+Qed.
+
 Lemma transf_program_match:
   forall p tp, transl_program p = OK tp -> match_prog p tp.
 Proof.

diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
@@ -23,6 +23,9 @@ Definition match_prog (p tp: RTL.program) :=
 Instance comp_transf_function: has_comp_transl transf_function.
 Proof. now intros. Qed.
 
+Instance is_external_transf_function: is_external_transl transf_fundef.
+Proof. unfold transf_fundef. intros ? [f | ef]; reflexivity. Qed.
+
 Lemma transf_program_match:
   forall p, match_prog p (transf_program p).
 Proof.

diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
@@ -46,6 +46,11 @@ Proof.
   exact (comp_transl_partial _ EQ).
 Qed.
 
+Instance is_external_match_fundef: is_external_match match_fundef.
+Proof.
+  intros cunit f tf cp (hf & hf_c & G & _ & H).
+  destruct f as [f|ef]; monadInv H; simpl; reflexivity.
+Qed.
 (** Processing of helper functions *)
 
 Lemma record_globdefs_sound:

diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
@@ -35,6 +35,12 @@ Proof.
   now monadInv H.
 Qed.
 
+Instance external_transf_fundef: is_external_transl_partial transf_fundef.
+Proof.
+  unfold transf_fundef.
+  intros [f | ef] tf ? H; try now monadInv H.
+Qed.
+
 Lemma transf_program_match:
   forall p tp, transf_program p = OK tp -> match_prog p tp.
 Proof.

diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
@@ -215,6 +215,12 @@ Proof.
   now destruct zeq.
 Qed.
 
+Instance external_transf_fundef cenv: is_external_transl (transf_fundef cenv).
+Proof.
+  unfold transf_fundef, transf_function, RTL.transf_function.
+  intros ? [f | ef]; simpl; reflexivity.
+Qed.
+
 Lemma transf_program_match:
   forall p, match_prog p (transf_program p).
 Proof.

diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
@@ -25,6 +25,9 @@ Definition match_prog (p tp: program) :=
 Instance comp_tunnel_fundef: has_comp_transl tunnel_function.
 Proof. now intro. Qed.
 
+Instance external_tunnel_fundef: is_external_transl tunnel_fundef.
+Proof. now intros ? []. Qed.
+
 Lemma transf_program_match:
   forall p, match_prog p (tunnel_program p).
 Proof.

diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
@@ -866,7 +866,7 @@ Proof.
         simpl. rewrite A. rewrite H0. subst; now destruct Ptrofs.eq_dec.
       + right.
         unfold Genv.allowed_cross_call in *.
-        destruct H2 as [i [cp' [H21 [H22 [H23 H24]]]]].
+        destruct H2 as [i [cp' [H21 [H22 [H23 [H24 H25]]]]]].
         exists i. exists cp'.
         repeat split.
         * apply Genv.find_invert_symbol.
@@ -875,16 +875,20 @@ Proof.
           specialize (E j H). unfold symbols_inject in E.
           destruct E as [E1 [E2 [E3 E4]]].
           specialize (E2 i _ _ _ H6). simpl in E2. specialize (E2 H21). destruct E2. auto.
-        * rewrite <- H22. unfold Genv.find_comp.
+        * intros. unfold Genv.find_funct in *.
+          destruct (Ptrofs.eq_dec (Ptrofs.add Ptrofs.zero (Ptrofs.repr delta)) Ptrofs.zero); try congruence.
+          assert (fd0 = fd) by congruence; subst fd0.
+          apply H22. eauto.
+        * rewrite <- H23. unfold Genv.find_comp.
           simpl. rewrite A. rewrite H0. subst; now destruct Ptrofs.eq_dec.
         * apply match_prog_pol in TRANSF.
           unfold tge, Genv.globalenv. rewrite TRANSF.
           rewrite Genv.genv_pol_add_globals. simpl.
-          unfold ge, Genv.globalenv in H23. now rewrite Genv.genv_pol_add_globals in H23.
+          unfold ge, Genv.globalenv in H24. now rewrite Genv.genv_pol_add_globals in H24.
         * apply match_prog_pol in TRANSF.
           unfold tge, Genv.globalenv. rewrite TRANSF.
           rewrite Genv.genv_pol_add_globals. simpl.
-          unfold ge, Genv.globalenv in H24. now rewrite Genv.genv_pol_add_globals in H24. }
+          unfold ge, Genv.globalenv in H25. now rewrite Genv.genv_pol_add_globals in H25. }
     { unfold Genv.type_of_call. unfold Genv.find_comp, Genv.find_funct.
       rewrite R, H0, A, B. now destruct Ptrofs.eq_dec. }
     { unfold Genv.find_comp, Genv.find_funct. rewrite R, H0, A, B. reflexivity. }
@@ -913,12 +917,16 @@ Proof.
           specialize (E j H). unfold symbols_inject in E.
           destruct E as [E1 [E2 [E3 E4]]].
           specialize (E2 i _ _ _ Q). simpl in E2. specialize (E2 H21). destruct E2. auto.
-        * rewrite <- H22. unfold Genv.find_comp.
+        * intros. unfold Genv.find_funct in *.
+          destruct Ptrofs.eq_dec; try congruence.
+          assert (fd0 = fd) by congruence; subst fd0.
+          apply H22. eauto.
+        * rewrite <- H23. unfold Genv.find_comp.
           simpl. rewrite A. rewrite H0. reflexivity.
         * apply match_prog_pol in TRANSF.
           unfold tge, Genv.globalenv. rewrite TRANSF.
           rewrite Genv.genv_pol_add_globals. simpl.
-          unfold ge, Genv.globalenv in H23. now rewrite Genv.genv_pol_add_globals in H23.
+          unfold ge, Genv.globalenv in H24. now rewrite Genv.genv_pol_add_globals in H24.
         * apply match_prog_pol in TRANSF.
           unfold tge, Genv.globalenv. rewrite TRANSF.
           rewrite Genv.genv_pol_add_globals. simpl.

diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
@@ -42,6 +42,16 @@ Proof.
   now monadInv H.
 Qed.
 
+Instance external_transl_fundef: is_external_transl_partial transl_fundef.
+Proof.
+  unfold transl_fundef, transl_function, transl_funbody.
+  intros [f | ef] tf ? H; simpl in H.
+  destruct build_compilenv.
+  destruct zle; try easy.
+  now monadInv H.
+  now monadInv H.
+Qed.
+
 Lemma transf_program_match:
   forall p tp, transl_program p = OK tp -> match_prog p tp.
 Proof.

diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
@@ -884,3 +884,4 @@ Proof.
   inv H; simpl; try lia. eapply external_call_trace_length; eauto.
   inv EV; simpl; try lia.
 Qed.
+
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
@@ -44,6 +44,11 @@ Proof.
   exact (comp_transl_partial _ H).
 Qed.
 
+Instance external_match_fundef: is_external_match match_fundef.
+Proof.
+  intros cu ? ? ? [f tf H|]; reflexivity.
+Qed.
+
 Lemma transf_program_match:
   forall p tp, transl_program p = OK tp -> match_prog p tp.
 Proof.

diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
@@ -17,7 +17,7 @@
 (** Abstract syntax for the Compcert C language *)
 
 Require Import Coqlib Maps Integers Floats Errors.
-Require Import AST Linking Values.
+Require Import AST Linking Values Builtins.
 Require Import Ctypes Cop.
 
 (** ** Expressions *)
@@ -227,3 +227,4 @@ Definition type_of_fundef (f: fundef) : type :=
 - a proof that this environment is consistent with the definitions. *)
 
 Definition program := Ctypes.program function.
+
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
@@ -17,7 +17,7 @@
 (** Type expressions for the Compcert C and Clight languages *)
 
 Require Import Axioms Coqlib Maps Errors.
-Require Import AST Linking.
+Require Import AST Linking Builtins.
 Require Archi.
 
 Set Asymmetric Patterns.
@@ -2021,3 +2021,60 @@ Qed.
 
 End LINK_MATCH_PROGRAM.
 
+
+Global Program Instance is_external_fundef_ctypes f : is_external (fundef f) :=
+  { is_ok :=
+    fun cp' fd =>
+      match fd with
+      | Internal _ => True
+      | External ef _ _ _ =>
+          match ef with
+          | EF_external cp name sg  => True
+          | EF_builtin cp name sg
+          | EF_runtime cp name sg =>
+              match Builtins.lookup_builtin_function name sg with
+              | None => True
+              | _ => cp = cp'
+              end
+          | EF_vload cp chunk          => cp = cp'
+          | EF_vstore cp chunk         => cp = cp'
+          | EF_malloc cp                => cp = cp'
+          | EF_free cp                 => cp = cp'
+          | EF_memcpy cp sz al         => cp = cp'
+          | EF_annot cp kind txt targs   => True
+          | EF_annot_val cp kind txt targ => True
+          | EF_inline_asm cp txt sg clb => True
+          | EF_debug cp kind txt targs => cp = cp'
+          end
+      end;
+    is_ok_b :=
+      fun cp' fd =>
+        match fd with
+        | Internal _ => true
+        | External ef _ _ _ =>
+            match ef with
+            | EF_external cp name sg  => true
+            | EF_builtin cp name sg
+            | EF_runtime cp name sg =>
+                match lookup_builtin_function name sg with
+                | None => true
+                | _ => Pos.eqb cp cp'
+                end
+            | EF_vload cp chunk          => Pos.eqb cp cp'
+            | EF_vstore cp chunk         => Pos.eqb cp cp'
+            | EF_malloc cp                => Pos.eqb cp cp'
+            | EF_free cp                 => Pos.eqb cp cp'
+            | EF_memcpy cp sz al         => Pos.eqb cp cp'
+            | EF_annot cp kind txt targs   => true
+            | EF_annot_val cp kind txt targ => true
+            | EF_inline_asm cp txt sg clb => true
+            | EF_debug cp kind txt targs => Pos.eqb cp cp'
+            end
+        end;
+    is_ok_reflect := _;
+  }.
+Next Obligation.
+  destruct fd as [| []]; simpl; try now (symmetry; eauto using Pos.eqb_eq).
+  destruct (lookup_builtin_function name sg); try now (symmetry; eauto using Pos.eqb_eq).
+  destruct (lookup_builtin_function name sg); try now (symmetry; eauto using Pos.eqb_eq).
+Defined.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
@@ -39,6 +39,13 @@ Proof.
   symmetry; eauto.
 Qed.
 
+Instance external_tr_fundef:
+  is_external_match (fun cu f tf => tr_fundef cu f tf).
+Proof.
+  intros ctx f tf ? [? ? []|]; reflexivity.
+Qed.
+
+
 Lemma transf_program_match:
   forall p tp, transl_program p = OK tp -> match_prog p tp.
 Proof.

diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
@@ -38,6 +38,11 @@ Proof.
   now monadInv EQ.
 Qed.
 
+Instance external_transf_fundef: is_external_transl_partial transf_fundef.
+Proof.
+  intros [f | ef] ? ? H; monadInv H; reflexivity.
+Qed.
+
 Lemma match_transf_program:
   forall p tp, transf_program p = OK tp -> match_prog p tp.
 Proof.
Original file line number	Diff line number	Diff line change
Expand Up		@@ -884,3 +884,4 @@ Proof.
		inv H; simpl; try lia. eapply external_call_trace_length; eauto.
		inv EV; simpl; try lia.
		Qed.