1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
|
Require Import Strings.String.
Require Import Classes.EquivDec.
Require Import Lists.List.
Inductive Owner : Type :=
| server : Owner
| client : Owner.
Inductive ClassName : Type :=
| className : string -> ClassName.
Inductive Label : Type :=
| label : nat -> Owner -> Label.
Inductive Var : Type :=
| var : string -> Var.
Inductive FieldName : Type :=
| fieldName : string -> Owner -> FieldName.
Inductive MethodCall : Type :=
| methodCall : string -> MethodCall.
Inductive Exp : Type :=
| varExp : Var -> Exp
| fieldReference : Var -> FieldName -> Exp
| methodCallExp : Var -> MethodCall -> list Var -> Exp
| allocation : ClassName -> list Var -> Exp
| cast : ClassName -> Var -> Exp.
Inductive Stmt : Type :=
| assignment : Var -> Exp -> Label -> Stmt
| returnStmt : Var -> Label -> Stmt
| fieldUpdate : Var -> FieldName -> Exp -> Label -> Stmt.
Inductive Konst : Type :=
| konst : ClassName -> (list (ClassName * FieldName)) -> list FieldName -> (list FieldName * FieldName) -> Konst.
Inductive Method : Type :=
| method : ClassName -> MethodCall -> list (ClassName * Var) -> list (ClassName * Var) -> (list Stmt) -> Method.
Inductive Class : Type :=
| class : ClassName -> ClassName -> (list (ClassName * FieldName)) -> (Konst * (list Method)) -> Class.
Inductive Context : Type :=
| context : nat -> Context.
Inductive HContext : Type :=
| heapContext : nat -> HContext.
Inductive Location := loc : nat -> Location.
Definition AbsLocation := ((Var * Context) + (FieldName * HContext)) % type.
Definition CallStack := list (Stmt * Context * Var) % type.
Inductive TypeState : Type :=
| fresh : TypeState
| stale : TypeState.
Definition Obj := (HContext * (FieldName -> option AbsLocation) * TypeState) % type.
Definition Store := Location -> option Obj.
Definition OwnerStore := Owner -> Store.
Definition AbsStore := AbsLocation -> option (list Obj).
Definition Stack := list (Var -> option Location).
Definition Batch := list Location.
Definition Sigma := (Stmt * Stack * OwnerStore * AbsStore * CallStack * Context * Batch) % type.
Definition update {A : Type} {B : Type} `{EqDec A} `{EqDec B} (f : A -> B) (k : A) (v : B) : (A -> B) :=
fun k' => if equiv_decb k' k then v else f k'.
Definition transfer : Label -> OwnerStore -> Batch -> (OwnerStore * Batch) :=
fun _ o b => (o,b).
Parameter succ : Label -> Stmt.
Parameter owner : Label -> Owner.
Inductive concreteSingleStep : Sigma -> Sigma -> Prop :=
| fieldAssignmentLocal : forall v f_do f o so sigma_so hc m sigma'_so v' l st sigma absSigma cst c b sigma' sigma'' b',
(f_do = fieldName f o) -> so = owner(l) -> sigma_so = sigma(so) -> Some (hc, m, fresh) = sigma_so(st(v)) -> sigma'_so = update sigma_so st(v) (Some (hc, update m f_do st(v'), fresh))
-> sigma' = update sigma so sigma'_so -> o = so -> (sigma'', b') = transfer l sigma' b ->
concreteSingleStep ((fieldUpdate v f_do (varExp v') l), st, sigma, absSigma, cst, c, b)
(succ(l), st, sigma'', absSigma, cst, c, b').
| fieldAssignmentRemote : forall v f_do f o so sigma_so hc m sigma'_so v' l st sigma absSigma cst c b sigma' sigma'' b',
(f_do = fieldName f o) -> so = owner(l) -> sigma_so = sigma(so) -> (hc, m, fresh) = sigma_so(st(v)) -> sigma'_so = update sigma_so st(v) (hc, update m f_do st(v'), fresh)
-> sigma' = update sigma so sigma'_so -> o <> so -> (sigma'', b') = transfer l sigma' (b ++ st(v)) ->
concreteSingleStep ((fieldUpdate v f_o (varExp v') l), st, sigma, absSigma, cst, c, b)
(succ(l), st, sigma'', absSigma, cst, c, b'')
| variableStep : forall v v' l st st' sigma sigma' absSigma cst c b b',
(st' = st ++ (update (fun _ => None) v st(v'))) -> (sigma',b') = transfer l sigma b ->
concreteSingleStep ((assignment v (varExp v') l), st, sigma, absSigma, cst, c, b) (succ(l), st', sigma', absSigma, cst, c, b')
| returnStep : forall v l st sigma absSigma cst c b v_ret s st' sigma' c' b',
(s,c',v_ret) = car(cst) -> st' = cdr(st) ++ update (fun _ => None) v_ret st(v) -> (sigma', b') = transfer l sigma b ->
concreteSingleStep ((returnStmt v l), st, sigma, absSigma, cst, c, b) (s, st', sigma', absSigma, cdr(cst), c', b')
| fieldReferenceStep : forall v v' f_do l st sigma absSigma cst c b so hc m' m st' sigma' absSigma cst c b',
so = owner(l) -> (hc, m', fresh) = sigma(so)(st(v')) -> m' = update m f_do l -> st' = st ++ update (fun _ => None) v l -> (sigma', b') = transfer l sigma b ->
concreteSingleStep ((assignment v (fieldReference v' f_do) l), st, sigma, absSigma, cst, c, b) (s, st', sigma', absSigma, cst, c, b').
|
