Library mcertikos.trap.TTrapCode_syscall_dispatch
*********************************************************************** * * * The CertiKOS Certified Kit Operating System * * * * The FLINT Group, Yale University * * * * Copyright The FLINT Group, Yale University. All rights reserved. * * This file is distributed under the terms of the Yale University * * Non-Commercial License Agreement. * * * ***********************************************************************
Require Import TacticsForTesting.
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 Clight.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Ctypes.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
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 DispatchGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import XOmega.
Require Import TTrapCSource.
Require Import AbstractDataType.
Require Import ObjArg.
Require Import ObjTrap.
Require Import ObjSyncIPC.
Require Export TrapPrimSemantics.
Require Import CommonTactic.
Module TTRAPCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
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 SYSCALLDISPATCHC.
Let L: compatlayer (cdata RData) := sys_proc_create ↦ trap_proccreate_compatsem trap_proc_create_spec
⊕ sys_get_quota ↦ gensem trap_get_quota_spec
⊕ sys_receive_chan ↦ gensem trap_receivechan_spec
⊕ sys_inject_event ↦ gensem trap_inject_event_spec
⊕ sys_check_int_shadow ↦ gensem trap_check_int_shadow_spec
⊕ sys_check_pending_event ↦ gensem trap_check_pending_event_spec
⊕ sys_intercept_int_window ↦ gensem trap_intercept_int_window_spec
⊕ sys_get_next_eip ↦ gensem trap_get_next_eip_spec
⊕ sys_get_reg ↦ gensem trap_get_reg_spec
⊕ sys_set_reg ↦ gensem trap_set_reg_spec
⊕ sys_set_seg ↦ gensem trap_set_seg_spec
⊕ sys_get_tsc_offset ↦ gensem trap_get_tsc_offset_spec
⊕ sys_set_tsc_offset ↦ gensem trap_set_tsc_offset_spec
⊕ sys_get_exitinfo ↦ gensem trap_get_exitinfo_spec
⊕ sys_handle_rdmsr ↦ gensem trap_handle_rdmsr_spec
⊕ sys_handle_wrmsr ↦ gensem trap_handle_wrmsr_spec
⊕ sys_mmap ↦ gensem trap_mmap_spec
⊕ sys_getc ↦ gensem sys_getc_spec
⊕ sys_putc ↦ gensem sys_putc_spec
⊕ uctx_arg1 ↦ gensem uctx_arg1_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SyscallDispatchCBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
sys_proc_create
Variable bsys_proc_create: block.
Hypothesis hsys_proc_create1 : Genv.find_symbol ge sys_proc_create = Some bsys_proc_create.
Hypothesis hsys_proc_create2 : Genv.find_funct_ptr ge bsys_proc_create = Some (External (EF_external sys_proc_create (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_get_quota
Variable bsys_get_quota: block.
Hypothesis hsys_get_quota1 : Genv.find_symbol ge sys_get_quota = Some bsys_get_quota.
Hypothesis hsys_get_quota2 : Genv.find_funct_ptr ge bsys_get_quota = Some (External (EF_external sys_get_quota (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_receive_chan
Variable bsys_receive_chan: block.
Hypothesis hsys_receive_chan1 : Genv.find_symbol ge sys_receive_chan = Some bsys_receive_chan.
Hypothesis hsys_receive_chan2 : Genv.find_funct_ptr ge bsys_receive_chan = Some (External (EF_external sys_receive_chan (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_inject_event
Variable bsys_inject_event: block.
Hypothesis hsys_inject_event1 : Genv.find_symbol ge sys_inject_event = Some bsys_inject_event.
Hypothesis hsys_inject_event2 : Genv.find_funct_ptr ge bsys_inject_event = Some (External (EF_external sys_inject_event (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_check_int_shadow
Variable bsys_check_int_shadow: block.
Hypothesis hsys_check_int_shadow1 : Genv.find_symbol ge sys_check_int_shadow = Some bsys_check_int_shadow.
Hypothesis hsys_check_int_shadow2 : Genv.find_funct_ptr ge bsys_check_int_shadow = Some (External (EF_external sys_check_int_shadow (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_check_pending_event
Variable bsys_check_pending_event: block.
Hypothesis hsys_check_pending_event1 : Genv.find_symbol ge sys_check_pending_event = Some bsys_check_pending_event.
Hypothesis hsys_check_pending_event2 : Genv.find_funct_ptr ge bsys_check_pending_event = Some (External (EF_external sys_check_pending_event (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_intercept_int_window
Variable bsys_intercept_int_window: block.
Hypothesis hsys_intercept_int_window1 : Genv.find_symbol ge sys_intercept_int_window = Some bsys_intercept_int_window.
Hypothesis hsys_intercept_int_window2 : Genv.find_funct_ptr ge bsys_intercept_int_window = Some (External (EF_external sys_intercept_int_window (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_get_next_eip
Variable bsys_get_next_eip: block.
Hypothesis hsys_get_next_eip1 : Genv.find_symbol ge sys_get_next_eip = Some bsys_get_next_eip.
Hypothesis hsys_get_next_eip2 : Genv.find_funct_ptr ge bsys_get_next_eip = Some (External (EF_external sys_get_next_eip (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_get_reg
Variable bsys_get_reg: block.
Hypothesis hsys_get_reg1 : Genv.find_symbol ge sys_get_reg = Some bsys_get_reg.
Hypothesis hsys_get_reg2 : Genv.find_funct_ptr ge bsys_get_reg = Some (External (EF_external sys_get_reg (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_set_reg
Variable bsys_set_reg: block.
Hypothesis hsys_set_reg1 : Genv.find_symbol ge sys_set_reg = Some bsys_set_reg.
Hypothesis hsys_set_reg2 : Genv.find_funct_ptr ge bsys_set_reg = Some (External (EF_external sys_set_reg (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_set_seg
Variable bsys_set_seg: block.
Hypothesis hsys_set_seg1 : Genv.find_symbol ge sys_set_seg = Some bsys_set_seg.
Hypothesis hsys_set_seg2 : Genv.find_funct_ptr ge bsys_set_seg = Some (External (EF_external sys_set_seg (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_get_tsc_offset
Variable bsys_get_tsc_offset: block.
Hypothesis hsys_get_tsc_offset1 : Genv.find_symbol ge sys_get_tsc_offset = Some bsys_get_tsc_offset.
Hypothesis hsys_get_tsc_offset2 : Genv.find_funct_ptr ge bsys_get_tsc_offset = Some (External (EF_external sys_get_tsc_offset (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_set_tsc_offset
Variable bsys_set_tsc_offset: block.
Hypothesis hsys_set_tsc_offset1 : Genv.find_symbol ge sys_set_tsc_offset = Some bsys_set_tsc_offset.
Hypothesis hsys_set_tsc_offset2 : Genv.find_funct_ptr ge bsys_set_tsc_offset = Some (External (EF_external sys_set_tsc_offset (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_get_exitinfo
Variable bsys_get_exitinfo: block.
Hypothesis hsys_get_exitinfo1 : Genv.find_symbol ge sys_get_exitinfo = Some bsys_get_exitinfo.
Hypothesis hsys_get_exitinfo2 : Genv.find_funct_ptr ge bsys_get_exitinfo = Some (External (EF_external sys_get_exitinfo (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_handle_rdmsr
Variable bsys_handle_rdmsr: block.
Hypothesis hsys_handle_rdmsr1 : Genv.find_symbol ge sys_handle_rdmsr = Some bsys_handle_rdmsr.
Hypothesis hsys_handle_rdmsr2 : Genv.find_funct_ptr ge bsys_handle_rdmsr = Some (External (EF_external sys_handle_rdmsr (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_handle_wrmsr
Variable bsys_handle_wrmsr: block.
Hypothesis hsys_handle_wrmsr1 : Genv.find_symbol ge sys_handle_wrmsr = Some bsys_handle_wrmsr.
Hypothesis hsys_handle_wrmsr2 : Genv.find_funct_ptr ge bsys_handle_wrmsr = Some (External (EF_external sys_handle_wrmsr (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_mmap
Variable bsys_mmap: block.
Hypothesis hsys_mmap1 : Genv.find_symbol ge sys_mmap = Some bsys_mmap.
Hypothesis hsys_mmap2 : Genv.find_funct_ptr ge bsys_mmap = Some (External (EF_external sys_mmap (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_getc
Variable bsys_getc: block.
Hypothesis hsys_getc1 : Genv.find_symbol ge sys_getc = Some bsys_getc.
Hypothesis hsys_getc2 : Genv.find_funct_ptr ge bsys_getc = Some (External (EF_external sys_getc (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
sys_putc
Variable bsys_putc: block.
Hypothesis hsys_putc1 : Genv.find_symbol ge sys_putc = Some bsys_putc.
Hypothesis hsys_putc2 : Genv.find_funct_ptr ge bsys_putc = Some (External (EF_external sys_putc (signature_of_type Tnil tvoid cc_default)) Tnil tvoid cc_default).
uctx_arg1
Variable buctx_arg1: block.
Hypothesis huctx_arg11 : Genv.find_symbol ge uctx_arg1 = Some buctx_arg1.
Hypothesis huctx_arg12 : Genv.find_funct_ptr ge buctx_arg1 = Some (External (EF_external uctx_arg1 (signature_of_type Tnil tint cc_default)) Tnil tint 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).
Lemma NSYS_NR_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
0 ≤ z ≤ Int.max_unsigned →
Syscall_Z2Num z = NSYS_NR →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H2.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
clear Hdestruct Hdestruct0 Hdestruct1 Hdestruct2 Hdestruct3 Hdestruct4 Hdestruct5 Hdestruct6 Hdestruct7 Hdestruct8 Hdestruct9 Hdestruct10 Hdestruct11 Hdestruct12 Hdestruct13 Hdestruct14 Hdestruct15 Hdestruct16 Hdestruct17 Hdestruct18 Hdestruct19 Hdestruct20 Hdestruct21 Hdestruct22 Hdestruct23 Hdestruct24 Hdestruct25 Hdestruct26.
clear n3 n4 n8.
change E0 with (E0 ** E0).
econstructor.
econstructor.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
change E0 with (E0 ** E0).
econstructor.
clear n26 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
clear n26 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
econstructor.
clear n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
clear n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
econstructor.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n0 n.
repeat vcgen.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n0 n.
repeat vcgen.
econstructor.
clear n26 n25 n24 n23 n22 n21 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
clear n26 n25 n24 n23 n22 n21 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
econstructor.
clear n26 n25 n24 n23 n22 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
clear n26 n25 n24 n23 n22 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
econstructor.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
econstructor.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
econstructor.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
repeat vcgen.
clear n0 n1 n5 n6 n9 n10 n11 n25 n26.
repeat vcgen.
assumption.
Qed.
Lemma NSYS_PUTS_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_PUTS →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_RING0_SPAWN_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_RING0_SPAWN →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_SPAWN_correct: ∀ m d d´ le z,
trap_proc_create_spec sc m d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_SPAWN →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_YIELD_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_YIELD →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_DISK_OP_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_DISK_OP →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_DISK_CAP_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_DISK_CAP →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_GET_TSC_PER_MS_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_GET_TSC_PER_MS →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_GET_TSC_OFFSET_correct: ∀ m d d´ le z,
trap_get_tsc_offset_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_GET_TSC_OFFSET →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_SET_TSC_OFFSET_correct: ∀ m d d´ le z,
trap_set_tsc_offset_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_SET_TSC_OFFSET →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_RUN_VM_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_RUN_VM →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_GET_EXITINFO_correct: ∀ m d d´ le z,
trap_get_exitinfo_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_GET_EXITINFO →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_MMAP_correct: ∀ m d d´ le z,
trap_mmap_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_MMAP →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_SET_REG_correct: ∀ m d d´ le z,
trap_set_reg_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_SET_REG →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_GET_REG_correct: ∀ m d d´ le z,
trap_get_reg_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_GET_REG →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_SET_SEG_correct: ∀ m d d´ le z,
trap_set_seg_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_SET_SEG →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_GET_NEXT_EIP_correct: ∀ m d d´ le z,
trap_get_next_eip_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_GET_NEXT_EIP →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_INJECT_EVENT_correct: ∀ m d d´ le z,
trap_inject_event_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_INJECT_EVENT →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_CHECK_PENDING_EVENT_correct: ∀ m d d´ le z,
trap_check_pending_event_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_CHECK_PENDING_EVENT →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_CHECK_INT_SHADOW_correct: ∀ m d d´ le z,
trap_check_int_shadow_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_CHECK_INT_SHADOW →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_INTERCEPT_INT_WINDOW_correct: ∀ m d d´ le z,
trap_intercept_int_window_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_INTERCEPT_INT_WINDOW →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_HANDLE_RDMSR_correct: ∀ m d d´ le z,
trap_handle_rdmsr_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_HANDLE_RDMSR →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_HANDLE_WRMSR_correct: ∀ m d d´ le z,
trap_handle_wrmsr_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_HANDLE_WRMSR →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_GET_QUOTA_correct: ∀ m d d´ le z,
trap_get_quota_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_GET_QUOTA →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_IS_CHAN_READY_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_IS_CHAN_READY →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_RECV_correct: ∀ m d d´ le z,
trap_receivechan_spec d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_RECV →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_SLEEP_correct: ∀ m d d´ le z,
uctx_set_errno_spec 3 d = Some d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_SLEEP →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
unfold Syscall_Z2Num in H1.
subdestruct.
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_PUTC_correct: ∀ m d d´ le z,
sys_putc_spec d = ret d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_PUTC →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
assert (z = 28).
{
unfold Syscall_Z2Num in H1.
subdestruct. assumption.
}
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma NSYS_GETC_correct: ∀ m d d´ le z,
sys_getc_spec d = ret d´ →
uctx_arg1_spec d = Some z →
Syscall_Z2Num z = NSYS_GETC →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold syscall_dispatch_c_body.
subst.
assert (z = 27).
{
unfold Syscall_Z2Num in H1.
subdestruct. assumption.
}
rewrite <- Int.unsigned_repr in H0 at 1.
esplit.
repeat vcgen.
omega.
Qed.
Lemma syscall_dispatch_c_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
sys_dispatch_c_spec sc m d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold sys_dispatch_c_spec in H0.
case_eq (uctx_arg1_spec d); intros; rewrite H in H0; try discriminate H0.
case_eq (zle_le 0 z Int.max_unsigned); intros; rewrite H2 in H0; try discriminate H0.
case_eq (Syscall_Z2Num z); intros; rewrite H3 in H0.
eapply NSYS_PUTS_correct; eauto.
eapply NSYS_RING0_SPAWN_correct; eauto.
eapply NSYS_SPAWN_correct; eauto.
eapply NSYS_YIELD_correct; eauto.
eapply NSYS_DISK_OP_correct; eauto.
eapply NSYS_DISK_CAP_correct; eauto.
eapply NSYS_GET_TSC_PER_MS_correct; eauto.
eapply NSYS_GET_TSC_OFFSET_correct; eauto.
eapply NSYS_SET_TSC_OFFSET_correct; eauto.
eapply NSYS_RUN_VM_correct; eauto.
eapply NSYS_GET_EXITINFO_correct; eauto.
eapply NSYS_MMAP_correct; eauto.
eapply NSYS_SET_REG_correct; eauto.
eapply NSYS_GET_REG_correct; eauto.
eapply NSYS_SET_SEG_correct; eauto.
eapply NSYS_GET_NEXT_EIP_correct; eauto.
eapply NSYS_INJECT_EVENT_correct; eauto.
eapply NSYS_CHECK_PENDING_EVENT_correct; eauto.
eapply NSYS_CHECK_INT_SHADOW_correct; eauto.
eapply NSYS_INTERCEPT_INT_WINDOW_correct; eauto.
eapply NSYS_HANDLE_RDMSR_correct; eauto.
eapply NSYS_HANDLE_WRMSR_correct; eauto.
eapply NSYS_GET_QUOTA_correct; eauto.
eapply NSYS_IS_CHAN_READY_correct; eauto.
eapply NSYS_RECV_correct; eauto.
eapply NSYS_SLEEP_correct; eauto.
eapply NSYS_PUTC_correct; eauto.
eapply NSYS_GETC_correct; eauto.
eapply NSYS_NR_correct; eauto.
Qed.
End SyscallDispatchCBody.
Theorem syscall_dispatch_c_code_correct:
spec_le (syscall_dispatch_C ↦ sys_dispatch_c_spec_low) (〚syscall_dispatch_C ↦ f_syscall_dispatch_c 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (syscall_dispatch_c_body_correct s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp b5 Hb5fs Hb5fp b6 Hb6fs Hb6fp b7 Hb7fs Hb7fp
b8 Hb8fs Hb8fp b9 Hb9fs Hb9fp b10 Hb10fs Hb10fp b11 Hb11fs Hb11fp
b12 Hb12fs Hb12fp b13 Hb13fs Hb13fp b14 Hb14fs Hb14fp b15 Hb15fs Hb15fp
b16 Hb16fs Hb16fp b17 Hb17fs Hb17fp b18 Hb18fs Hb18fp
b19 Hb19fs Hb19fp b20 Hb20fs Hb20fp
m´0 labd labd0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_syscall_dispatch_c)
nil
(create_undef_temps (fn_temps f_syscall_dispatch_c)))) H0.
Qed.
End SYSCALLDISPATCHC.
Section TRAPSENDTOCHANPRE.
Let L: compatlayer (cdata RData) :=
uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
⊕ syncsendto_chan_pre ↦ gensem syncsendto_chan_pre_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TrapSenToChanBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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 tuint 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 tuint cc_default))
Tnil tint cc_default).
uctx_arg3
Variable buctx_arg3: block.
Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
uctx_arg4
Variable buctx_arg4: block.
Hypothesis huctx_arg41 : Genv.find_symbol ge uctx_arg4 = Some buctx_arg4.
Hypothesis huctx_arg42 : Genv.find_funct_ptr ge buctx_arg4 =
Some (External (EF_external uctx_arg4 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
Hypothesis huctx_arg41 : Genv.find_symbol ge uctx_arg4 = Some buctx_arg4.
Hypothesis huctx_arg42 : Genv.find_funct_ptr ge buctx_arg4 =
Some (External (EF_external uctx_arg4 (signature_of_type Tnil tuint cc_default))
Tnil tint cc_default).
syncsendto_chan_pre
Variable bsyncsendto_chan_pre: block.
Hypothesis hsyncsendto_chan_pre1 : Genv.find_symbol ge syncsendto_chan_pre = Some bsyncsendto_chan_pre.
Hypothesis hsyncsendto_chan_pre2 : Genv.find_funct_ptr ge bsyncsendto_chan_pre =
Some (External (EF_external syncsendto_chan_pre
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Lemma trap_sendtochan_pre_body_correct: ∀ m d d´ env le val,
env = PTree.empty _ →
trap_sendtochan_pre_spec d = Some (d´, Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) trap_sendtochan_pre_body E0 le´ (m, d´) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; try subst;
functional inversion H2; try subst;
functional inversion H3; try subst;
unfold trap_sendtochan_pre_body;
esplit;
repeat vcgen.
Qed.
End TrapSenToChanBody.
Theorem trap_sendtochan_pre_code_correct:
spec_le
(trap_sendtochan_pre ↦ trap_sendtochan_pre_spec_low)
(〚trap_sendtochan_pre ↦ f_trap_sendtochan_pre 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(trap_sendtochan_pre_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_trap_sendtochan_pre)
nil
(create_undef_temps (fn_temps f_trap_sendtochan_pre)))) H0.
Qed.
End TRAPSENDTOCHANPRE.
End WithPrimitives.
End TTRAPCODE.
Hypothesis hsyncsendto_chan_pre1 : Genv.find_symbol ge syncsendto_chan_pre = Some bsyncsendto_chan_pre.
Hypothesis hsyncsendto_chan_pre2 : Genv.find_funct_ptr ge bsyncsendto_chan_pre =
Some (External (EF_external syncsendto_chan_pre
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Lemma trap_sendtochan_pre_body_correct: ∀ m d d´ env le val,
env = PTree.empty _ →
trap_sendtochan_pre_spec d = Some (d´, Int.unsigned val) →
∃ le´,
exec_stmt ge env le ((m, d): mem) trap_sendtochan_pre_body E0 le´ (m, d´) (Out_return (Some (Vint val, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
functional inversion H1; try subst;
functional inversion H2; try subst;
functional inversion H3; try subst;
unfold trap_sendtochan_pre_body;
esplit;
repeat vcgen.
Qed.
End TrapSenToChanBody.
Theorem trap_sendtochan_pre_code_correct:
spec_le
(trap_sendtochan_pre ↦ trap_sendtochan_pre_spec_low)
(〚trap_sendtochan_pre ↦ f_trap_sendtochan_pre 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(trap_sendtochan_pre_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m´0 labd labd0
(PTree.empty _)
(bind_parameter_temps´ (fn_params f_trap_sendtochan_pre)
nil
(create_undef_temps (fn_temps f_trap_sendtochan_pre)))) H0.
Qed.
End TRAPSENDTOCHANPRE.
End WithPrimitives.
End TTRAPCODE.