Library mcertikos.trap.TTrapArgCode3
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import TacticsForTesting.
Require Import XOmega.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import TTrapArg.
Require Import TrapGenSpec.
Require Import TTrapArgCSource2.
Require Import ObjTrap.
Require Import CommonTactic.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Module TTRAPARGCODE3.
Section WithPrimitives.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Section SYSGETC.
Let L: compatlayer (cdata RData) :=
serial_intr_disable ↦ gensem thread_serial_intr_disable_spec
⊕ serial_intr_enable ↦ gensem thread_serial_intr_enable_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ cons_buf_read ↦ gensem thread_cons_buf_read_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysGetcBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import TacticsForTesting.
Require Import XOmega.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import TTrapArg.
Require Import TrapGenSpec.
Require Import TTrapArgCSource2.
Require Import ObjTrap.
Require Import CommonTactic.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Module TTRAPARGCODE3.
Section WithPrimitives.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{single_oracle_prop: SingleOracleProp}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Let mem := mwd (cdata RData).
Context `{Hstencil: Stencil}.
Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.
Section SYSGETC.
Let L: compatlayer (cdata RData) :=
serial_intr_disable ↦ gensem thread_serial_intr_disable_spec
⊕ serial_intr_enable ↦ gensem thread_serial_intr_enable_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ cons_buf_read ↦ gensem thread_cons_buf_read_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysGetcBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
serial_intr_disable
Variable bserial_intr_disable: block.
Hypothesis hserial_intr_disable1 : Genv.find_symbol ge serial_intr_disable = Some bserial_intr_disable.
Hypothesis hserial_intr_disable2 : Genv.find_funct_ptr ge bserial_intr_disable = Some (External (EF_external serial_intr_disable (signature_of_type Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
Hypothesis hserial_intr_disable1 : Genv.find_symbol ge serial_intr_disable = Some bserial_intr_disable.
Hypothesis hserial_intr_disable2 : Genv.find_funct_ptr ge bserial_intr_disable = Some (External (EF_external serial_intr_disable (signature_of_type Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
serial_intr_enable
Variable bserial_intr_enable: block.
Hypothesis hserial_intr_enable1 : Genv.find_symbol ge serial_intr_enable = Some bserial_intr_enable.
Hypothesis hserial_intr_enable2 : Genv.find_funct_ptr ge bserial_intr_enable = Some (External (EF_external serial_intr_enable (signature_of_type Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
Hypothesis hserial_intr_enable1 : Genv.find_symbol ge serial_intr_enable = Some bserial_intr_enable.
Hypothesis hserial_intr_enable2 : Genv.find_funct_ptr ge bserial_intr_enable = Some (External (EF_external serial_intr_enable (signature_of_type Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
uctx_set_errno
Variable buctx_set_errno: block.
Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno = Some (External (EF_external uctx_set_errno (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno = Some (External (EF_external uctx_set_errno (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
uctx_set_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 = Some (External (EF_external uctx_set_retval1 (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 = Some (External (EF_external uctx_set_retval1 (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
cons_buf_read
Variable bcons_buf_read: block.
Hypothesis hcons_buf_read1 : Genv.find_symbol ge cons_buf_read = Some bcons_buf_read.
Hypothesis hcons_buf_read2 : Genv.find_funct_ptr ge bcons_buf_read = Some (External (EF_external cons_buf_read (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).
Lemma sys_getc_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
sys_getc_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_getc_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hspec Hinv.
functional inversion Hspec; subst.
esplit.
unfold sys_getc_body.
repeat vcgen.
Qed.
End SysGetcBody.
Theorem sys_getc_code_correct:
spec_le (sys_getc ↦ sys_getc_spec_low) (〚sys_getc ↦ f_sys_getc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sys_getc_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b3 Hb3fs Hb3fp b2 Hb2fs Hb2fp b4 Hb4fs Hb4fp m´0 labd labd0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_getc)
nil
(create_undef_temps (fn_temps f_sys_getc)))) H1.
Qed.
End SYSGETC.
Section SYSPUTC.
Let L: compatlayer (cdata RData) :=
uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ serial_intr_disable ↦ gensem thread_serial_intr_disable_spec
⊕ serial_intr_enable ↦ gensem thread_serial_intr_enable_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ serial_putc ↦ gensem thread_serial_putc_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysPutcBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis hcons_buf_read1 : Genv.find_symbol ge cons_buf_read = Some bcons_buf_read.
Hypothesis hcons_buf_read2 : Genv.find_funct_ptr ge bcons_buf_read = Some (External (EF_external cons_buf_read (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).
Lemma sys_getc_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
sys_getc_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_getc_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hspec Hinv.
functional inversion Hspec; subst.
esplit.
unfold sys_getc_body.
repeat vcgen.
Qed.
End SysGetcBody.
Theorem sys_getc_code_correct:
spec_le (sys_getc ↦ sys_getc_spec_low) (〚sys_getc ↦ f_sys_getc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sys_getc_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b3 Hb3fs Hb3fp b2 Hb2fs Hb2fp b4 Hb4fs Hb4fp m´0 labd labd0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_getc)
nil
(create_undef_temps (fn_temps f_sys_getc)))) H1.
Qed.
End SYSGETC.
Section SYSPUTC.
Let L: compatlayer (cdata RData) :=
uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ serial_intr_disable ↦ gensem thread_serial_intr_disable_spec
⊕ serial_intr_enable ↦ gensem thread_serial_intr_enable_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ serial_putc ↦ gensem thread_serial_putc_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysPutcBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
serial_intr_disable
Variable bserial_intr_disable: block.
Hypothesis hserial_intr_disable1 : Genv.find_symbol ge serial_intr_disable = Some bserial_intr_disable.
Hypothesis hserial_intr_disable2 : Genv.find_funct_ptr ge bserial_intr_disable = Some (External (EF_external serial_intr_disable (signature_of_type Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
Hypothesis hserial_intr_disable1 : Genv.find_symbol ge serial_intr_disable = Some bserial_intr_disable.
Hypothesis hserial_intr_disable2 : Genv.find_funct_ptr ge bserial_intr_disable = Some (External (EF_external serial_intr_disable (signature_of_type Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
serial_intr_enable
Variable bserial_intr_enable: block.
Hypothesis hserial_intr_enable1 : Genv.find_symbol ge serial_intr_enable = Some bserial_intr_enable.
Hypothesis hserial_intr_enable2 : Genv.find_funct_ptr ge bserial_intr_enable = Some (External (EF_external serial_intr_enable (signature_of_type Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
Hypothesis hserial_intr_enable1 : Genv.find_symbol ge serial_intr_enable = Some bserial_intr_enable.
Hypothesis hserial_intr_enable2 : Genv.find_funct_ptr ge bserial_intr_enable = Some (External (EF_external serial_intr_enable (signature_of_type Tnil Tvoid cc_default)) Tnil Tvoid cc_default).
uctx_set_errno
Variable buctx_set_errno: block.
Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno = Some (External (EF_external uctx_set_errno (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.
Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno = Some (External (EF_external uctx_set_errno (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
uctx_arg2
Variable buctx_arg2: block.
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 = Some (External (EF_external uctx_arg2 (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).
Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 = Some (External (EF_external uctx_arg2 (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).
serial_putc
Variable bserial_putc: block.
Hypothesis hserial_putc1 : Genv.find_symbol ge serial_putc = Some bserial_putc.
Hypothesis hserial_putc2 : Genv.find_funct_ptr ge bserial_putc = Some (External (EF_external serial_putc (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Lemma sys_putc_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
sys_putc_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_putc_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hspec Hinv.
functional inversion Hspec; subst.
esplit.
unfold sys_putc_body.
repeat vcgen. rewrite Int.unsigned_repr. reflexivity. omega.
rewrite Int.unsigned_repr. eapply H3. omega.
Qed.
End SysPutcBody.
Theorem sys_putc_code_correct:
spec_le (sys_putc ↦ sys_putc_spec_low) (〚sys_putc ↦ f_sys_putc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sys_putc_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp b0 Hb0fs Hb0fp b4 Hb4fs Hb4fp m´0 labd labd0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_putc)
nil
(create_undef_temps (fn_temps f_sys_putc)))) H0.
Qed.
End SYSPUTC.
End WithPrimitives.
End TTRAPARGCODE3.
Hypothesis hserial_putc1 : Genv.find_symbol ge serial_putc = Some bserial_putc.
Hypothesis hserial_putc2 : Genv.find_funct_ptr ge bserial_putc = Some (External (EF_external serial_putc (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Lemma sys_putc_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
sys_putc_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_putc_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros m d d´ env le Henv Hspec Hinv.
functional inversion Hspec; subst.
esplit.
unfold sys_putc_body.
repeat vcgen. rewrite Int.unsigned_repr. reflexivity. omega.
rewrite Int.unsigned_repr. eapply H3. omega.
Qed.
End SysPutcBody.
Theorem sys_putc_code_correct:
spec_le (sys_putc ↦ sys_putc_spec_low) (〚sys_putc ↦ f_sys_putc 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sys_putc_body_correct s (Genv.globalenv p) makeglobalenv
b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp b0 Hb0fs Hb0fp b4 Hb4fs Hb4fp m´0 labd labd0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_putc)
nil
(create_undef_temps (fn_temps f_sys_putc)))) H0.
Qed.
End SYSPUTC.
End WithPrimitives.
End TTRAPARGCODE3.