/
parsetree.ml
80 lines (62 loc) · 2.42 KB
/
parsetree.ml
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
(*****************************************************************************)
(* Datatypes for parse trees and internal representations *)
(*****************************************************************************)
open Global
(*****************************************************************************)
(* Parse trees *)
(*****************************************************************************)
type space_pred =
| SpacePredEmpty
| SpacePredPointsTo of identifier * expression
| SpacePredListseg of expression * expression
type pure_pred =
| PurePredEquality of expression * expression
type assertion =
| Assertion of pure_pred list * space_pred list
type condition =
| IfEqual of expression * expression
| IfUnequal of expression * expression
| NondetChoice
| STrue
| SFalse
type statement =
| StmtSkip
| StmtAssign of identifier * expression
| StmtLookup of identifier * identifier
| StmtMemAssign of identifier * expression
| StmtDispose of identifier
| StmtNew of identifier
| StmtBlock of statement list
| StmtIf of condition * statement * statement
| StmtWhile of condition * statement
| StmtGoto of int
| StmtReturn of expression;;
type fun_decl =
| FunDecl of string * identifier list * statement list
type program = fun_decl list
(*****************************************************************************)
(* Internal representation of assertions *)
(*****************************************************************************)
type pure_heap = Eq of exp * exp | Topp;;
type spatialheap = Pointsto of exp * exp | ListSeg of exp * exp | Junk | Emp | Tops;;
type symbheap = pure_heap list * spatialheap list;;
type stat =
Assign of exp * exp * label
| Lookup of exp * exp * label
| New of exp * label
| Disp of exp * label
| Mutate of exp * exp * label
| Seq of stat * stat
| If of bexp * label * stat * stat
| While of bexp * label * stat
| Skip of label
| Return of exp * label
| Goto of int * label;;
let primitive_command comm =
match comm with
| Assign(x,_,_) -> (false,x)
| Lookup(_,x,_) -> (true,x)
| Mutate(x,_,_) -> (true,x)
| New(x,_) -> (false,x)
| Disp(x,_) -> (true,x)
| _ -> (false,Var("y"));;