NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library topsy_threadBuild

Require Import List EqNat.
Require Import ssreflect ssrbool.
Require Import ZArith_ext.
Require Import bipl.
Require Import seplog.

Require Import integral_type.

Module seplog_Z_m := Seplog ZIT.
Import seplog_Z_m.
Import seplog_Z_m.assert_m.expr_m.
Import seplog_Z_m.assert_m.

Local Open Scope heap_scope.
Local Open Scope seplog_expr_scope.
Local Open Scope seplog_cmd_scope.
Local Open Scope seplog_assert_scope.
Local Open Scope seplog_hoare_scope.
Local Open Scope Z_scope.

structure ProcContextPtr

Definition pcp_tf_gs := 0.
Definition pcp_tf_fs := 1.
Definition pcp_tf_es := 2.
Definition pcp_tf_ds := 3.
Definition pcp_tf_trapno := 4.
Definition pcp_tf_edi := 5.
Definition pcp_tf_esi := 6.
Definition pcp_tf_ebp := 7.
Definition pcp_tf_temp_esp := 8.
Definition pcp_tf_ebx := 9.
Definition pcp_tf_edx := 10.
Definition pcp_tf_ecx := 11.
Definition pcp_tf_eax := 12.
Definition pcp_tf_err := 13.
Definition pcp_tf_eip := 14.
Definition pcp_tf_cs := 15.
Definition pcp_tf_eflags := 16.
Definition pcp_tf_esp := 17.
Definition pcp_tf_ss := 18.

structure Thread

Definition th_contextPtr := 0.
Definition th_id := 1.
Definition th_name := 2.
Definition th_parentId := 3.
Definition th_stackStart := 4.
Definition th_stackEnd := 5.
Definition th_msgQueue := 6.
Definition th_schedInfo := 7.
Definition th_stat := 8.

Local Close Scope Z_scope.
Local Close Scope positive_scope.

Definition USER : Z := 1%Z.
Definition KERNEL : Z := 0%Z.

Axiom sizeof_Message : nat.
Axiom exitCodeLength : nat.
Axiom MAXNAMESIZE : nat.
Axiom STATUS_INT_ENABLE_USER_PREV : nat.
Axiom STATUS_INT_ENABLE_KERNEL_PREV : nat.

Open Local Scope vc_scope.

Definition skip : cmd' := (0) <- (var_e 0).

Subroutines


Open Local Scope Z_scope.

tmp serves as a temporary buffer variable
Definition stringNCopy (tmp target source size : nat) :=
  tmp <-* var_e source;
  var_e target *<- var_e tmp;
  size <- var_e size .-e cst_e 1%Z;
  while' ((var_e tmp =e cst_e 0) &e (var_e size <>e cst_e 0)) (TT) (
    tmp <-* var_e source;
    var_e target *<- var_e tmp;
    size <- var_e size .-e cst_e 1
  ).

Initialization of fields for registers

Definition tmSetMachineDependentRegisters (context_ptr space : nat) :=
  ifte' (var_e space =e cst_e USER)
  ( (context_ptr -.> pcp_tf_cs) *<- cst_e 3;
    (context_ptr -.> pcp_tf_ds) *<- cst_e 3;
    (context_ptr -.> pcp_tf_es) *<- cst_e 3;
    (context_ptr -.> pcp_tf_fs) *<- cst_e 3;
    (context_ptr -.> pcp_tf_gs) *<- cst_e 3;
    (context_ptr -.> pcp_tf_ss) *<- cst_e 3 )
  ( (context_ptr -.> pcp_tf_cs) *<- cst_e 0;
    (context_ptr -.> pcp_tf_ds) *<- cst_e 0;
    (context_ptr -.> pcp_tf_es) *<- cst_e 0;
    (context_ptr -.> pcp_tf_fs) *<- cst_e 0;
    (context_ptr -.> pcp_tf_gs) *<- cst_e 0;
    (context_ptr -.> pcp_tf_ss) *<- cst_e 0 ).

Definition precond (cs0 ds0 es0 fs0 gs0 ss0 : expr) (context_ptr space : var.v) := fun s h =>
  [ var_e space ]e_ s = USER /\ (
    (context_ptr -.> pcp_tf_cs |~> cs0) **
    (context_ptr -.> pcp_tf_ds |~> ds0) **
    (context_ptr -.> pcp_tf_es |~> es0) **
    (context_ptr -.> pcp_tf_fs |~> fs0) **
    (context_ptr -.> pcp_tf_gs |~> gs0) **
    (context_ptr -.> pcp_tf_ss |~> ss0)) s h.

Definition postcond (context_ptr space : var.v) :=
  (context_ptr -.> pcp_tf_cs |~> cst_e 3) **
  (context_ptr -.> pcp_tf_ds |~> cst_e 3) **
  (context_ptr -.> pcp_tf_es |~> cst_e 3) **
  (context_ptr -.> pcp_tf_fs |~> cst_e 3) **
  (context_ptr -.> pcp_tf_gs |~> cst_e 3) **
  (context_ptr -.> pcp_tf_ss |~> cst_e 3) .

Definition threadBuild
variables for stringNCopy
  (stringNCopy_source stringNCopy_target stringNCopy_size : nat)
buffer variable
  (tmp : nat)
local variables
  (sp mode_ : nat)
parameters
  (id parentId name contextPtr stackBaseAddress stackSize mainFunction parameter space threadPtr priority : nat) :=
  (threadPtr -.> th_id) *<- var_e id;
  (threadPtr -.> th_parentId) *<- var_e parentId;
  ifte' (var_e name <>e cst_e 0)
  ( stringNCopy_source <-* (threadPtr -.> th_name);
    stringNCopy_target <- var_e name;
    stringNCopy_size <- cst_e (Z_of_nat MAXNAMESIZE);
    stringNCopy tmp stringNCopy_source stringNCopy_target stringNCopy_size )
  ( stringNCopy_source <-* (threadPtr -.> th_name);
    stringNCopy tmp stringNCopy_source stringNCopy_target stringNCopy_size ) ;

  ifte' (var_e space =e cst_e USER)
  ( skip;
    mode_ <- cst_e (Z_of_nat STATUS_INT_ENABLE_USER_PREV) )
  ( skip;
    mode_ <- cst_e (Z_of_nat STATUS_INT_ENABLE_KERNEL_PREV) );
  (threadPtr -.> th_stackStart) *<- var_e stackBaseAddress +e var_e stackSize .-e cst_e 4 ;
  (threadPtr -.> th_stackEnd) *<- var_e stackBaseAddress ;
  (threadPtr -.> th_contextPtr) *<- var_e contextPtr ;

  tmp <-* (threadPtr -.> th_stackStart) ;
  sp <- var_e tmp .-e cst_e (Z_of_nat sizeof_Message) .-e cst_e (Z_of_nat exitCodeLength)
.

Local Close Scope vc_scope.

Require Import ssrnat nodup.

Lemma tmSetMachineDependentRegisters_Lemma: forall (cs0 ds0 es0 fs0 gs0 ss0 : expr),
  forall (context_ptr space : var.v), nodup (context_ptr :: space :: nil) ->
    {{ (precond cs0 ds0 es0 fs0 gs0 ss0) context_ptr space }}
    proj_cmd (tmSetMachineDependentRegisters context_ptr space)
    {{ postcond context_ptr space }}.
Proof.
move=> cs0 ds0 es0 fs0 gs0 ss0 context_ptr space H.
rewrite /tmSetMachineDependentRegisters /=.
ifte var_e space =e cst_e USER
apply while.hoare_ifte.
- apply hoare_prop_m.hoare_stren with (precond cs0 ds0 es0 fs0 gs0 ss0 context_ptr space).
  rewrite /while.entails; by intuition.
  rewrite /precond /postcond.
  apply hoare_prop_m.hoare_stren with (
    (((((((context_ptr -.> pcp_tf_cs) |~> cs0) **
      ((context_ptr -.> pcp_tf_ds) |~> ds0)) **
    ((context_ptr -.> pcp_tf_es) |~> es0)) **
    ((context_ptr -.> pcp_tf_fs) |~> fs0)) **
    ((context_ptr -.> pcp_tf_gs) |~> gs0)) **
    ((context_ptr -.> pcp_tf_ss) |~> ss0))).
  rewrite /while.entails; intros; by intuition.

  eapply while.hoare_seq.

  do 4 rewrite assert_m.con_assoc_equiv.

  apply frame_rule.
  apply hoare_mutation_local.
  rewrite /inde /=; contradiction.

  eapply while.hoare_seq.

  rewrite assert_m.con_com_equiv assert_m.con_assoc_equiv.
  apply frame_rule.
  apply hoare_mutation_local.
  rewrite /inde /=; contradiction.

  eapply while.hoare_seq.

  rewrite assert_m.con_com_equiv assert_m.con_assoc_equiv assert_m.con_assoc_equiv.

  apply frame_rule.
  apply hoare_mutation_local.
  rewrite /inde /=; contradiction.

  eapply while.hoare_seq.

  rewrite assert_m.con_com_equiv 3!assert_m.con_assoc_equiv.

  apply frame_rule.
  apply hoare_mutation_local.
  rewrite /inde /=; contradiction.

  eapply while.hoare_seq.

  rewrite assert_m.con_com_equiv 4!assert_m.con_assoc_equiv.

  apply frame_rule.
  apply hoare_mutation_local.
  rewrite /inde /=; contradiction.

  rewrite assert_m.con_com_equiv 4!assert_m.con_assoc_equiv.
  rewrite -(assert_m.con_com_equiv ((context_ptr -.> pcp_tf_ss) |~> cst_e 3)).
  rewrite 3!assert_m.con_assoc_equiv.

  apply frame_rule.
  apply hoare_mutation_local.
  rewrite /= /inde /=; contradiction.
  rewrite /precond /=.
  apply hoare_prop_m.hoare_stren with FF.
  - move=> s h [[H3 H4] H2].
    move/ZIT.tP : H2 => H2; contradiction.
  - by apply hoare_false.
Qed.