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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
module Resolver
open System
open Forro
exception ResolutionError of string
let ResolutionError(s: string) =
raise (ResolutionError s)
type VarKind = InParam | OutParam | Local
type Context(procedures: Collections.Generic.IDictionary<string,Procedure>) =
let mutable locals = null
let mutable ProcName = ""
member c.Procedures = procedures
member c.StartNewProcedure procName =
ProcName <- procName
locals <- new Collections.Generic.Dictionary<string,VarKind>()
member c.AddLocal v kind =
let name = VarName v
if locals.ContainsKey name then ResolutionError ("duplicate variable '" + name + "' in procedure '" + ProcName + "'") else ()
locals.Add(name, kind)
member c.HasLocal v =
locals.ContainsKey (VarName v)
member c.IncludeAssignmentTarget v =
let name = VarName v
if locals.ContainsKey name then
let kind = locals.Item name
if kind = VarKind.InParam then ResolutionError ("variable '"+ name + "' is an in-parameter, which cannot be used as an assignment target") else ()
else
locals.Add(name, VarKind.Local)
member v.GetLocals = locals
let rec ResolveExpr (ctx: Context) expr twoState specContext =
match expr with
| Constant(x) -> ()
| Null -> ()
| Identifier(v) ->
if ctx.HasLocal v then () else ResolutionError ("undefined variable: " + VarName v)
| Not(e) -> ResolveExpr ctx e twoState specContext
| Binary(op,a,b) ->
ResolveExpr ctx a twoState specContext
ResolveExpr ctx b twoState specContext
| Select(e,f) ->
ResolveExpr ctx e twoState specContext
match f with
| Valid -> if specContext then () else ResolutionError "valid can only be used in specification contexts"
| _ -> ()
| Old(e) ->
if twoState then () else ResolutionError "old expressions can only be used in two-state contexts"
ResolveExpr ctx e twoState specContext
let rec ResolveStmt ctx s =
match s with
| Assign(v, e) ->
ResolveExpr ctx e false false
ctx.IncludeAssignmentTarget v
| Update(obj,f,rhs) ->
ResolveExpr ctx obj false false
match f with
| Valid -> ResolutionError "valid can only be used in specification contexts (in particular, it cannot be assigned to)"
| _ -> ()
ResolveExpr ctx rhs false false
| Alloc(v,hd,tl) ->
ResolveExpr ctx hd false false
ResolveExpr ctx tl false false
ctx.IncludeAssignmentTarget v
| IfStmt(guard,thn,els) ->
ResolveExpr ctx guard false false
ResolveStmtList ctx thn
ResolveStmtList ctx els
| WhileStmt(guard,invs,body) ->
ResolveExpr ctx guard false false
List.iter (fun inv -> ResolveExpr ctx inv true true) invs
ResolveStmtList ctx body
| CallStmt(outs,name,ins) ->
if ctx.Procedures.ContainsKey name then () else ResolutionError ("call to undefined procedure: " + name)
match ctx.Procedures.Item name with
| Proc(_,fIns,fOuts,_,_,_) ->
if fIns.Length = ins.Length then () else ResolutionError ("call to " + name + " has wrong number of in-parameters (got " + ins.Length.ToString() + ", expected " + fIns.Length.ToString() + ")")
if fOuts.Length = outs.Length then () else ResolutionError ("call to " + name + " has wrong number of out-parameters (got " + outs.Length.ToString() + ", expected " + fOuts.Length.ToString() + ")")
List.iter (fun e -> ResolveExpr ctx e false false) ins
let outnames = new Collections.Generic.Dictionary<string,Variable>()
List.iter (fun v ->
ctx.IncludeAssignmentTarget v
let name = VarName v
if outnames.ContainsKey name then ResolutionError ("an actual out-parameter is allowed only once for a call: " + name) else ()
outnames.Add(name, v)
) outs
| Assert(e) ->
ResolveExpr ctx e true true
and ResolveStmtList ctx slist =
match slist with
| Block(ss) -> List.iter (fun s -> ResolveStmt ctx s) ss
let ProcedureName p =
match p with Proc(id,_,_,_,_,_) -> id
let ResolveProc (ctx: Context) p =
match p with
| Proc(name, ins, outs, req, ens, body) ->
// look up 'name' in ctx.Procedures, report an error if it is not 'p'
let q = ctx.Procedures.Item name
if p <> q then ResolutionError ("duplicate procedure: " + name) else ()
ctx.StartNewProcedure name
// look for duplicates in ins+outs
List.iter (fun v -> ctx.AddLocal v VarKind.InParam) ins
List.iter (fun v -> ctx.AddLocal v VarKind.OutParam) outs
// resolve specification
ResolveExpr ctx req false true
ResolveExpr ctx ens true true
// resolve body
ResolveStmtList ctx body
ctx.GetLocals
let Resolve prog =
match prog with
| Prog(procs) ->
let procedures = dict [ for p in procs -> ProcedureName p, p ]
let ctx = Context(procedures)
List.map (fun p -> p, ResolveProc ctx p) procs
|
