diff options
| author |  rustanleino <unknown> | 2010-11-06 19:47:03 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-11-06 19:47:03 +0000 |
| commit | ea1898f88e2edcecf3a58923fcd1a5d2b87219a8 (patch) | |
| tree | 82944147dd136bf68b4cb2f8e40d440c6705d42e /Source/Forro/Parser.fsy | |
| parent | 8d1dd0f01a78bf29aa98832317d8fc951ed15075 (diff) | |
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.
Diffstat (limited to 'Source/Forro/Parser.fsy')
| -rw-r--r-- | Source/Forro/Parser.fsy | 115 |
1 files changed, 115 insertions, 0 deletions
diff --git a/Source/Forro/Parser.fsy b/Source/Forro/Parser.fsy new file mode 100644 index 00000000..6fa41431 --- /dev/null +++ b/Source/Forro/Parser.fsy @@ -0,0 +1,115 @@ +%{
+
+open Forro
+
+exception ParseError of string
+
+let StringsToVariables ss = [ for s in ss -> Var(s) ]
+
+let IdToField id =
+ match id with
+ | "head" -> Field.Head
+ | "tail" -> Field.Tail
+ | "valid" -> Field.Valid
+ | _ -> raise (ParseError ("illegal field selector: '" + id + "' (legal selectors are 'head', 'tail', and 'valid')"))
+
+%}
+
+// The start token becomes a parser function in the compiled code:
+%start start
+
+// These are the terminal tokens of the grammar along with the types of
+// the data carried by each token:
+%token <string> ID
+%token <System.Int32> INT32
+%token NULL
+%token DOT
+%token NOT
+%token PLUS MINUS
+%token STAR
+%token EQ NEQ LESS ATMOST
+%token AND OR
+%token OLD LPAREN RPAREN SEMI ASSIGN
+%token PROCEDURE REQUIRES ENSURES DO END
+%token NEW IF THEN ELSE WHILE INVARIANT CALL ASSERT
+%token EOF
+
+// This is the type of the data produced by a successful reduction of the 'start'
+// symbol:
+%type < Forro.Program > start
+
+%%
+
+// These are the rules of the grammar along with the F# code of the
+// actions executed as rules are reduced. In this case the actions
+// produce data using F# data construction terms.
+start: Prog EOF { Prog(List.rev($1)) }
+
+Prog: Proc { [$1] }
+ | Prog Proc { $2 :: $1 }
+
+Proc:
+ PROCEDURE Signature
+ REQUIRES Expression ENSURES Expression
+ DO StmtList END SEMI
+ { match $2 with outs,id,ins -> Proc(id, StringsToVariables ins, StringsToVariables outs, $4, $6, $8) }
+
+Signature:
+ IdList { [], List.head $1, List.tail $1 }
+ | IdList ASSIGN IdList { $1, List.head $3, List.tail $3 }
+
+IdList: ID { [$1] }
+ | ID IdList { $1 :: $2 }
+
+Expression:
+ AtomicExpr { $1 }
+ | NOT Expression { Not($2) }
+ | Expression PLUS Expression { Binary(Operator.Plus, $1, $3) }
+ | Expression MINUS Expression { Binary(Operator.Minus, $1, $3) }
+ | Expression STAR Expression { Binary(Operator.Times, $1, $3) }
+ | Expression EQ Expression { Binary(Operator.Eq, $1, $3) }
+ | Expression NEQ Expression { Binary(Operator.Neq, $1, $3) }
+ | Expression LESS Expression { Binary(Operator.Less, $1, $3) }
+ | Expression ATMOST Expression { Binary(Operator.AtMost, $1, $3) }
+ | Expression AND Expression { Binary(Operator.And, $1, $3) }
+ | Expression OR Expression { Binary(Operator.Or, $1, $3) }
+
+AtomicExpr:
+ INT32 { Constant($1) }
+ | NULL { Null }
+ | ID { Identifier(Var($1)) }
+ | OLD LPAREN Expression RPAREN { Old($3) }
+ | LPAREN Expression RPAREN { $2 }
+ | FieldSelect { match $1 with e,f -> Select(e,f) }
+
+FieldSelect:
+ AtomicExpr DOT ID { $1, IdToField $3 }
+
+ExprList: // possibly empty
+ { [] }
+ | Expression ExprList { $1::$2 }
+
+VarList: // nonempty
+ | ID ASSIGN { [Var($1)] }
+ | ID VarList { Var($1)::$2 }
+
+StmtList:
+ StmtListX { Block($1) }
+
+StmtListX:
+ { [] }
+ | Stmt StmtListX { $1::$2 }
+
+Stmt:
+ ID ASSIGN Expression SEMI { Assign(Var($1), $3) }
+ | ID ASSIGN NEW Expression Expression SEMI { Alloc(Var($1), $4, $5) }
+ | FieldSelect ASSIGN Expression SEMI { match $1 with e,f -> Update(e, f, $3) }
+ | IF Expression THEN StmtList ELSE StmtList END SEMI { IfStmt($2,$4,$6) }
+ | WHILE Expression Invariants DO StmtList END SEMI { WhileStmt($2,$3,$5) }
+ | CALL ID LPAREN ExprList RPAREN SEMI { CallStmt([],$2,$4) }
+ | CALL VarList ID LPAREN ExprList RPAREN SEMI { CallStmt($2,$3,$5) }
+ | ASSERT Expression SEMI { Assert($2) }
+
+Invariants:
+ { [] }
+ | INVARIANT Expression Invariants { $2::$3 }
|