Introducing Forr?! Forr? is a tiny language that translates to Boogie. The purpose of the language and verifier is to serve as a tutorial example for how to build a verifier on top of Boogie.

1 files changed, 126 insertions, 0 deletions

diff --git a/Source/Forro/Resolver.fs b/Source/Forro/Resolver.fs
new file mode 100644
index 00000000..9844c24b
--- /dev/null
+++ b/Source/Forro/Resolver.fs
@@ -0,0 +1,126 @@
+module Resolver

+

+open System

+open Forro

+

+exception ResolutionError of string

+

+let ResolutionError(s: string) =

+    raise (ResolutionError s)

+

+let VarName v =

+    match v with Var(x) -> x

+

+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