CSemantics




Given these operations, we define a straightforward operational semantics for this fragment of C that is undefined for programs that access deallocated memory locations. The standard operational semantics of C evaluates a left-hand-side of an assignment to an address. The value at that address is overwritten by the value that the corresponding right-hand-side evaluates to. Note that, because the compiler transformations that yield code in this intermediate form depend on source-program type information (to calculate struct field indices, for example) and CETS' instrumentation itself uses types, our non-standard semantics depends on source type information.

Inductive uResult: Set :=
| uROK : uResult
| uRLoc : Loc -> uResult
| uRVal : Value -> uResult
| uSystemError : uResult
.

Definition uError (R: uResult) := (R = uSystemError).

Inductive us_lhs : uEnv -> c_lhs -> uResult -> AType -> Prop :=
  
  | uS_GVar : forall (E:uEnv) (v: Var) (l: nat) (t: AType),
     (uStack2frame (ustack E)) v = None ->
     lookUpGlobal E.(uglobal) v = Some (l, t) ->
     wf_AType t ->
     us_lhs E (C_Var v) (uRLoc l) t

  | uS_SVar : forall (E:uEnv) (v: Var) (l: nat) (t: AType),
     lookUpuStack E.(ustack) v = Some (l, t) ->
     wf_AType t ->
     us_lhs E (C_Var v) (uRLoc l) t

  
  | uS_Deref : forall E lhs loc loc' t,
     us_lhs E lhs (uRLoc loc) (A_Pointer (P_AType t)) ->
     accessMem E.(umem) loc = Some loc' ->
     us_lhs E (C_Deref lhs) (uRLoc loc') t

  
  | uS_StructPos : forall E lhs id loc s t' offset loc',
     us_lhs E lhs (uRLoc loc) (A_Pointer (P_Struct s)) ->
     accessMem E.(umem) loc = Some loc' ->
     getStructOffset s id = Some offset ->
     getStructType s id = Some t' ->
     us_lhs E (C_StructPos lhs id) (uRLoc (loc'+offset)) t'

  
  | uS_NamePos : forall E lhs id loc n s t' offset loc',
     us_lhs E lhs (uRLoc loc) (A_Pointer (P_Name n)) ->
     accessMem E.(umem) loc = Some loc' ->
     typeTable n = Some s ->
     getStructOffset s id = Some offset ->
     getStructType s id = Some t' ->
     us_lhs E (C_NamePos lhs id) (uRLoc (loc'+offset)) t'
  .

Inductive us_rhs : uEnv -> c_rhs -> uResult -> AType -> uEnv -> Prop :=
  
  | uS_Const : forall E n,
     us_rhs E (C_Const n) (uRVal n) A_Int E

  
  | uS_Lhs : forall E lhs loc t ds,
     us_lhs E lhs (uRLoc loc) t ->
     accessMem E.(umem) loc = Some ds->
     us_rhs E (C_Lhs lhs) (uRVal ds) t E

  
  | uS_Ref : forall E lhs loc t,
     us_lhs E lhs (uRLoc loc) t ->
     wf_AType (A_Pointer (P_AType t)) ->
     us_rhs E (C_Ref (P_AType t) lhs)
                   (uRVal loc)
                   (A_Pointer (P_AType t)) E

  
  | uS_Add_Int_Int : forall E E' E'' rhs1 rhs2 n1 n2,
     us_rhs E rhs1 (uRVal n1) A_Int E' ->
     us_rhs E' rhs2 (uRVal n2) A_Int E'' ->
     us_rhs E (C_Add rhs1 rhs2)
                   (uRVal (n1+n2))
                   A_Int E''
  | uS_Add_Int_Int_ErrorProp1 : forall E E' rhs1 R t rhs2 t',
     us_rhs E rhs1 R t E' -> uError R ->
     us_rhs E (C_Add rhs1 rhs2) R t' E'
  | uS_Add_Int_Int_ErrorProp2 : forall E E' E'' rhs1 ds1 rhs2 R t t',
     us_rhs E rhs1 (uRVal ds1) A_Int E' ->
     us_rhs E' rhs2 R t E'' -> uError R ->
     us_rhs E (C_Add rhs1 rhs2) R t' E''

  
  | uS_Add_Ptr_Int : forall E E' E'' rhs1 rhs2 p n1 n2 size,
     us_rhs E rhs1 (uRVal n1) (A_Pointer p) E' ->
     us_rhs E' rhs2 (uRVal n2) A_Int E'' ->
     wf_AType (A_Pointer p) ->
     sizeOfPType p = Some size ->
     us_rhs E (C_Add rhs1 rhs2)
                   (uRVal (n1+n2*size))
                   (A_Pointer p) E''
  | uS_Add_Ptr_Int_ErrorProp1 : forall E E' rhs1 R t rhs2 t',
     us_rhs E rhs1 R t E' -> uError R ->
     us_rhs E (C_Add rhs1 rhs2) R t' E'
  | uS_Add_Ptr_Int_ErrorProp2 : forall E E' E'' rhs1 ds1 rhs2 R p t' t'',
     us_rhs E rhs1 (uRVal ds1) (A_Pointer p) E' ->
     us_rhs E' rhs2 R t' E'' -> uError R ->
     us_rhs E (C_Add rhs1 rhs2) R t'' E''

  
  | uS_Cast : forall E E' rhs ds t t',
     us_rhs E rhs (uRVal ds) t E' ->
     wf_AType t' ->
     us_rhs E (C_Cast t' rhs) (uRVal ds) t' E'
  | uS_Cast_ErrorProp : forall E E' rhs R t t' t'',
     us_rhs E rhs R t E' -> uError R ->
     us_rhs E (C_Cast t' rhs) R t'' E'

  
  | uS_Size : forall E t size,
     wf_PType t ->
     sizeOfPType t = Some size ->
     us_rhs E (C_Size t) (uRVal size) A_Int E

  
  | uS_Alloc : forall E E' E'' rhs loc n p size,
    us_rhs E rhs (uRVal n) A_Int E'->
    wf_AType (A_Pointer p) ->
    sizeOfPType p = Some size ->
    size > 0 ->
    umalloc E' n = Some (E'', loc)->
    us_rhs E (C_Alloc p rhs)
                  (uRVal loc)
                  (A_Pointer p)
                  E''
  | uS_Alloc_ErrorProp : forall E E' rhs R t t' p,
    us_rhs E rhs R t E'-> uError R ->
    wf_AType (A_Pointer p) ->
    us_rhs E (C_Alloc p rhs) R t' E'
  | uS_Alloc_OutofMem : forall E E' rhs n t' p size,
    us_rhs E rhs (uRVal n) A_Int E'->
    wf_AType (A_Pointer p) ->
    sizeOfPType p = Some size ->
    size > 0 ->
    umalloc E' n = None->
    us_rhs E (C_Alloc p rhs) uSystemError t' E'
  .

Inductive us_cmd : uEnv -> c_cmd -> uResult-> uEnv->Prop :=
  
  | uS_Skip : forall E,
    us_cmd E (C_Skip) uROK E

  
  | uS_Seq : forall E E' E'' c1 c2,
    us_cmd E c1 uROK E' ->
    us_cmd E' c2 uROK E'' ->
    us_cmd E (C_Seq c1 c2) uROK E''
  | uS_Seq_ErrorProp1 : forall E E' R c1 c2,
    us_cmd E c1 R E' -> uError R->
    us_cmd E (C_Seq c1 c2) R E'
  | uS_Seq_ErrorProp2 : forall E E' E'' c1 c2 R,
    us_cmd E c1 uROK E' ->
    us_cmd E' c2 R E'' -> uError R->
    us_cmd E (C_Seq c1 c2) R E''

  
  | uS_Assign : forall E E' lhs rhs loc tl ds tr M'' AMB'' G'' S'',
    us_lhs E lhs (uRLoc loc) tl ->
    us_rhs E rhs (uRVal ds) tr E' ->
    storeMem E'.(umem) loc ds = Some M''->
    E'.(uglobal) = G'' ->
    E'.(ustack) = S'' ->
    us_cmd E (C_Assign lhs rhs) uROK (MkuEnv M'' AMB'' G'' S'')
  | uS_Assign_ErrorProp1 : forall E lhs rhs tl R,
    us_lhs E lhs R tl -> uError R->
    us_cmd E (C_Assign lhs rhs) R E
  | uS_Assign_ErrorProp2 : forall E E' lhs rhs loc tl R tr,
    us_lhs E lhs (uRLoc loc) tl ->
    us_rhs E rhs R tr E' -> uError R->
    us_cmd E (C_Assign lhs rhs) R E'

  | uS_Free : forall E lhs loc p E',
    us_lhs E lhs (uRLoc loc) (A_Pointer p) ->
    ufree E loc = Some E' ->
    us_cmd E (C_Free lhs) uROK E'
  | uS_Free_ErrorProp : forall E lhs tl R,
    us_lhs E lhs R tl -> uError R->
    us_cmd E (C_Free lhs) R E
  | uS_Free_Error : forall E lhs loc p,
    us_lhs E lhs (uRLoc loc) (A_Pointer p) ->
    ufree E loc = None ->
    us_cmd E (C_Free lhs) uSystemError E

  | uS_Call : forall E n f c R E' E'' E''',
    funTable n = Some (f, c) ->
    ucreateFrame E f = Some E' ->
    us_cmd E' c R E'' ->
    ~ uError R ->
    udestroyFrame E'' = Some E''' ->
    us_cmd E (C_Call n) R E'''
  | uS_Call_ErrorProp : forall E n f c R E' E'',
    funTable n = Some (f, c) ->
    ucreateFrame E f = Some E' ->
    us_cmd E' c R E'' ->
    uError R ->
    us_cmd E (C_Call n) R E''
  | uS_Call_Error1 : forall E n f c,
    funTable n = Some (f, c) ->
    ucreateFrame E f = None ->
    us_cmd E (C_Call n) uSystemError E
  | uS_Call_Error2 : forall E n f c R E' E'',
    funTable n = Some (f, c) ->
    ucreateFrame E f = Some E' ->
    us_cmd E' c R E'' ->
    ~ uError R ->
    udestroyFrame E'' = None ->
    us_cmd E (C_Call n) uSystemError E''
  .