Library liblayers.compat.CompatClightSem

Building Clight programs

How to construct a C signature from an assembly signature for assembly primitives

Definition type_of_typ (t: AST.typ): Ctypes.type :=
  match t with
    | AST.Tsingle ⇒ Ctypes.Tfloat Ctypes.F32 Ctypes.noattr
    | AST.Tfloat ⇒ Ctypes.Tfloat Ctypes.F64 Ctypes.noattr
    | AST.Tlong ⇒ Ctypes.Tlong Ctypes.Signed Ctypes.noattr
    | AST.Tint ⇒ Ctypes.Tint Ctypes.I32 Ctypes.Signed Ctypes.noattr
  end.

Definition type_of_opttyp (t: option AST.typ): Ctypes.type :=
  match t with
    | Some t´ ⇒ type_of_typ t´
    | None ⇒ Tvoid
  end.

Fixpoint typelist_of_typlist (l: list AST.typ): typelist :=
  match l with
    | nil ⇒ Ctypes.Tnil
    | t :: l´ ⇒ Ctypes.Tcons (type_of_typ t) (typelist_of_typlist l´)
  end.

Lemma typ_of_type_of_typ t:
  typ_of_type (type_of_typ t) = t.
Proof.
  destruct t; reflexivity.
Qed.

Lemma opttyp_of_type_of_opttyp t:
  opttyp_of_type (type_of_opttyp t) = t.
Proof.
  destruct t; try reflexivity.
  destruct t; reflexivity.
Qed.

Lemma typlist_of_typelist_of_typlist l:
  typlist_of_typelist (typelist_of_typlist l) = l.
Proof.
  induction l; simpl; f_equal; eauto using typ_of_type_of_typ.
Qed.

Lemma signature_of_type_correct s:
  signature_of_type (typelist_of_typlist (AST.sig_args s)) (type_of_opttyp (AST.sig_res s)) (AST.sig_cc s) = s.
Proof.
  unfold signature_of_type.
  destruct s; simpl.
  rewrite typlist_of_typelist_of_typlist.
  rewrite opttyp_of_type_of_opttyp.
  reflexivity.
Qed.

Definition make_external {D} (i: ident) (σ: compatsem D): Clight.fundef :=
  match σ with
    | inl σe ⇒
      External
        (EF_external i (sextcall_sig σe))
        (sextcall_args σe)
        (sextcall_res σe)
        (sextcall_cc σe)
    | inr σp ⇒
      External
        (EF_external i (sprimcall_sig σp))
        (typelist_of_typlist (AST.sig_args (sprimcall_sig σp)))
        (type_of_opttyp (AST.sig_res (sprimcall_sig σp)))
        (AST.sig_cc (sprimcall_sig σp))
  end.

Global Instance make_clight_fundef_varinfo_ops:
  ProgramFormatOps Clight.function Ctypes.type Clight.fundef Ctypes.type :=
  {
    make_internal κ := OK (Clight.Internal κ);
    make_external D i σ := OK (make_external i σ);
    make_varinfo := (fun x ⇒ x)
  }.

Global Instance make_clight_fundef_varinfo_prf:
  ProgramFormat Clight.function Ctypes.type Clight.fundef Ctypes.type.
Proof.
  constructor.
  × intro D. intros i ? ?; subst. intro σ1. intro σ2. intro LE.
    simpl.
    unfold make_external.
    inversion LE; subst.
    + destruct H as [[Hstep Hsig Hvalid] Hinvs].
      destruct x; simpl in *; subst.
      destruct y0; simpl in *; subst.
      unfold sextcall_sig, sextcall_args, sextcall_res, sextcall_cc.
      rewrite !Hsig.
      reflexivity.
    + destruct H as [[Hstep Hsig Hvalid] Hinvs].
      simpl.
      rewrite !Hsig.
      reflexivity.
Qed.

Context `{mkp_ops: !MakeProgramOps _ _ _ _}.
Context `{Hmkp: !MakeProgram _ _ _ _}.

Semantics of internal functions

Definition clight_step {D} (M: cmodule) (L: compatlayer D) i f s (WB: block → Prop) vargs m vres m´ :=
  ∃ ge b,
    make_globalenv s M L = ret ge ∧
    Genv.find_symbol ge i = Some b ∧
    Genv.find_funct_ptr ge b = Some (Internal f) ∧
    star (Clight.step2 (compiler_config_ops := compatlayer_compiler_config_ops L)
                       (WB := Events.writable_block_with_init_mem m))
         ge
         (Callstate (Internal f) vargs Kstop m) E0
         (Returnstate vres Kstop m´).

Local Existing Instance extcall_invariants_defined_dec.
Local Existing Instance primcall_invariants_defined_dec.

Local Existing Instance prim_valid_dec.

Definition clight_info {D} (M: cmodule) (L: compatlayer D) i f: sextcall_info :=
  {|
    sextcall_step := clight_step M L i f ;
    sextcall_csig :=
      {|
        csig_args := type_of_params (fn_params f );
        csig_res := fn_return f ;
        csig_cc := fn_callconv f
      |};
    sextcall_valid s :=
      if decide (ExtcallInvariantsDefined L ) then
        if decide (PrimcallInvariantsDefined L ) then
          if decide (get_layer_prim_valid L s ) then
            match make_program s M L with
              | OK _ ⇒ true
              | _ ⇒ false
            end
          else false
        else false
      else false
  |}.

Definition sextcall_invs_defined {D} (f: res (option (compatsem D))): bool :=
  match f with
    | OK (Some (inl σ)) ⇒
      match sextcall_invs _ σ with
        | Error _ ⇒ false
        | _ ⇒ true
      end
    | _ ⇒ true
  end.

Definition sextcall_invs_defined_all {D} (L: compatlayer D): Prop :=
  ∀ i: ident, (fun f ⇒ sextcall_invs_defined f = true) (get_layer_primitive (primsem := compatsem) i L).

XXX: need to know that the layer preserves invariants asa a premise.

Definition clight_primsem D (M: cmodule) (L: compatlayer D) i f: compatsem D :=
  inl {|
    sextcall_primsem_step := clight_info M L i f ;
    sextcall_props := Error nil ;
    sextcall_invs := Error nil

  |}.

Semantics of whole modules

Local Instance clight_ptree_sem_ops: FunctionSemanticsOps _ _ _ _ _ _ :=
  {
    semof_fundef D M L i f := OK (clight_primsem D M L i f)
  }.

NB: we're not going to prove this before POPL. Instead, we will compile everything by function, and so won't need a Semantics instance at all.

Global Instance clight_semantics_ops:
SemanticsOps _ _ _ _ cmodule compatlayer :=
compat_semantics_ops.

In fact, we already need monotonicity wrt. cl_le

Lemma make_program_monotonic_exists {D: compatdata}
      `{L1: compatlayer D} `{L2: compatlayer D}:
  ∀ M1 M2 s p,
    M1 ≤ M2 →
    L1 ≤ L2 →
    make_program s M2 L2 = OK p →
    ∃ p´, make_program s M1 L1 = OK p´.
Proof.
  intros M1 M2 s p LEM SIM MKP.
  assert (LEP: res_le program_le (make_program s M1 L1) (make_program s M2 L2))
    by (eapply make_program_monotonic; eauto; typeclasses eauto).
  rewrite MKP in LEP.
  inversion LEP; subst.
  eauto.
Qed.

Lemma clight_semantics_monotonic
  {NOREPET: CompCertBuiltins.BuiltinIdentsNorepet}
  {D}:
  @Proper (cmodule → compatlayer D → compatlayer D ) ((≤) ==> (≤) ==> (≤)) 〚-〛.
Proof.
    eapply compat_semantics_monotonic.
    clear D.
    intros D M1 M2 M_le L1 L2 L_le i f.
    econstructor; simpl.
    econstructor; simpl.
    econstructor; simpl; [| econstructor; reflexivity].
    econstructor; simpl; [| reflexivity |].
    + intros.
      destruct (Decision.decide (ExtcallInvariantsDefined L2)); try discriminate.
      destruct (Decision.decide (PrimcallInvariantsDefined L2)); try discriminate.
      destruct (Decision.decide (get_layer_prim_valid L2 s)); try discriminate.
      match goal with H: match ?m with | OK _ ⇒ true | Error _ ⇒ false end = true |- _ ⇒
                      destruct m eqn:Hmake; try discriminate
      end.
      assert (Hmake_: make_program s M2 L2 = OK p0) by assumption.
      assert (OKmake: isOK (make_program s M2 L2)).
      {
        rewrite Hmake_.
        esplit; eauto.
      }
      assert (OKLayer: LayerOK L2).
      {
        eapply make_program_layer_ok; eauto.
      }
      assert (Hge´: ∃ ge´, make_globalenv s M2 L2 = ret ge´).
      {
        eapply make_program_make_globalenv in Hmake.
        eauto.
      }
      destruct Hge´ as [ge´ Hge´].
      destruct 1
        as (ge & b & Hge & Hsymb & Hfunc & Hstar).

      assert (Hgele: res_le (≤) (make_globalenv s M1 L1) (make_globalenv s M2 L2)).
      {
        exploit @make_globalenv_monotonic; eauto.
      }
      rewrite Hge´ in Hgele.
      inversion Hgele; subst.
      replace x with ge in × by (vm_compute in Hge, H0; congruence).
      generalize (fun b f ⇒ genv_le_find_funct_ptr_some ge ge´ b f H2).
      intro HF.

      econstructor; eauto.
      esplit. split.
      { eassumption. }
      split.
      {
       erewrite stencil_matches_symbols in Hsymb by eauto using make_globalenv_stencil_matches.
       erewrite stencil_matches_symbols by eauto using make_globalenv_stencil_matches.
       eassumption.
      }
      split; eauto.
      eapply (@ClightXFacts.star2_mono NOREPET _ _ (mwd_memory_model D)
                                       (compatlayer_extcall_ops_x L1) (compatlayer_extcall_ops_x L2)
                                       ge ge´); eauto.
      × intro.
        erewrite stencil_matches_symbols by eauto using make_globalenv_stencil_matches.
        erewrite stencil_matches_symbols by eauto using make_globalenv_stencil_matches.
        reflexivity.
      × intro.
        erewrite stencil_matches_volatile by eauto using make_globalenv_stencil_matches.
        erewrite stencil_matches_volatile by eauto using make_globalenv_stencil_matches.
        reflexivity.
      ×
        erewrite stencil_matches_genv_next by eauto using make_globalenv_stencil_matches.
        erewrite stencil_matches_genv_next by eauto using make_globalenv_stencil_matches.
        reflexivity.
      × intros until m´.
        destruct (ClightXFacts.builtin_is_enabled (compiler_config_ops := compatlayer_compiler_config_ops L1) (refl_equal _) ef).
        {
          exploit (@ClightXFacts.external_call_spec _ _ _ (compatlayer_compiler_config_ops L2)); eauto.
          { eapply CompCertBuiltins.builtin_functions_properties; eauto. }
          { constructor; intros; contradiction. }
          intro PROP.
          intro K.
          eapply @ec_symbols_preserved.
          { eassumption. }
          {
            instantiate (1 := ge). intro.
            erewrite stencil_matches_symbols by eauto using make_globalenv_stencil_matches.
            erewrite stencil_matches_symbols by eauto using make_globalenv_stencil_matches.
            reflexivity.
          }
          {
            intro.
            erewrite stencil_matches_volatile by eauto using make_globalenv_stencil_matches.
            erewrite stencil_matches_volatile by eauto using make_globalenv_stencil_matches.
            reflexivity.
          }
          {
            erewrite stencil_matches_genv_next by eauto using make_globalenv_stencil_matches.
            erewrite stencil_matches_genv_next by eauto using make_globalenv_stencil_matches.
            reflexivity.
          }
          eapply @ec_writable_block_weak.
          { eassumption. }
          { instantiate (1 := writable_block a1 ge).
            destruct ef; try assumption.
            contradiction.
          }
          unfold writable_block.
          erewrite stencil_matches_genv_next by eauto using make_globalenv_stencil_matches.
          erewrite stencil_matches_genv_next by eauto using make_globalenv_stencil_matches.
          tauto.
        }
        destruct ef; simpl in n; try (exfalso; tauto).
        destruct 1.
        destruct H1.
        generalize (get_layer_primitive_sim_monotonic _ _ id name _ _ L_le).
        rewrite H1.
        inversion 1; subst.
        {
          inversion H7; subst.
          destruct H3
          as (st & PR & MATCH & HPRIM & ? & ? & ?); subst.
          inversion H8; subst.
          replace st with s in × by eauto using stencil_matches_unique, make_globalenv_stencil_matches.
          revert HPRIM.
          unfold writable_block.
          erewrite stencil_matches_genv_next by eauto using make_globalenv_stencil_matches.
          erewrite stencil_matches_genv_next by eauto using make_globalenv_stencil_matches.
          intros.
          esplit.
          split; eauto.
          esplit.
          ∃ y.
          split.
          { eapply make_globalenv_stencil_matches; eauto. }
          split.
          {
            eapply sextcall_info_le_sem.
            { eapply sextcall_primsem_le_step; eauto. }
            { symmetry in H6. exact (g _ _ H6). }
            assumption.
          }
          split; auto.
          split; auto.
          generalize (sextcall_info_le_sig _ _ (sextcall_primsem_le_step _ _ H5)).
          unfold sextcall_sig. congruence.
        }
        exfalso.
        destruct (OKLayer name) as [[σ Hσ] _ _].
        simpl in Hσ.
        rewrite Hσ in H7.
        discriminate.
    + intros.
      destruct (Decision.decide (ExtcallInvariantsDefined L2)); try discriminate.
      destruct (Decision.decide (PrimcallInvariantsDefined L2)); try discriminate.
      destruct (Decision.decide (get_layer_prim_valid L2 s)); try discriminate.
      assert (Hmake: isOK (make_program s M2 L2)).
      {
        match goal with H: match ?m with | OK _ ⇒ true | Error _ ⇒ false end = true |- _ ⇒
                        destruct m eqn:Hmake; try discriminate
        end.
        assert (Hmake_: make_program s M2 L2 = OK p0) by assumption.
        rewrite Hmake_. unfold isOK. eauto.
      }
      assert (OKLayer: LayerOK L2).
      {
        eapply make_program_layer_ok; eauto.
      }
      destruct Hmake as [pr Hmake].
      destruct (Decision.decide (ExtcallInvariantsDefined L1)).
      destruct (Decision.decide (PrimcallInvariantsDefined L1)).
      destruct (Decision.decide (get_layer_prim_valid L1 s)).
      × destruct (make_program_monotonic_exists (L1:=L1) (L2:=L2) M1 M2 s pr); eauto 1.
        rewrite H0. reflexivity.
      × elim n.
        eapply (cl_le_get_layer_prim_valid _ L_le); try eassumption.
      ×
        elim n.
        eapply (cl_le_invs_prim _ L_le); eassumption.
      ×
        elim n.
        eapply (cl_le_invs_ext _ L_le); eassumption.
Qed.

The following are no longer needed

Lemma clight_globvar_le {D} (L: _ D) (i: ident) (t: AST.globvar Ctypes.type): i ↦ t ≤ 〚i ↦ t〛 L. Proof.

Lemma clight_vertical_composition {D} (L: _ D) M1 M2: 〚 M1 〛 ( (〚 M2 〛 L ) ⊕ L) ≤ 〚 M1 ⊕ M2 〛 L. Proof.

Relate to ClightBigstepX

Inductive primitive_le {D}: relation (compatsem D) :=
| primitive_le_sextcall:
    ∀ (σ1 σ2: sextcall_primsem D)
           (VALID: ∀ s, sextcall_valid σ2 s = true → sextcall_valid σ1 s = true)
           (SIG: sextcall_sig σ2 = sextcall_sig σ1)
           (SEM: ∀ m,
                   high_level_invariant (snd m) →
                   ∀ (s: stencil),
                     sextcall_valid σ2 s = true →
                     ∀ WB vargs vres m´,
                       sextcall_step σ1 s WB vargs m vres m´ →
                       sextcall_step σ2 s WB vargs m vres m´),
      primitive_le (compatsem_inl σ1) (compatsem_inl σ2).

Record spec_le {D} (L1 L2: compatlayer D): Prop :=
  {
    spec_le_primitive:
      ∀ i,
        res_le (option_le primitive_le) (get_layer_primitive i L1) (get_layer_primitive i L2)
    ;
    spec_le_globalvars:
      ∀ i,
        res_le (option_le eq) (get_layer_globalvar i L1) (get_layer_globalvar i L2)
    ;
    spec_le_load:
      res_le (option_le eq) (cl_exec_load L1) (cl_exec_load L2)
    ;
    spec_le_store:
      res_le (option_le eq) (cl_exec_store L1) (cl_exec_store L2)

  }.

Lemma clight_sem_intro {D} (i: ident) (f: Clight.function) (L: compatlayer D) (σ: sextcall_primsem D):
  (∀ s WB vargs m vres m´ p,
     let ec_ops := compatlayer_extcall_ops L in
     let cc_ops := compatlayer_compiler_config_ops L in
     let WRITABLE_BLOCK_OPS := EventsX.writable_block_ops m in
     let WRITABLE_BLOCK_ALLOW_GLOBALS := EventsX.Hwritable_block_allow_globals m in
     sextcall_step σ s WB vargs m vres m´ →
     make_program s (i ↦ f) L = ret p →
     (high_level_invariant (snd m) →
      bigstep_function_terminates2 p i (sextcall_sig σ) vargs m E0 vres m´)) →

NB: we could do with a res_le version of compat_semantics_spec_some as well.

  ∀ NOCONFLICT: get_layer_primitive i L = OK None,
  ∀ VALID: ∀ s p, make_program s (i ↦ f) L = ret p → sextcall_valid σ s = true,
  ∀ SIG: sextcall_sig σ = Ctypes.signature_of_type (type_of_params (fn_params f)) (fn_return f) (fn_callconv f),
  spec_le (i ↦ compatsem_inl σ) (〚i ↦ f 〛 L).
Proof.
  intros.
  constructor.
{
  intros.
  destruct (Coqlib.peq i0 i).
  × subst.
    rewrite get_layer_primitive_mapsto.
    generalize (get_module_function_mapsto i f).
    intro MODULE.
    pose proof (ptree_get_semof_primitive i (i ↦ f) L) as Hi.
    unfold cmodule; simpl in ×.
    rewrite Hi; clear Hi.
    unfold semof_function; simpl.
    get_module_normalize; monad_norm.
    repeat constructor.
    - simpl.
      intro s.
      destruct (decide (ExtcallInvariantsDefined L)); try discriminate.
      destruct (decide (PrimcallInvariantsDefined L)); try discriminate.
      destruct (decide (get_layer_prim_valid L s)); try discriminate.
      destruct (make_program s (i ↦ f) L) eqn:Heqr; simpl in *; try discriminate.
      eauto.
    - auto.
    - simpl.
      intros.
      destruct (decide (ExtcallInvariantsDefined L)) as [ Hext | ] ; try discriminate.
      destruct (decide (PrimcallInvariantsDefined L)) as [ Hprim | ]; try discriminate.
      destruct (decide (get_layer_prim_valid L s)) as [ Hlayerprim | ]; try discriminate.
      destruct (make_program _ _ _) eqn:MAKEPROG; try discriminate.
      generalize MAKEPROG.
      intro MAKEGENV.
      apply make_program_make_globalenv in MAKEGENV.
      generalize (H _ _ _ _ _ _ _ H2 MAKEPROG H0).
      revert MAKEGENV.
      pose proof Hmkp as Hmkp´.
      revert Hmkp´.
      clear.
      intros.
      inversion H; subst.
      unfold ge in ×. clear ge.
      assert (MAKEGENV´: (make_globalenv s (i ↦ f) L = ret (Genv.globalenv p))) by assumption.
      inv_make_globalenv MAKEGENV´.
      replace f0 with (Internal f) in × by congruence; clear f0.
      econstructor.
      esplit.
      split.
      eassumption.
      split.
      eassumption.
      split.
      assumption.
      eapply ClightBigstep.eval_funcall_steps; eauto.
      repeat constructor.
  ×
    rewrite get_layer_primitive_mapsto_other_primitive; eauto.
    apply lower_bound.
}
{
  intro i0.
  rewrite get_layer_globalvar_mapsto_primitive.
  match goal with
    | |- res_le _ _ ?x ⇒ destruct x as [ [ ? | ] | ?]
  end;
    repeat constructor.
}
{
  reflexivity.
}
{
  reflexivity.
}

Qed.

Lemma primitive_le_compatsem_le_right {D} (σ1 σ2 σ3: compatsem D):
  primitive_le σ1 σ2 →
  compatsem_le D σ2 σ3 →
  primitive_le σ1 σ3.
Proof.
  intros Hσ12 Hσ23.
  destruct Hσ12 as [σe1 σe2 Hvalid12 Hsig12 Hstep12].
  inversion Hσ23 as [σe2´ σe3 Hσe23 | ]; clear Hσ23; subst.
  destruct σe1 as [σe1 props1 invs1]; simpl in ×.
  destruct σe2 as [σe2 props2 invs2]; simpl in ×.
  destruct σe3 as [σe3 props3 invs3]; simpl in ×.
  destruct Hσe23 as [[Hstep23 Hsig23 Hvalid23] Hinvs23].
  constructor; simpl in *; try rel_auto.
  unfold sextcall_sig in ×. congruence.
Qed.

Lemma spec_le_right {D}
      (L1 L2 L3: _ D)
      (Hspec12: spec_le L1 L2)
      (Hle23: cl_sim _ _ id L2 L3)
:
  spec_le L1 L3.
Proof.
  destruct Hspec12 as [Hprim12 Hvar12 Hload12 Hstore12].
  destruct Hle23 as [Hbase23 Hload23 Hstore23].
  apply cl_le_layer_pointwise in Hbase23.
  destruct Hbase23 as [Hprim23 Hvar23].

  constructor.
{
  intros i.
  specialize (Hprim12 i); specialize (Hprim23 i).
  clear Hvar12 Hvar23 Hload12 Hload23 Hstore12 Hstore23.
  revert Hprim12 Hprim23.
  generalize (get_layer_primitive i L1), (get_layer_primitive i L2), (get_layer_primitive i L3).
  intros prim1 prim2 prim3 Hprim12 Hprim23.
  destruct Hprim23 as [σ2 σ3 Hσ23 Hσ3 | ]; try constructor.
  inversion Hprim12 as [σ1 σ2´ Hσ12 | σ1 Hσ1]; subst.
  constructor.
  destruct Hσ12 as [σ2 | σ1 σ2 Hσ12]; try constructor.
  inversion Hσ23 as [σ3´ | σ2´ σ3´ Hσ23´]; subst.
  constructor.
  eapply primitive_le_compatsem_le_right;
  eassumption.
}
{
  intro; etransitivity; eauto.
}
{
  etransitivity; eauto.
}
{
  etransitivity; eauto.
}

Qed.

End WITH_MEMORY_MODEL.