Changes to the compartment model

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
+SECURITY= Split.v Tactics.v MemoryWeak.v MemoryDelta.v BtBasics.v BtInfoAsm.v BtInfoAsmBound.v Backtranslation.v BacktranslationAux.v BacktranslationProof.v
 
 # Parser
 

backend/Allocation.v

@@ -1008,13 +1008,13 @@ Definition kind_second_word := if Archi.big_endian then Low else High.
   equations that must hold "before" these instructions, or [None] if
   impossible. *)
 
-(* FIXME A [Genv.type_of_call]-like function that closely mimics it but does not
-   take a global environment as a parameter and only distinguishes between
-   cross-compartment calls and everything else. Can be made cleaner. *)
-Definition is_external_call (cp: compartment) (cp': compartment): bool :=
-  if Pos.eqb cp cp' then false
-  else if Pos.eqb cp' default_compartment then false
-       else true.
+(* (* FIXME A [Genv.type_of_call]-like function that closely mimics it but does not *)
+(*    take a global environment as a parameter and only distinguishes between *)
+(*    cross-compartment calls and everything else. Can be made cleaner. *) *)
+(* Definition is_external_call (cp: compartment) (cp': compartment): bool := *)
+(*   if Pos.eqb cp cp' then false *)
+(*   else if Pos.eqb cp' default_compartment then false *)
+(*        else true. *)
 
 Definition transfer_aux (f: RTL.function) (env: regenv)
                         (shape: block_shape) (e: eqs) : option eqs :=
@@ -1120,7 +1120,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       assertion (can_undef (destroyed_by_builtin ef) e2);
       do e3 <-
         match ef with
-        | EF_debug _ _ _ _ => add_equations_debug_args env args args' e2
+        | EF_debug _ _ _ => add_equations_debug_args env args args' e2
         | _              => add_equations_builtin_args env args args' e2
         end;
       track_moves env mv1 e3
@@ -1365,7 +1365,7 @@ Definition check_function (rtl: RTL.function) (ltl: LTL.function) (env: regenv):
   match analyze rtl env bsh with
   | None => Error (msg "allocation analysis diverges")
   | Some a =>
-    if eq_compartment rtl.(RTL.fn_comp) ltl.(LTL.fn_comp) then
+    if cp_eq_dec rtl.(RTL.fn_comp) ltl.(LTL.fn_comp) then
       check_entrypoints rtl ltl env bsh a
     else Error (msg "register allocation changed the function compartment")
   end.
@@ -1390,6 +1390,32 @@ Definition transf_function (f: RTL.function) : res LTL.function :=
 Definition transf_fundef (fd: RTL.fundef) : res LTL.fundef :=
   AST.transf_partial_fundef transf_function fd.
 
+#[global] Instance comp_transf_function: has_comp_transl_partial transf_function.
+Proof.
+  unfold transf_function, check_function.
+  intros f ? H.
+  destruct type_function; try easy.
+  destruct regalloc; try easy.
+  destruct analyze; try easy.
+  destruct cp_eq_dec as [e|?]; try easy.
+  monadInv H.
+  exact e.
+Qed.
+
+#[global] Instance comp_transf_fundef: has_comp_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 cp_eq_dec as [e|?]; try easy.
+    monadInv H. monadInv EQ.
+    exact e.
+  - now inv H.
+Qed.
+
 Definition transf_program (p: RTL.program) : res LTL.program :=
   transform_partial_program transf_fundef p.
 

backend/Allocproof.v

@@ -25,34 +25,6 @@ Require Import Allocation.
 Definition match_prog (p: RTL.program) (tp: LTL.program) :=
   match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.
 
-#[global]
-Instance comp_transf_function: has_comp_transl_partial transf_function.
-Proof.
-  unfold transf_function, check_function.
-  intros f ? H.
-  destruct type_function; try easy.
-  destruct regalloc; try easy.
-  destruct analyze; try easy.
-  destruct eq_compartment as [e|?]; try easy.
-  monadInv H.
-  exact e.
-Qed.
-
-#[global]
-Instance comp_transf_fundef: has_comp_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.
-    exact e.
-  - now inv H.
-Qed.
-
 Lemma transf_program_match:
   forall p tp, transf_program p = OK tp -> match_prog p tp.
 Proof.
@@ -2297,20 +2269,20 @@ Proof.
 Qed.
 
 Lemma add_equations_builtin_eval:
-  forall ef env args args' e1 e2 m1 m1' rs ls (ge: RTL.genv) sp vargs t vres m2,
+  forall ef cp env args args' e1 e2 m1 m1' rs ls (ge: RTL.genv) sp vargs t vres m2,
   wt_regset env rs ->
   match ef with
-  | EF_debug _ _ _ _ => add_equations_debug_args env args args' e1
+  | EF_debug _ _ _ => add_equations_debug_args env args args' e1
   | _              => add_equations_builtin_args env args args' e1
   end = Some e2 ->
   Mem.extends m1 m1' ->
   satisf rs ls e2 ->
   eval_builtin_args ge (fun r => rs # r) sp m1 args vargs ->
-  external_call ef ge vargs m1 t vres m2 ->
+  external_call ef ge cp vargs m1 t vres m2 ->
   satisf rs ls e1 /\
   exists vargs' vres' m2',
      eval_builtin_args ge ls sp m1' args' vargs'
-  /\ external_call ef ge vargs' m1' t vres' m2'
+  /\ external_call ef ge cp vargs' m1' t vres' m2'
   /\ Val.lessdef vres vres'
   /\ Mem.extends m2 m2'.
 Proof.
@@ -2319,7 +2291,7 @@ Proof.
     satisf rs ls e1 /\
     exists vargs' vres' m2',
        eval_builtin_args ge ls sp m1' args' vargs'
-    /\ external_call ef ge vargs' m1' t vres' m2'
+    /\ external_call ef ge cp vargs' m1' t vres' m2'
     /\ Val.lessdef vres vres'
     /\ Mem.extends m2 m2').
   {
@@ -2428,7 +2400,7 @@ Proof.
   destruct (check_function f f0 env) as [] eqn:?; inv H.
   unfold check_function in Heqr.
   destruct (analyze f env (pair_codes f tf)) as [an|] eqn:?; try discriminate.
-  destruct eq_compartment as [e|]; try discriminate.
+  destruct cp_eq_dec as [e|]; try discriminate.
   monadInv Heqr.
   destruct (check_entrypoints_aux f tf env x) as [y|] eqn:?; try discriminate.
   unfold check_entrypoints_aux, pair_entrypoints in Heqo0. MonadInv.
@@ -2551,9 +2523,9 @@ Qed.
 
 Lemma find_comp_translated:
   forall vf,
-    Genv.find_comp ge vf = Genv.find_comp tge vf.
+    Genv.find_comp_in_genv ge vf = Genv.find_comp_in_genv tge vf.
 Proof.
-  eapply (Genv.match_genvs_find_comp TRANSF).
+  eapply (Genv.match_genvs_find_comp_in_genv TRANSF).
 Qed.
 
 Lemma exec_moves:
@@ -2653,15 +2625,15 @@ Inductive match_states: RTL.state -> LTL.state -> Prop :=
       match_states (RTL.State s f sp pc rs m)
                    (LTL.State ts tf sp pc ls m')
   | match_states_call:
-      forall s f args m ts tf ls m'
+      forall s f args m ts tf ls m' cp
         (STACKS: match_stackframes s ts (funsig tf))
         (FUN: transf_fundef f = OK tf)
         (ARGS: Val.lessdef_list args (map (fun p => Locmap.getpair p ls) (loc_arguments (funsig tf))))
         (AG: agree_callee_save (parent_locset ts) ls)
         (MEM: Mem.extends m m')
         (WTARGS: Val.has_type_list args (sig_args (funsig tf))),
-      match_states (RTL.Callstate s f args m)
-                   (LTL.Callstate ts tf (funsig tf) ls m')
+      match_states (RTL.Callstate s f args m cp)
+                   (LTL.Callstate ts tf (funsig tf) ls m' cp)
   | match_states_return:
       forall s res m ts ls m' sg cp
         (STACKS: match_stackframes s ts sg)
@@ -2864,7 +2836,7 @@ Proof.
   exploit eval_addressing_lessdef. eexact LD3.
   eapply eval_offset_addressing; eauto; apply Archi.splitlong_ptr32; auto.
   intros [a2' [F2 G2]].
-  assert (LOADX: exists v2'', Mem.loadv Mint32 m' a2' (Some (comp_of f)) = Some v2'' /\ Val.lessdef v2' v2'').
+  assert (LOADX: exists v2'', Mem.loadv Mint32 m' a2' (comp_of f) = Some v2'' /\ Val.lessdef v2' v2'').
   { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G2]). }
   destruct LOADX as (v2'' & LOAD2' & LD4).
   set (ls4 := Locmap.set (R dst2') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls3)).
@@ -2935,7 +2907,7 @@ Proof.
   exploit eval_addressing_lessdef. eexact LD1.
   eapply eval_offset_addressing; eauto; apply Archi.splitlong_ptr32; auto.
   intros [a1' [F1 G1]].
-  assert (LOADX: exists v2'', Mem.loadv Mint32 m' a1' (Some (comp_of f)) = Some v2'' /\ Val.lessdef v2' v2'').
+  assert (LOADX: exists v2'', Mem.loadv Mint32 m' a1' (comp_of f) = Some v2'' /\ Val.lessdef v2' v2'').
   { discriminate || (eapply Mem.loadv_extends; [eauto|eexact LOAD2|eexact G1]). }
   destruct LOADX as (v2'' & LOAD2' & LD2).
   set (ls2 := Locmap.set (R dst') v2'' (undef_regs (destroyed_by_load Mint32 addr2) ls1)).
@@ -3173,7 +3145,7 @@ Proof.
   }
   traceEq. traceEq.
   exploit analyze_successors; eauto. simpl. left; eauto. intros [enext [U V]].
-  rewrite <- SIG.
+  rewrite <- SIG. rewrite comp_transf_function; eauto.
   econstructor; eauto.
   {
   econstructor; eauto.
@@ -3210,7 +3182,7 @@ Proof.
   rewrite <- comp_transf_function; eauto.
   destruct (transf_function_inv _ _ FUN); auto.
   eauto. traceEq.
-  rewrite <- SIG'.
+  rewrite <- SIG'. rewrite comp_transf_function; eauto.
   econstructor; eauto.
   eapply match_stackframes_change_sig; eauto. rewrite SIG'. rewrite e0. decEq.
   destruct (transf_function_inv _ _ FUN); auto.
@@ -3234,8 +3206,9 @@ Proof.
   eapply star_trans. eexact A1.
   eapply star_left. econstructor.
   eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  rewrite <- comp_transf_function; eauto.
   eapply external_call_symbols_preserved. apply senv_preserved. eauto.
-  eauto. rewrite <- comp_transf_function; eauto.
+  eauto.
   eapply star_right. eexact A3.
   econstructor.
   reflexivity. reflexivity. reflexivity. traceEq.
@@ -3395,7 +3368,7 @@ Proof.
   intros. inv H.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   exploit sig_function_translated; eauto. intros SIG.
-  exists (LTL.Callstate nil tf signature_main (Locmap.init Vundef) m0); split.
+  exists (LTL.Callstate nil tf signature_main (Locmap.init Vundef) m0 top); split.
   econstructor; eauto.
   eapply (Genv.init_mem_transf_partial TRANSF); eauto.
   rewrite symbols_preserved.
@@ -3438,6 +3411,7 @@ Proof.
   set (ms := fun s s' => wt_state s /\ match_states s s').
   eapply forward_simulation_plus with (match_states := ms).
 - apply senv_preserved.
+- apply senv_preserved.
 - intros. exploit initial_states_simulation; eauto. intros [st2 [A B]].
   exists st2; split; auto. split; auto.
   apply wt_initial_state with (p := prog); auto. exact wt_prog.

backend/Asmexpandaux.ml

@@ -26,7 +26,7 @@ let emit i = current_code := i :: !current_code
 
 (* Generation of fresh labels *)
 
-let dummy_function = { fn_comp = privileged_compartment; fn_code = []; fn_sig = signature_main }
+let dummy_function = { fn_comp = COMP.top; fn_code = []; fn_sig = signature_main }
 let current_function = ref dummy_function
 let next_label = ref (None: label option)
 
@@ -95,10 +95,10 @@ let translate_annot sp preg_to_dwarf annot =
   | [] -> None
   | a::_ -> aux a)
 
-let builtin_nop cp =
+let builtin_nop =
   let signature ={sig_args = []; sig_res = Tvoid; sig_cc = cc_default} in
   let name = coqstring_of_camlstring "__builtin_nop" in
-  Pbuiltin(EF_builtin(cp,name,signature),[],BR_none)
+  Pbuiltin(EF_builtin(name,signature),[],BR_none)
 
 let rec lbl_follows = function
   | Pbuiltin (EF_debug _, _, _):: rest ->
@@ -115,7 +115,7 @@ let expand_debug id sp preg simple l =
     | Some lbl -> lbl in
   let rec  aux lbl scopes = function
     | [] -> ()
-    | (Pbuiltin(EF_debug (_cp,kind,txt,_x),args,_) as i)::rest ->
+    | (Pbuiltin(EF_debug (kind,txt,_x),args,_) as i)::rest ->
         let kind = (P.to_int kind) in
         begin
           match kind with
@@ -152,16 +152,16 @@ let expand_debug id sp preg simple l =
           | _ ->
               aux None scopes rest
         end
-    | (Pbuiltin(EF_annot (cp, kind, _, _),_,_) as annot)::rest ->
+    | (Pbuiltin(EF_annot (kind, _, _),_,_) as annot)::rest ->
       simple annot;
       if P.to_int kind = 2 && lbl_follows rest then
-        simple (builtin_nop cp);
+        simple (builtin_nop);
       aux None scopes rest
     | (Plabel lbl)::rest -> simple (Plabel lbl); aux (Some lbl) scopes rest
     | i::rest -> simple i; aux None scopes rest in
   (* We need to move all closing debug annotations before the last real statement *)
   let rec move_debug acc bcc = function
-    | (Pbuiltin(EF_debug (_cp,kind,_,_),_,_) as i)::rest ->
+    | (Pbuiltin(EF_debug (kind,_,_),_,_) as i)::rest ->
         let kind = (P.to_int kind) in
         if kind = 1 then
           move_debug acc (i::bcc) rest (* Do not move debug line *)
@@ -173,10 +173,10 @@ let expand_debug id sp preg simple l =
 
 let expand_simple simple l =
   let rec aux = function
-   | (Pbuiltin(EF_annot (cp, kind, _, _),_,_) as annot)::rest ->
+   | (Pbuiltin(EF_annot (kind, _, _),_,_) as annot)::rest ->
      simple annot;
      if P.to_int kind = 2 && lbl_follows rest then
-       simple (builtin_nop cp);
+       simple (builtin_nop);
      aux rest
    | i::rest -> simple i; aux rest
    | [] -> () in

backend/Asmgenproof0.v

@@ -929,11 +929,11 @@ Lemma exec_straight_steps_1:
   forall s c rs m c' rs' m',
   exec_straight c rs m c' rs' m' ->
   list_length_z (fn_code fn) <= Ptrofs.max_unsigned ->
-  forall b ofs,
+  forall b ofs cp,
   rs#PC = Vptr b ofs ->
   Genv.find_funct_ptr ge b = Some (Internal fn) ->
   code_tail (Ptrofs.unsigned ofs) (fn_code fn) c ->
-  plus step ge (State s rs m) E0 (State s rs' m').
+  plus step ge (State s rs m cp) E0 (State s rs' m' (comp_of fn)).
 Proof.
   induction 1; intros.
   apply plus_one.

backend/CSE.v

@@ -471,16 +471,16 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
           empty_numbering
       | Ibuiltin ef args res s =>
           match ef with
-          | EF_external _ _ _ | EF_runtime _ _ _ | EF_malloc _ | EF_free _ | EF_inline_asm _ _ _ _ =>
+          | EF_external _ _ | EF_runtime _ _ | EF_malloc | EF_free | EF_inline_asm _ _ _ =>
               empty_numbering
-          | EF_vstore _ _ =>
+          | EF_vstore _ =>
               set_res_unknown (kill_all_loads before) res
-          | EF_builtin cp name sg =>
-              match lookup_builtin_function name cp sg with
+          | EF_builtin name sg =>
+              match lookup_builtin_function name sg with
               | Some bf => set_res_unknown before res
               | None    => set_res_unknown (kill_all_loads before) res
               end
-          | EF_memcpy _ sz al =>
+          | EF_memcpy sz al =>
               match args with
               | dst :: src :: nil =>
                   let app := approx!!pc in
@@ -491,7 +491,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
               | _ =>
                   empty_numbering
               end
-          | EF_vload _ _ | EF_annot _ _ _ _ | EF_annot_val _ _ _ _ | EF_debug _ _ _ _ =>
+          | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ =>
               set_res_unknown before res
           end
       | Icond cond args ifso ifnot =>
@@ -574,6 +574,15 @@ Definition transf_function (rm: romem) (f: function) : res function :=
            f.(fn_entrypoint))
   end.
 
+#[global] Instance comp_transf_function rm:
+  has_comp_transl_partial (transf_function rm).
+Proof.
+  unfold transf_function.
+  intros f ? H.
+  destruct analyze; try easy.
+  now inv H.
+Qed.
+
 Definition transf_fundef (rm: romem) (f: fundef) : res fundef :=
   AST.transf_partial_fundef (transf_function rm) f.