diff options
| author |  rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-08-10 02:16:29 +0000 |
| commit | 554fb3a6780c412b81dc935835c2760e4cbe0b4d (patch) | |
| tree | b50aa3dbbb369a52751bfcb9f142c9c928e591ae | |
| parent | c2aa0b56fce36a101c3bef7ce901b8f26dcb5f08 (diff) | |
Boogie: Added boolean code expressions (sans well-formedness checks on the input).
34 files changed, 1413 insertions, 1059 deletions
diff --git a/Binaries/TypedUnivBackPred2.sx b/Binaries/TypedUnivBackPred2.sx index 5ee200f1..450e658a 100644 --- a/Binaries/TypedUnivBackPred2.sx +++ b/Binaries/TypedUnivBackPred2.sx @@ -10,6 +10,8 @@ (DEFOP <: U U $bool) ; used for translation with type premisses
(DEFOP <:: T U U $bool) ; used for translation with type arguments
+(DEFOP tickleBool $bool $bool) ; used in triggers to exhaustively instantiate quantifiers over booleans
+
(BG_PUSH (AND
; false is not true
@@ -126,6 +128,8 @@ ; Reflect plus
(FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))
+ (tickleBool FALSE)
+ (tickleBool TRUE)
)) ;; AND, BG_PUSH
; End Boogie universal background predicate
; -------------------------------------------------------------------------
diff --git a/Binaries/UnivBackPred2.sx b/Binaries/UnivBackPred2.sx index 7c3dac8e..7e30017b 100644 --- a/Binaries/UnivBackPred2.sx +++ b/Binaries/UnivBackPred2.sx @@ -80,6 +80,8 @@ ; Reflect plus
(FORALL (a b) (PATS (Reflect$Add a b)) (EQ (Reflect$Add a b) (+ a b)))
+ (EQ (tickleBool |@false|) |@true|)
+ (EQ (tickleBool |@true|) |@true|)
)) ;; AND, BG_PUSH
; End Boogie universal background predicate
; -------------------------------------------------------------------------
diff --git a/Source/AIFramework/Expr.ssc b/Source/AIFramework/Expr.ssc index 42621239..1f21f84a 100644 --- a/Source/AIFramework/Expr.ssc +++ b/Source/AIFramework/Expr.ssc @@ -26,7 +26,7 @@ namespace Microsoft.AbstractInterpretationFramework /// AST nodes as AIF expressions.
///
/// This only serves as a place for operations on expressions. Clients
- /// should implement directly either IVariable or IFunApp.
+ /// should implement directly IVariable, IFunApp, ...
/// </summary>
public interface IExpr
{
@@ -90,6 +90,14 @@ namespace Microsoft.AbstractInterpretationFramework }
/// <summary>
+ /// An interface representing an expression that at any moment could, in principle, evaluate
+ /// to a different value. That is, the abstract interpreter should treat these IExpr's
+ /// as unknown values. They are used when there is no other IExpr corresponding to the
+ /// expression to be modeled.
+ /// </summary>
+ public interface IUnknown : IExpr {}
+
+ /// <summary>
/// An abstract class that provides an interface for expression visitors.
/// </summary>
public abstract class ExprVisitor
@@ -147,6 +155,10 @@ namespace Microsoft.AbstractInterpretationFramework else
result = fun.CloneWithBody(Substitute(subst, var, fun.Body));
}
+ else if (inexpr is IUnknown)
+ {
+ result = inexpr;
+ }
else
{
assert false;
diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc index c0293493..ab030b59 100644 --- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc +++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc @@ -78,7 +78,7 @@ namespace Microsoft.AbstractInterpretationFramework public bool IsBottom {
get {
- return this.constraints == null; + return this.constraints == null;
}
}
@@ -89,7 +89,7 @@ namespace Microsoft.AbstractInterpretationFramework requires !this.IsBottom;
{
assume this.constraints != null;
- return (!) this.constraints.Keys; + return (!) this.constraints.Keys;
}
}
@@ -117,7 +117,7 @@ namespace Microsoft.AbstractInterpretationFramework requires !this.IsBottom;
{
assume this.constraints != null;
- return (Element)constraints[key]; + return (Element)constraints[key];
}
}
@@ -303,7 +303,7 @@ namespace Microsoft.AbstractInterpretationFramework }
Elt! join = new Elt(newMap);
- // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join)); + // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
return join;
}
@@ -368,9 +368,9 @@ namespace Microsoft.AbstractInterpretationFramework }
Element! widen= new Elt(newMap);
- // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen)); + // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
- return widen; + return widen;
}
internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)
@@ -400,6 +400,10 @@ namespace Microsoft.AbstractInterpretationFramework // Ignore the bound variable
s.AddAll(VariablesInExpression(lambda.Body, (!) Set.Union(ignoreVars, x)));
}
+ else if (e is IUnknown)
+ {
+ // skip (actually, it would be appropriate to return the universal set of all variables)
+ }
else
{
Debug.Assert(false, "case not handled: " + e);
@@ -482,7 +486,7 @@ namespace Microsoft.AbstractInterpretationFramework else
{
IExpr! left = (IExpr!) fun.Arguments[0];
- IExpr! right = (IExpr!) fun.Arguments[1]; + IExpr! right = (IExpr!) fun.Arguments[1];
if(!(left is IVariable || right is IVariable)) // At least one of the two operands must be a variable
return false;
@@ -493,7 +497,7 @@ namespace Microsoft.AbstractInterpretationFramework || fun.FunctionSymbol.Equals(Int.Mul)
|| fun.FunctionSymbol.Equals(Int.Div)
|| fun.FunctionSymbol.Equals(Int.Mod))
- return IsArithmeticExpr(left) && IsArithmeticExpr(right); + return IsArithmeticExpr(left) && IsArithmeticExpr(right);
else
return false;
}
@@ -592,6 +596,12 @@ namespace Microsoft.AbstractInterpretationFramework );
}
+ // else
+
+ if (expr is IUnknown) {
+ return expr;
+ }
+
else
{
throw
diff --git a/Source/AbsInt/LoopInvariantsOnDemand.cs b/Source/AbsInt/LoopInvariantsOnDemand.cs index 49958289..5bb5916d 100644 --- a/Source/AbsInt/LoopInvariantsOnDemand.cs +++ b/Source/AbsInt/LoopInvariantsOnDemand.cs @@ -55,6 +55,8 @@ namespace Microsoft.Boogie.AbstractInterpretation { return VisitFunApp((AI.IFunApp)expr);
else if (expr is AI.IFunction)
return VisitFunction((AI.IFunction)expr);
+ else if (expr is AI.IUnknown)
+ return null;
else {
Contract.Assert(false);
throw new cce.UnreachableException();
diff --git a/Source/Core/Absy.ssc b/Source/Core/Absy.ssc index fbc2d253..22d21f0c 100644 --- a/Source/Core/Absy.ssc +++ b/Source/Core/Absy.ssc @@ -881,7 +881,7 @@ namespace Microsoft.Boogie p.Parent.Emit(stream);
}
if (ChildrenComplete)
- stream.Write(this, level, " complete"); + stream.Write(this, level, " complete");
}
stream.WriteLine(";");
@@ -1119,7 +1119,7 @@ namespace Microsoft.Boogie // Register all type parameters at the resolution context
protected void RegisterTypeParameters(ResolutionContext! rc) {
foreach (TypeVariable! v in TypeParameters)
- rc.AddTypeBinder(v); + rc.AddTypeBinder(v);
}
protected void SortTypeParams() {
@@ -1812,7 +1812,7 @@ namespace Microsoft.Boogie v.ResolveWhere(rc);
}
- rc.StartProcedureContext();
+ rc.PushProcedureContext();
foreach (Block b in Blocks)
{
b.Register(rc);
@@ -1827,7 +1827,7 @@ namespace Microsoft.Boogie }
rc.StateMode = ResolutionContext.State.Single;
- rc.EndProcedureContext();
+ rc.PopProcedureContext();
rc.PopVarContext();
Type.CheckBoundVariableOccurrences(TypeParameters,
diff --git a/Source/Core/AbsyCmd.ssc b/Source/Core/AbsyCmd.ssc index b24e83e3..7aa3e1fc 100644 --- a/Source/Core/AbsyCmd.ssc +++ b/Source/Core/AbsyCmd.ssc @@ -1467,7 +1467,7 @@ namespace Microsoft.Boogie int previousTypeBinderState = rc.TypeBinderState;
try {
foreach (TypeVariable! v in Proc.TypeParameters)
- rc.AddTypeBinder(v); + rc.AddTypeBinder(v);
Type.CheckBoundVariableOccurrences(Proc.TypeParameters,
formalInTypes, formalOutTypes,
this.tok, "types of given arguments",
@@ -1578,7 +1578,7 @@ namespace Microsoft.Boogie // cins : new variables created just for this call, one per ains
// cframe : new variables created just for this call, to keep track of OLD values
// couts : new variables created just for this call, one per aouts
- // WildcarVars : new variables created just for this call, one per null in ains
+ // WildcardVars : new variables created just for this call, one per null in ains
#region Create cins; each one is an incarnation of the corresponding in parameter
VariableSeq! cins = new VariableSeq();
diff --git a/Source/Core/AbsyExpr.ssc b/Source/Core/AbsyExpr.ssc index 5947c822..250820ed 100644 --- a/Source/Core/AbsyExpr.ssc +++ b/Source/Core/AbsyExpr.ssc @@ -81,19 +81,19 @@ namespace Microsoft.Boogie // Handy syntactic sugar follows:
- public static NAryExpr! Binary (IToken! x, BinaryOperator.Opcode op, Expr! e1, Expr! e2)
+ public static NAryExpr! Unary (IToken! x, UnaryOperator.Opcode op, Expr! e1)
{
- return new NAryExpr(x, new BinaryOperator(x, op), new ExprSeq(e1, e2));
+ return new NAryExpr(x, new UnaryOperator(x, op), new ExprSeq(e1));
}
- public static NAryExpr! Unary (IToken! x, UnaryOperator.Opcode op, Expr! e1)
+ public static NAryExpr! Binary (IToken! x, BinaryOperator.Opcode op, Expr! e0, Expr! e1)
{
- return new NAryExpr(x, new UnaryOperator(x, op), new ExprSeq(e1));
+ return new NAryExpr(x, new BinaryOperator(x, op), new ExprSeq(e0, e1));
}
- public static NAryExpr! Binary (BinaryOperator.Opcode op, Expr! e1, Expr! e2)
+ public static NAryExpr! Binary (BinaryOperator.Opcode op, Expr! e0, Expr! e1)
{
- return new NAryExpr(Token.NoToken, new BinaryOperator(Token.NoToken, op), new ExprSeq(e1, e2));
+ return Binary(Token.NoToken, op, e0, e1);
}
public static NAryExpr! Eq (Expr! e1, Expr! e2) { return Binary(BinaryOperator.Opcode.Eq, e1, e2); }
@@ -115,7 +115,7 @@ namespace Microsoft.Boogie else { return Binary(BinaryOperator.Opcode.Or, e1, e2); }
}
public static Expr! Not (Expr! e1) {
- NAryExpr nary = e1 as NAryExpr; + NAryExpr nary = e1 as NAryExpr;
if (e1 == true_) { return false_; }
else if (e1 == false_) { return true_; }
@@ -480,7 +480,7 @@ namespace Microsoft.Boogie public override bool Equals(object obj)
{
BvConst other = obj as BvConst;
- if (other == null) return false; + if (other == null) return false;
return Bits == other.Bits && Value == other.Value;
}
@@ -1375,8 +1375,8 @@ namespace Microsoft.Boogie case Opcode.Imp: if (e1 is bool && e2 is bool) { return ! (bool)e1 || (bool)e2; } break;
case Opcode.Iff: if (e1 is bool && e2 is bool) { return e1 == e2; } break;
- case Opcode.Eq: return Equals(e1,e2); - case Opcode.Neq: return ! Equals(e1,e2); + case Opcode.Eq: return Equals(e1,e2);
+ case Opcode.Neq: return ! Equals(e1,e2);
case Opcode.Subtype: throw new System.NotImplementedException();
}
@@ -1942,7 +1942,7 @@ namespace Microsoft.Boogie return null;
}
- return ((!)args[0]).Type; + return ((!)args[0]).Type;
}
public Type Typecheck(ref ExprSeq! args,
@@ -2071,25 +2071,22 @@ namespace Microsoft.Boogie - public class BlockExpr : Expr
+ public class CodeExpr : Expr, AI.IUnknown
{
public VariableSeq! LocVars;
[Rep]
- public BlockSeq! Blocks;
- public BlockExpr(VariableSeq! localVariables, BlockSeq! blocks)
+ public List<Block!>! Blocks;
+ public CodeExpr(VariableSeq! localVariables, List<Block!>! blocks)
: base(Token.NoToken)
+ requires 0 < blocks.Count;
{
LocVars = localVariables;
Blocks = blocks;
}
- public override AI.IExpr! IExpr {
- get {
- // An BlockExpr has no AI.IExpr representation
- assert false;
- throw new System.Exception(); // make compiler shut up
- return Expr.False;
- }
- }
+
+ public override AI.IExpr! IExpr { get { return this; } }
+ [Pure] public object DoVisit(AI.ExprVisitor! visitor) { return this; }
+
public override void ComputeFreeVariables(Set /*Variable*/! freeVars) {
// Treat a BlockEexpr as if it has no free variables at all
}
@@ -2097,7 +2094,7 @@ namespace Microsoft.Boogie {
//level++;
int level = 0;
- stream.WriteLine(level, "{0}", '{');
+ stream.WriteLine(level, "|{");
if (this.LocVars.Length > 0)
{
@@ -2112,7 +2109,7 @@ namespace Microsoft.Boogie }
stream.WriteLine();
- stream.WriteLine(level, "{0}", '}');
+ stream.WriteLine(level, "}|");
stream.WriteLine();
stream.WriteLine();
@@ -2128,7 +2125,7 @@ namespace Microsoft.Boogie v.Resolve(rc);
}
- rc.StartProcedureContext();
+ rc.PushProcedureContext();
foreach (Block! b in Blocks)
{
b.Register(rc);
@@ -2139,7 +2136,7 @@ namespace Microsoft.Boogie b.Resolve(rc);
}
- rc.EndProcedureContext();
+ rc.PopProcedureContext();
rc.PopVarContext();
}
@@ -2160,7 +2157,7 @@ namespace Microsoft.Boogie public override Absy! StdDispatch(StandardVisitor! visitor)
{
- return visitor.VisitBlockExpr(this);
+ return visitor.VisitCodeExpr(this);
}
}
@@ -2272,7 +2269,7 @@ namespace Microsoft.Boogie }
public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)
{
- AI.IFunApp! retFun; + AI.IFunApp! retFun;
if(args.Count == 3)
{
@@ -2403,7 +2400,7 @@ namespace Microsoft.Boogie }
public AI.IFunApp! CloneWithArguments(IList/*<AI.IExpr!>*/! args)
{
- AI.IFunApp! retFun; + AI.IFunApp! retFun;
if(args.Count == 2)
{
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 42f9f735..fe302acb 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -38,7 +38,6 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines, FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
-// Scanner scanner = new Scanner(stream);
if (defines == null) {
defines = new List<string!>();
@@ -49,9 +48,6 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines, Errors errors = new Errors();
Scanner scanner = new Scanner(ms, errors, filename);
-/*
- Scanner scanner = new Scanner(filename);
-*/
Parser parser = new Parser(scanner, errors);
Pgm = new Program(); // reset the global variable
parser.Parse();
@@ -65,48 +61,7 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines, program = null;
return parser.errors.count;
}
-/*
- using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
- Buffer.Fill(reader);
- Scanner.Init(filename);
- return Parse(out program);
- }
-*/
-}
-
-///<summary>
-///Returns the number of parsing errors encountered. If 0, "program" returns as
-///the parsed program.
-///Note: first initialize the Scanner.
-///</summary>
-//public static int Parse (out /*maybe null*/ Program program) {
-// Pgm = new Program(); // reset the global variable
-// Parse();
-// if (Errors.count == 0)
-// {
-// program = Pgm;
-// return 0;
-// }
-// else
-// {
-// program = null;
-// return Errors.count;
-// }
-//}
-
-/*
-public static int ParseProposition (string! text, out Expr! expression)
-{
- Buffer.Fill(text);
- Scanner.Init(string.Format("\"{0}\"", text));
-
- Errors.SynErr = new ErrorProc(SynErr);
- la = new Token();
- Get();
- Proposition(out expression);
- return Errors.count;
}
-*/
// Class to represent the bounds of a bitvector expression t[a:b].
// Objects of this class only exist during parsing and are directly
@@ -639,60 +594,13 @@ SpecPrePost<bool free, RequiresSeq! pre, EnsuresSeq! post> = (. Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; .)
( "requires" (. tok = t; .)
{ Attribute<ref kv> }
- (Proposition<out e> ";" (. pre.Add(new Requires(tok, free, e, null, kv)); .)
- |
- SpecBody<out locals, out blocks> ";"
- (. pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); .)
- )
+ Proposition<out e> ";" (. pre.Add(new Requires(tok, free, e, null, kv)); .)
| "ensures" (. tok = t; .)
{ Attribute<ref kv> }
- (Proposition<out e> ";" (. post.Add(new Ensures(tok, free, e, null, kv)); .)
- |
- SpecBody<out locals, out blocks> ";"
- (. post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); .)
- )
+ Proposition<out e> ";" (. post.Add(new Ensures(tok, free, e, null, kv)); .)
)
.
-SpecBody<out VariableSeq! locals, out BlockSeq! blocks>
-= (. locals = new VariableSeq(); Block! b; .)
- "{{"
- { LocalVars<locals> }
- SpecBlock<out b> (. blocks = new BlockSeq(b); .)
- { SpecBlock<out b> (. blocks.Add(b); .)
- }
- "}}"
- .
-
-SpecBlock<out Block! b>
-= (. IToken! x; IToken! y;
- Cmd c; IToken label;
- CmdSeq cs = new CmdSeq();
- TokenSeq! xs;
- StringSeq ss = new StringSeq();
- b = dummyBlock;
- Expr! e;
- .)
- Ident<out x> ":"
- { LabelOrCmd<out c, out label>
- (. if (c != null) {
- assert label == null;
- cs.Add(c);
- } else {
- assert label != null;
- this.SemErr("SpecBlock's can only have one label");
- }
- .)
- }
- ( "goto" (. y = t; .)
- Idents<out xs> (. foreach (IToken! s in xs) { ss.Add(s.val); }
- b = new Block(x,x.val,cs,new GotoCmd(y,ss));
- .)
- | "return" Expression<out e>
- (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)
- ) ";"
- .
-
/*------------------------------------------------------------------------*/
ImplBody<out VariableSeq! locals, out StmtList! stmtList>
@@ -891,21 +799,29 @@ LabelOrCmd<out Cmd c, out IToken label> LabelOrAssign<out Cmd c, out IToken label>
/* ensures (c == null) != (label != null) */
-= (. IToken! id; IToken! x; Expr! e, e0;
+= (. IToken! id; IToken! x, y; Expr! e, e0;
c = dummyCmd; label = null;
AssignLhs! lhs;
List<AssignLhs!>! lhss;
List<Expr!>! rhss;
+ List<Expr!>! indexes;
.)
Ident<out id> (. x = t; .)
( ":" (. c = null; label = x; .)
- |
- MapAssignIndexes<id, out lhs> (. lhss = new List<AssignLhs!> ();
- lhss.Add(lhs); .)
+
+ | (. lhss = new List<AssignLhs!>(); .)
+ (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
+
+ { MapAssignIndex<out y, out indexes> (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
+ (. lhss.Add(lhs); .)
+
{ ","
Ident<out id>
- MapAssignIndexes<id, out lhs> (. lhss.Add(lhs); .)
+ (. lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val)); .)
+ { MapAssignIndex<out y, out indexes> (. lhs = new MapAssignLhs(y, lhs, indexes); .) }
+ (. lhss.Add(lhs); .)
}
+
":=" (. x = t; /* use location of := */ .)
Expression<out e0> (. rhss = new List<Expr!> ();
rhss.Add(e0); .)
@@ -916,27 +832,18 @@ LabelOrAssign<out Cmd c, out IToken label> )
.
-MapAssignIndexes<IToken! assignedVariable, out AssignLhs! lhs>
-= (. IToken! x;
- AssignLhs! runningLhs =
- new SimpleAssignLhs(assignedVariable,
- new IdentifierExpr(assignedVariable, assignedVariable.val));
- List<Expr!>! indexes;
- Expr! e0;
+MapAssignIndex<.out IToken! x, out List<Expr!>! indexes.>
+= (. indexes = new List<Expr!> ();
+ Expr! e;
.)
- {
- "[" (. x = t;
- indexes = new List<Expr!> (); .)
- [
- Expression<out e0> (. indexes.Add(e0); .)
- { ","
- Expression<out e0> (. indexes.Add(e0); .)
- }
- ]
- "]" (. runningLhs =
- new MapAssignLhs (x, runningLhs, indexes); .)
- }
- (. lhs = runningLhs; .)
+ "[" (. x = t; .)
+ [
+ Expression<out e> (. indexes.Add(e); .)
+ { ","
+ Expression<out e> (. indexes.Add(e); .)
+ }
+ ]
+ "]"
.
/*------------------------------------------------------------------------*/
@@ -1296,6 +1203,8 @@ AtomExpression<out Expr! e> Bpl.Type! ty;
QKeyValue kv;
e = dummyExpr;
+ VariableSeq! locals;
+ List<Block!>! blocks;
.)
( "false" (. e = new LiteralExpr(t, false); .)
| "true" (. e = new LiteralExpr(t, true); .)
@@ -1335,9 +1244,52 @@ AtomExpression<out Expr! e> )
")"
| IfThenElseExpression<out e>
+ | CodeExpression<out locals, out blocks> (. e = new CodeExpr(locals, blocks); .)
)
.
+CodeExpression<.out VariableSeq! locals, out List<Block!>! blocks.>
+= (. locals = new VariableSeq(); Block! b;
+ blocks = new List<Block!>();
+ .)
+ "|{"
+ { LocalVars<locals> }
+ SpecBlock<out b> (. blocks.Add(b); .)
+ { SpecBlock<out b> (. blocks.Add(b); .)
+ }
+ "}|"
+ .
+
+SpecBlock<out Block! b>
+= (. IToken! x; IToken! y;
+ Cmd c; IToken label;
+ CmdSeq cs = new CmdSeq();
+ TokenSeq! xs;
+ StringSeq ss = new StringSeq();
+ b = dummyBlock;
+ Expr! e;
+ .)
+ Ident<out x> ":"
+ { LabelOrCmd<out c, out label>
+ (. if (c != null) {
+ assert label == null;
+ cs.Add(c);
+ } else {
+ assert label != null;
+ SemErr("SpecBlock's can only have one label");
+ }
+ .)
+ }
+ ( "goto" (. y = t; .)
+ Idents<out xs> (. foreach (IToken! s in xs) { ss.Add(s.val); }
+ b = new Block(x,x.val,cs,new GotoCmd(y,ss));
+ .)
+ | "return" Expression<out e>
+ (. b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); .)
+ )
+ ";"
+ .
+
Attribute<ref QKeyValue kv>
= (. Trigger trig = null; .)
AttributeOrTrigger<ref kv, ref trig> (. if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); .)
diff --git a/Source/Core/Duplicator.ssc b/Source/Core/Duplicator.ssc index 667eaf5e..f265ee35 100644 --- a/Source/Core/Duplicator.ssc +++ b/Source/Core/Duplicator.ssc @@ -52,9 +52,35 @@ namespace Microsoft.Boogie {
return base.VisitBlock ((Block)node.Clone());
}
+ public override Expr! VisitCodeExpr(CodeExpr! node)
+ {
+ CodeExpr clone = (CodeExpr)base.VisitCodeExpr((CodeExpr)node.Clone());
+ // Before returning, fix up the resolved goto targets
+ assert node.Blocks.Count == clone.Blocks.Count;
+ Dictionary<Block,Block> subst = new Dictionary<Block,Block>();
+ for (int i = 0; i < node.Blocks.Count; i++) {
+ subst.Add(node.Blocks[i], clone.Blocks[i]);
+ }
+ foreach (Block! b in clone.Blocks) {
+ GotoCmd g = b.TransferCmd as GotoCmd;
+ if (g != null) {
+ BlockSeq targets = new BlockSeq();
+ foreach (Block t in (!)g.labelTargets) {
+ Block nt = subst[t];
+ targets.Add(nt);
+ }
+ g.labelTargets = targets;
+ }
+ }
+ return clone;
+ }
public override BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)
{
- return base.VisitBlockSeq (blockSeq);
+ return base.VisitBlockSeq (new BlockSeq(blockSeq));
+ }
+ public override List<Block!>! VisitBlockList(List<Block!>! blocks)
+ {
+ return base.VisitBlockList (new List<Block!>(blocks));
}
public override BoundVariable! VisitBoundVariable(BoundVariable! node)
{
@@ -206,6 +232,10 @@ namespace Microsoft.Boogie {
return base.VisitReturnCmd ((ReturnCmd) node.Clone());
}
+ public override ReturnExprCmd! VisitReturnExprCmd(ReturnExprCmd! node)
+ {
+ return base.VisitReturnExprCmd((ReturnExprCmd)node.Clone());
+ }
public override Sequential! VisitSequential(Sequential! node)
{
return base.VisitSequential ((Sequential) node.Clone());
@@ -245,11 +275,11 @@ namespace Microsoft.Boogie }
public override Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
{
- return base.VisitAssertRequiresCmd((AssertRequiresCmd)node.Clone()); + return base.VisitAssertRequiresCmd((AssertRequiresCmd)node.Clone());
}
public override Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
{
- return base.VisitAssertEnsuresCmd((AssertEnsuresCmd)node.Clone()); + return base.VisitAssertEnsuresCmd((AssertEnsuresCmd)node.Clone());
}
public override Ensures! VisitEnsures(Ensures! node)
{
diff --git a/Source/Core/Parser.ssc b/Source/Core/Parser.ssc index 432c5ab2..68148acf 100644 --- a/Source/Core/Parser.ssc +++ b/Source/Core/Parser.ssc @@ -57,7 +57,6 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines, FileStream stream = new FileStream(filename, FileMode.Open, FileAccess.Read, FileShare.Read);
-// Scanner scanner = new Scanner(stream);
if (defines == null) {
defines = new List<string!>();
@@ -68,9 +67,6 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines, Errors errors = new Errors();
Scanner scanner = new Scanner(ms, errors, filename);
-/*
- Scanner scanner = new Scanner(filename);
-*/
Parser parser = new Parser(scanner, errors);
Pgm = new Program(); // reset the global variable
parser.Parse();
@@ -84,49 +80,8 @@ public static int Parse (string! filename, /*maybe null*/ List<string!> defines, program = null;
return parser.errors.count;
}
-/*
- using (System.IO.StreamReader reader = new System.IO.StreamReader(filename)) {
- Buffer.Fill(reader);
- Scanner.Init(filename);
- return Parse(out program);
- }
-*/
}
-///<summary>
-///Returns the number of parsing errors encountered. If 0, "program" returns as
-///the parsed program.
-///Note: first initialize the Scanner.
-///</summary>
-//public static int Parse (out /*maybe null*/ Program program) {
-// Pgm = new Program(); // reset the global variable
-// Parse();
-// if (Errors.count == 0)
-// {
-// program = Pgm;
-// return 0;
-// }
-// else
-// {
-// program = null;
-// return Errors.count;
-// }
-//}
-
-/*
-public static int ParseProposition (string! text, out Expr! expression)
-{
- Buffer.Fill(text);
- Scanner.Init(string.Format("\"{0}\"", text));
-
- Errors.SynErr = new ErrorProc(SynErr);
- la = new Token();
- Get();
- Proposition(out expression);
- return Errors.count;
-}
-*/
-
// Class to represent the bounds of a bitvector expression t[a:b].
// Objects of this class only exist during parsing and are directly
// turned into BvExtract before they get anywhere else
@@ -241,7 +196,7 @@ private class BvBounds : Expr { }
case 27: {
Axiom(out ax);
- Pgm.TopLevelDeclarations.Add(ax); + Pgm.TopLevelDeclarations.Add(ax);
break;
}
case 28: {
@@ -267,7 +222,7 @@ private class BvBounds : Expr { }
case 31: {
Implementation(out nnim);
- Pgm.TopLevelDeclarations.Add(nnim); + Pgm.TopLevelDeclarations.Add(nnim);
break;
}
}
@@ -280,15 +235,15 @@ private class BvBounds : Expr { ds = new VariableSeq();
bool u = false; QKeyValue kv = null;
bool ChildrenComplete = false;
- List<ConstantParent!> Parents = null; + List<ConstantParent!> Parents = null;
Expect(19);
- y = t; + y = t;
while (la.kind == 25) {
Attribute(ref kv);
}
if (la.kind == 20) {
Get();
- u = true; + u = true;
}
IdsType(out xs);
if (la.kind == 21) {
@@ -339,11 +294,11 @@ private class BvBounds : Expr { Expect(8);
if (StartOf(2)) {
VarOrType(out tyd);
- arguments.Add(new Formal(tyd.tok, tyd, true)); + arguments.Add(new Formal(tyd.tok, tyd, true));
while (la.kind == 11) {
Get();
VarOrType(out tyd);
- arguments.Add(new Formal(tyd.tok, tyd, true)); + arguments.Add(new Formal(tyd.tok, tyd, true));
}
}
Expect(9);
@@ -352,16 +307,16 @@ private class BvBounds : Expr { Expect(8);
VarOrType(out tyd);
Expect(9);
- retTyd = tyd; + retTyd = tyd;
} else if (la.kind == 10) {
Get();
Type(out retTy);
- retTyd = new TypedIdent(retTy.tok, "", retTy); + retTyd = new TypedIdent(retTy.tok, "", retTy);
} else SynErr(89);
if (la.kind == 25) {
Get();
Expression(out tmp);
- definition = tmp; + definition = tmp;
Expect(26);
} else if (la.kind == 7) {
Get();
@@ -440,35 +395,35 @@ private class BvBounds : Expr { }
void Axiom(out Axiom! m) {
- Expr! e; QKeyValue kv = null; + Expr! e; QKeyValue kv = null;
Expect(27);
while (la.kind == 25) {
Attribute(ref kv);
}
- IToken! x = t; + IToken! x = t;
Proposition(out e);
Expect(7);
- m = new Axiom(x,e, null, kv); + m = new Axiom(x,e, null, kv);
}
void UserDefinedTypes(out List<Declaration!>! ts) {
- Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> (); + Declaration! decl; QKeyValue kv = null; ts = new List<Declaration!> ();
Expect(28);
while (la.kind == 25) {
Attribute(ref kv);
}
UserDefinedType(out decl, kv);
- ts.Add(decl); + ts.Add(decl);
while (la.kind == 11) {
Get();
UserDefinedType(out decl, kv);
- ts.Add(decl); + ts.Add(decl);
}
Expect(7);
}
void GlobalVars(out VariableSeq! ds) {
- TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null; + TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null;
Expect(6);
while (la.kind == 25) {
Attribute(ref kv);
@@ -507,10 +462,10 @@ private class BvBounds : Expr { }
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams,
- Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors); + Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, null, this.errors);
} else SynErr(91);
- proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv); + proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
void Implementation(out Implementation! impl) {
@@ -524,13 +479,13 @@ private class BvBounds : Expr { Expect(31);
ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
ImplBody(out locals, out stmtList);
- impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors); + impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors);
}
void Attribute(ref QKeyValue kv) {
- Trigger trig = null; + Trigger trig = null;
AttributeOrTrigger(ref kv, ref trig);
- if (trig != null) this.SemErr("only attributes, not triggers, allowed here"); + if (trig != null) this.SemErr("only attributes, not triggers, allowed here");
}
void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq! tyds) {
@@ -542,7 +497,7 @@ private class BvBounds : Expr { }
void LocalVars(VariableSeq! ds) {
- TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null; + TypedIdentSeq! tyds = new TypedIdentSeq(); QKeyValue kv = null;
Expect(6);
while (la.kind == 25) {
Attribute(ref kv);
@@ -556,7 +511,7 @@ private class BvBounds : Expr { }
void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq! ds) {
- TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); + TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq();
Expect(8);
if (la.kind == 1) {
IdsTypeWheres(allowWhereClauses, tyds);
@@ -569,7 +524,7 @@ private class BvBounds : Expr { }
void BoundVars(IToken! x, out VariableSeq! ds) {
- TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq(); + TypedIdentSeq! tyds = new TypedIdentSeq(); ds = new VariableSeq();
IdsTypeWheres(false, tyds);
foreach (TypedIdent! tyd in tyds) {
ds.Add(new BoundVariable(tyd.tok, tyd));
@@ -578,7 +533,7 @@ private class BvBounds : Expr { }
void IdsType(out TypedIdentSeq! tyds) {
- TokenSeq! ids; Bpl.Type! ty; + TokenSeq! ids; Bpl.Type! ty;
Idents(out ids);
Expect(10);
Type(out ty);
@@ -590,34 +545,34 @@ private class BvBounds : Expr { }
void Idents(out TokenSeq! xs) {
- IToken! id; xs = new TokenSeq(); + IToken! id; xs = new TokenSeq();
Ident(out id);
- xs.Add(id); + xs.Add(id);
while (la.kind == 11) {
Get();
Ident(out id);
- xs.Add(id); + xs.Add(id);
}
}
void Type(out Bpl.Type! ty) {
- IToken! tok; ty = dummyType; + IToken! tok; ty = dummyType;
if (la.kind == 8 || la.kind == 13 || la.kind == 14) {
TypeAtom(out ty);
} else if (la.kind == 1) {
Ident(out tok);
- TypeSeq! args = new TypeSeq (); + TypeSeq! args = new TypeSeq ();
if (StartOf(2)) {
TypeArgs(args);
}
- ty = new UnresolvedTypeIdentifier (tok, tok.val, args); + ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
} else if (la.kind == 15 || la.kind == 17) {
MapType(out ty);
} else SynErr(92);
}
void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq! tyds) {
- TokenSeq! ids; Bpl.Type! ty; Expr wh = null; Expr! nne; + TokenSeq! ids; Bpl.Type! ty; Expr wh = null; Expr! nne;
Idents(out ids);
Expect(10);
Type(out ty);
@@ -638,24 +593,24 @@ private class BvBounds : Expr { }
void Expression(out Expr! e0) {
- IToken! x; Expr! e1; + IToken! x; Expr! e1;
ImpliesExpression(false, out e0);
- while (la.kind == 52 || la.kind == 53) {
+ while (la.kind == 50 || la.kind == 51) {
EquivOp();
- x = t; + x = t;
ImpliesExpression(false, out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1); + e0 = Expr.Binary(x, BinaryOperator.Opcode.Iff, e0, e1);
}
}
void TypeAtom(out Bpl.Type! ty) {
- ty = dummyType; + ty = dummyType;
if (la.kind == 13) {
Get();
- ty = new BasicType(t, SimpleType.Int); + ty = new BasicType(t, SimpleType.Int);
} else if (la.kind == 14) {
Get();
- ty = new BasicType(t, SimpleType.Bool); + ty = new BasicType(t, SimpleType.Bool);
} else if (la.kind == 8) {
Get();
Type(out ty);
@@ -672,23 +627,23 @@ private class BvBounds : Expr { }
void TypeArgs(TypeSeq! ts) {
- IToken! tok; Type! ty; + IToken! tok; Type! ty;
if (la.kind == 8 || la.kind == 13 || la.kind == 14) {
TypeAtom(out ty);
- ts.Add(ty); + ts.Add(ty);
if (StartOf(2)) {
TypeArgs(ts);
}
} else if (la.kind == 1) {
Ident(out tok);
TypeSeq! args = new TypeSeq ();
- ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args)); + ts.Add(new UnresolvedTypeIdentifier (tok, tok.val, args));
if (StartOf(2)) {
TypeArgs(ts);
}
} else if (la.kind == 15 || la.kind == 17) {
MapType(out ty);
- ts.Add(ty); + ts.Add(ty);
} else SynErr(94);
}
@@ -701,10 +656,10 @@ private class BvBounds : Expr { if (la.kind == 17) {
TypeParams(out nnTok, out typeParameters);
- tok = nnTok; + tok = nnTok;
}
Expect(15);
- if (tok == null) tok = t; + if (tok == null) tok = t;
if (StartOf(2)) {
Types(arguments);
}
@@ -715,9 +670,9 @@ private class BvBounds : Expr { }
void TypeParams(out IToken! tok, out Bpl.TypeVariableSeq! typeParams) {
- TokenSeq! typeParamToks; + TokenSeq! typeParamToks;
Expect(17);
- tok = t; + tok = t;
Idents(out typeParamToks);
Expect(18);
typeParams = new TypeVariableSeq ();
@@ -727,13 +682,13 @@ private class BvBounds : Expr { }
void Types(TypeSeq! ts) {
- Bpl.Type! ty; + Bpl.Type! ty;
Type(out ty);
- ts.Add(ty); + ts.Add(ty);
while (la.kind == 11) {
Get();
Type(out ty);
- ts.Add(ty); + ts.Add(ty);
}
}
@@ -741,40 +696,40 @@ private class BvBounds : Expr { ChildrenComplete = false;
Parents = null;
bool u;
- IToken! parent; + IToken! parent;
Expect(21);
Parents = new List<ConstantParent!> ();
- u = false; + u = false;
if (la.kind == 1 || la.kind == 20) {
if (la.kind == 20) {
Get();
- u = true; + u = true;
}
Ident(out parent);
Parents.Add(new ConstantParent (
- new IdentifierExpr(parent, parent.val), u)); + new IdentifierExpr(parent, parent.val), u));
while (la.kind == 11) {
Get();
- u = false; + u = false;
if (la.kind == 20) {
Get();
- u = true; + u = true;
}
Ident(out parent);
Parents.Add(new ConstantParent (
- new IdentifierExpr(parent, parent.val), u)); + new IdentifierExpr(parent, parent.val), u));
}
}
if (la.kind == 22) {
Get();
- ChildrenComplete = true; + ChildrenComplete = true;
}
}
void VarOrType(out TypedIdent! tyd) {
- string! varName = ""; Bpl.Type! ty; IToken! tok; + string! varName = ""; Bpl.Type! ty; IToken! tok;
Type(out ty);
- tok = ty.tok; + tok = ty.tok;
if (la.kind == 10) {
Get();
if (ty is UnresolvedTypeIdentifier &&
@@ -786,7 +741,7 @@ private class BvBounds : Expr { Type(out ty);
}
- tyd = new TypedIdent(tok, varName, ty); + tyd = new TypedIdent(tok, varName, ty);
}
void Proposition(out Expr! e) {
@@ -795,7 +750,7 @@ private class BvBounds : Expr { void UserDefinedType(out Declaration! decl, QKeyValue kv) {
IToken! id; IToken! id2; TokenSeq! paramTokens = new TokenSeq ();
- Type! body = dummyType; bool synonym = false; + Type! body = dummyType; bool synonym = false;
Ident(out id);
if (la.kind == 1) {
WhiteSpaceIdents(out paramTokens);
@@ -803,7 +758,7 @@ private class BvBounds : Expr { if (la.kind == 29) {
Get();
Type(out body);
- synonym = true; + synonym = true;
}
if (synonym) {
TypeVariableSeq! typeParams = new TypeVariableSeq();
@@ -817,19 +772,19 @@ private class BvBounds : Expr { }
void WhiteSpaceIdents(out TokenSeq! xs) {
- IToken! id; xs = new TokenSeq(); + IToken! id; xs = new TokenSeq();
Ident(out id);
- xs.Add(id); + xs.Add(id);
while (la.kind == 1) {
Ident(out id);
- xs.Add(id); + xs.Add(id);
}
}
void ProcSignature(bool allowWhereClausesOnFormals, out IToken! name, out TypeVariableSeq! typeParams,
out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) {
IToken! typeParamTok; typeParams = new TypeVariableSeq();
- outs = new VariableSeq(); kv = null; + outs = new VariableSeq(); kv = null;
while (la.kind == 25) {
Attribute(ref kv);
}
@@ -845,7 +800,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
void Spec(RequiresSeq! pre, IdentifierExprSeq! mods, EnsuresSeq! post) {
- TokenSeq! ms; + TokenSeq! ms;
if (la.kind == 32) {
Get();
if (la.kind == 1) {
@@ -865,7 +820,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
void ImplBody(out VariableSeq! locals, out StmtList! stmtList) {
- locals = new VariableSeq(); + locals = new VariableSeq();
Expect(25);
while (la.kind == 6) {
LocalVars(locals);
@@ -874,133 +829,26 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
void SpecPrePost(bool free, RequiresSeq! pre, EnsuresSeq! post) {
- Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null; + Expr! e; VariableSeq! locals; BlockSeq! blocks; Token tok = null; QKeyValue kv = null;
if (la.kind == 34) {
Get();
- tok = t; + tok = t;
while (la.kind == 25) {
Attribute(ref kv);
}
- if (StartOf(5)) {
- Proposition(out e);
- Expect(7);
- pre.Add(new Requires(tok, free, e, null, kv)); - } else if (la.kind == 36) {
- SpecBody(out locals, out blocks);
- Expect(7);
- pre.Add(new Requires(tok, free, new BlockExpr(locals, blocks), null, kv)); - } else SynErr(96);
+ Proposition(out e);
+ Expect(7);
+ pre.Add(new Requires(tok, free, e, null, kv));
} else if (la.kind == 35) {
Get();
- tok = t; - while (la.kind == 25) {
- Attribute(ref kv);
- }
- if (StartOf(5)) {
- Proposition(out e);
- Expect(7);
- post.Add(new Ensures(tok, free, e, null, kv)); - } else if (la.kind == 36) {
- SpecBody(out locals, out blocks);
- Expect(7);
- post.Add(new Ensures(tok, free, new BlockExpr(locals, blocks), null, kv)); - } else SynErr(97);
- } else SynErr(98);
- }
-
- void SpecBody(out VariableSeq! locals, out BlockSeq! blocks) {
- locals = new VariableSeq(); Block! b; - Expect(36);
- while (la.kind == 6) {
- LocalVars(locals);
- }
- SpecBlock(out b);
- blocks = new BlockSeq(b); - while (la.kind == 1) {
- SpecBlock(out b);
- blocks.Add(b); - }
- Expect(37);
- }
-
- void SpecBlock(out Block! b) {
- IToken! x; IToken! y;
- Cmd c; IToken label;
- CmdSeq cs = new CmdSeq();
- TokenSeq! xs;
- StringSeq ss = new StringSeq();
- b = dummyBlock;
- Expr! e;
-
- Ident(out x);
- Expect(10);
- while (StartOf(6)) {
- LabelOrCmd(out c, out label);
- if (c != null) {
- assert label == null;
- cs.Add(c);
- } else {
- assert label != null;
- this.SemErr("SpecBlock's can only have one label");
- }
-
- }
- if (la.kind == 38) {
- Get();
- y = t; - Idents(out xs);
- foreach (IToken! s in xs) { ss.Add(s.val); }
- b = new Block(x,x.val,cs,new GotoCmd(y,ss));
-
- } else if (la.kind == 39) {
- Get();
- Expression(out e);
- b = new Block(x,x.val,cs,new ReturnExprCmd(t,e)); - } else SynErr(99);
- Expect(7);
- }
-
- void LabelOrCmd(out Cmd c, out IToken label) {
- IToken! x; Expr! e;
- TokenSeq! xs;
- IdentifierExprSeq ids;
- c = dummyCmd; label = null;
- Cmd! cn;
- QKeyValue kv = null;
-
- if (la.kind == 1) {
- LabelOrAssign(out c, out label);
- } else if (la.kind == 46) {
- Get();
- x = t; + tok = t;
while (la.kind == 25) {
Attribute(ref kv);
}
Proposition(out e);
- c = new AssertCmd(x,e, kv); Expect(7);
- } else if (la.kind == 47) {
- Get();
- x = t; - Proposition(out e);
- c = new AssumeCmd(x,e); - Expect(7);
- } else if (la.kind == 48) {
- Get();
- x = t; - Idents(out xs);
- Expect(7);
- ids = new IdentifierExprSeq();
- foreach (IToken! y in xs) {
- ids.Add(new IdentifierExpr(y, y.val));
- }
- c = new HavocCmd(x,ids);
-
- } else if (la.kind == 50) {
- CallCmd(out cn);
- Expect(7);
- c = cn; - } else SynErr(100);
+ post.Add(new Ensures(tok, free, e, null, kv));
+ } else SynErr(96);
}
void StmtList(out StmtList! stmtList) {
@@ -1013,7 +861,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { StructuredCmd ec = null; StructuredCmd! ecn;
TransferCmd tc = null; TransferCmd! tcn;
- while (StartOf(7)) {
+ while (StartOf(5)) {
if (StartOf(6)) {
LabelOrCmd(out c, out label);
if (c != null) {
@@ -1037,7 +885,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { cs = new CmdSeq();
}
- } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {
+ } else if (la.kind == 38 || la.kind == 40 || la.kind == 43) {
StructuredCmd(out ecn);
ec = ecn;
if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); }
@@ -1072,20 +920,63 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
+ void LabelOrCmd(out Cmd c, out IToken label) {
+ IToken! x; Expr! e;
+ TokenSeq! xs;
+ IdentifierExprSeq ids;
+ c = dummyCmd; label = null;
+ Cmd! cn;
+ QKeyValue kv = null;
+
+ if (la.kind == 1) {
+ LabelOrAssign(out c, out label);
+ } else if (la.kind == 44) {
+ Get();
+ x = t;
+ while (la.kind == 25) {
+ Attribute(ref kv);
+ }
+ Proposition(out e);
+ c = new AssertCmd(x,e, kv);
+ Expect(7);
+ } else if (la.kind == 45) {
+ Get();
+ x = t;
+ Proposition(out e);
+ c = new AssumeCmd(x,e);
+ Expect(7);
+ } else if (la.kind == 46) {
+ Get();
+ x = t;
+ Idents(out xs);
+ Expect(7);
+ ids = new IdentifierExprSeq();
+ foreach (IToken! y in xs) {
+ ids.Add(new IdentifierExpr(y, y.val));
+ }
+ c = new HavocCmd(x,ids);
+
+ } else if (la.kind == 48) {
+ CallCmd(out cn);
+ Expect(7);
+ c = cn;
+ } else SynErr(97);
+ }
+
void StructuredCmd(out StructuredCmd! ec) {
ec = dummyStructuredCmd; assume ec.IsPeerConsistent;
IfCmd! ifcmd; WhileCmd! wcmd; BreakCmd! bcmd;
- if (la.kind == 40) {
+ if (la.kind == 38) {
IfCmd(out ifcmd);
- ec = ifcmd; - } else if (la.kind == 42) {
+ ec = ifcmd;
+ } else if (la.kind == 40) {
WhileCmd(out wcmd);
- ec = wcmd; - } else if (la.kind == 45) {
+ ec = wcmd;
+ } else if (la.kind == 43) {
BreakCmd(out bcmd);
- ec = bcmd; - } else SynErr(101);
+ ec = bcmd;
+ } else SynErr(98);
}
void TransferCmd(out TransferCmd! tc) {
@@ -1093,17 +984,17 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Token y; TokenSeq! xs;
StringSeq ss = new StringSeq();
- if (la.kind == 38) {
+ if (la.kind == 36) {
Get();
- y = t; + y = t;
Idents(out xs);
foreach (IToken! s in xs) { ss.Add(s.val); }
tc = new GotoCmd(y, ss);
- } else if (la.kind == 39) {
+ } else if (la.kind == 37) {
Get();
- tc = new ReturnCmd(t); - } else SynErr(102);
+ tc = new ReturnCmd(t);
+ } else SynErr(99);
Expect(7);
}
@@ -1114,23 +1005,23 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { IfCmd! elseIf; IfCmd elseIfOption = null;
StmtList! els; StmtList elseOption = null;
- Expect(40);
- x = t; + Expect(38);
+ x = t;
Guard(out guard);
Expect(25);
StmtList(out thn);
- if (la.kind == 41) {
+ if (la.kind == 39) {
Get();
- if (la.kind == 40) {
+ if (la.kind == 38) {
IfCmd(out elseIf);
- elseIfOption = elseIf; + elseIfOption = elseIf;
} else if (la.kind == 25) {
Get();
StmtList(out els);
- elseOption = els; - } else SynErr(103);
+ elseOption = els;
+ } else SynErr(100);
}
- ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption); + ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
void WhileCmd(out WhileCmd! wcmd) {
@@ -1139,17 +1030,17 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { List<PredicateCmd!> invariants = new List<PredicateCmd!>();
StmtList! body;
- Expect(42);
- x = t; + Expect(40);
+ x = t;
Guard(out guard);
- assume guard == null || Owner.None(guard); - while (la.kind == 33 || la.kind == 43) {
- isFree = false; z = la/*lookahead token*/; + assume guard == null || Owner.None(guard);
+ while (la.kind == 33 || la.kind == 41) {
+ isFree = false; z = la/*lookahead token*/;
if (la.kind == 33) {
Get();
- isFree = true; + isFree = true;
}
- Expect(43);
+ Expect(41);
Expression(out e);
if (isFree) {
invariants.Add(new AssumeCmd(z, e));
@@ -1161,71 +1052,80 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
Expect(25);
StmtList(out body);
- wcmd = new WhileCmd(x, guard, invariants, body); + wcmd = new WhileCmd(x, guard, invariants, body);
}
void BreakCmd(out BreakCmd! bcmd) {
IToken! x; IToken! y;
string breakLabel = null;
- Expect(45);
- x = t; + Expect(43);
+ x = t;
if (la.kind == 1) {
Ident(out y);
- breakLabel = y.val; + breakLabel = y.val;
}
Expect(7);
- bcmd = new BreakCmd(x, breakLabel); + bcmd = new BreakCmd(x, breakLabel);
}
void Guard(out Expr e) {
- Expr! ee; e = null; + Expr! ee; e = null;
Expect(8);
- if (la.kind == 44) {
+ if (la.kind == 42) {
Get();
- e = null; - } else if (StartOf(5)) {
+ e = null;
+ } else if (StartOf(7)) {
Expression(out ee);
- e = ee; - } else SynErr(104);
+ e = ee;
+ } else SynErr(101);
Expect(9);
}
void LabelOrAssign(out Cmd c, out IToken label) {
- IToken! id; IToken! x; Expr! e, e0;
+ IToken! id; IToken! x, y; Expr! e, e0;
c = dummyCmd; label = null;
AssignLhs! lhs;
List<AssignLhs!>! lhss;
List<Expr!>! rhss;
+ List<Expr!>! indexes;
Ident(out id);
- x = t; + x = t;
if (la.kind == 10) {
Get();
- c = null; label = x; - } else if (la.kind == 11 || la.kind == 15 || la.kind == 49) {
- MapAssignIndexes(id, out lhs);
- lhss = new List<AssignLhs!> ();
- lhss.Add(lhs); + c = null; label = x;
+ } else if (la.kind == 11 || la.kind == 15 || la.kind == 47) {
+ lhss = new List<AssignLhs!>();
+ lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
+ while (la.kind == 15) {
+ MapAssignIndex(out y, out indexes);
+ lhs = new MapAssignLhs(y, lhs, indexes);
+ }
+ lhss.Add(lhs);
while (la.kind == 11) {
Get();
Ident(out id);
- MapAssignIndexes(id, out lhs);
- lhss.Add(lhs); + lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
+ while (la.kind == 15) {
+ MapAssignIndex(out y, out indexes);
+ lhs = new MapAssignLhs(y, lhs, indexes);
+ }
+ lhss.Add(lhs);
}
- Expect(49);
+ Expect(47);
x = t; /* use location of := */
Expression(out e0);
rhss = new List<Expr!> ();
- rhss.Add(e0); + rhss.Add(e0);
while (la.kind == 11) {
Get();
Expression(out e0);
- rhss.Add(e0); + rhss.Add(e0);
}
Expect(7);
- c = new AssignCmd(x, lhss, rhss); - } else SynErr(105);
+ c = new AssignCmd(x, lhss, rhss);
+ } else SynErr(102);
}
void CallCmd(out Cmd! c) {
@@ -1236,8 +1136,8 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Expr en; List<Expr> args;
c = dummyCmd;
- Expect(50);
- x = t; + Expect(48);
+ x = t;
while (la.kind == 25) {
Attribute(ref kv);
}
@@ -1247,17 +1147,17 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
if (StartOf(8)) {
CallForallArg(out en);
- es.Add(en); + es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
- es.Add(en); + es.Add(en);
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv); - } else if (la.kind == 11 || la.kind == 49) {
- ids.Add(new IdentifierExpr(first, first.val)); + c = new CallCmd(x, first.val, es, ids, kv);
+ } else if (la.kind == 11 || la.kind == 47) {
+ ids.Add(new IdentifierExpr(first, first.val));
if (la.kind == 11) {
Get();
CallOutIdent(out p);
@@ -1278,40 +1178,40 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
}
- Expect(49);
+ Expect(47);
Ident(out first);
Expect(8);
if (StartOf(8)) {
CallForallArg(out en);
- es.Add(en); + es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
- es.Add(en); + es.Add(en);
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv); - } else SynErr(106);
- } else if (la.kind == 51) {
+ c = new CallCmd(x, first.val, es, ids, kv);
+ } else SynErr(103);
+ } else if (la.kind == 49) {
Get();
Ident(out first);
Expect(8);
- args = new List<Expr>(); + args = new List<Expr>();
if (StartOf(8)) {
CallForallArg(out en);
- args.Add(en); + args.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
- args.Add(en); + args.Add(en);
}
}
Expect(9);
- c = new CallForallCmd(x, first.val, args, kv); - } else if (la.kind == 44) {
+ c = new CallForallCmd(x, first.val, args, kv);
+ } else if (la.kind == 42) {
Get();
- ids.Add(null); + ids.Add(null);
if (la.kind == 11) {
Get();
CallOutIdent(out p);
@@ -1332,330 +1232,320 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
}
- Expect(49);
+ Expect(47);
Ident(out first);
Expect(8);
if (StartOf(8)) {
CallForallArg(out en);
- es.Add(en); + es.Add(en);
while (la.kind == 11) {
Get();
CallForallArg(out en);
- es.Add(en); + es.Add(en);
}
}
Expect(9);
- c = new CallCmd(x, first.val, es, ids, kv); - } else SynErr(107);
+ c = new CallCmd(x, first.val, es, ids, kv);
+ } else SynErr(104);
}
- void MapAssignIndexes(IToken! assignedVariable, out AssignLhs! lhs) {
- IToken! x;
- AssignLhs! runningLhs =
- new SimpleAssignLhs(assignedVariable,
- new IdentifierExpr(assignedVariable, assignedVariable.val));
- List<Expr!>! indexes;
- Expr! e0;
+ void MapAssignIndex(out IToken! x, out List<Expr!>! indexes) {
+ indexes = new List<Expr!> ();
+ Expr! e;
- while (la.kind == 15) {
- Get();
- x = t;
- indexes = new List<Expr!> (); - if (StartOf(5)) {
- Expression(out e0);
- indexes.Add(e0); - while (la.kind == 11) {
- Get();
- Expression(out e0);
- indexes.Add(e0); - }
+ Expect(15);
+ x = t;
+ if (StartOf(7)) {
+ Expression(out e);
+ indexes.Add(e);
+ while (la.kind == 11) {
+ Get();
+ Expression(out e);
+ indexes.Add(e);
}
- Expect(16);
- runningLhs =
- new MapAssignLhs (x, runningLhs, indexes); }
- lhs = runningLhs; + Expect(16);
}
void CallForallArg(out Expr exprOptional) {
exprOptional = null;
Expr! e;
- if (la.kind == 44) {
+ if (la.kind == 42) {
Get();
- } else if (StartOf(5)) {
+ } else if (StartOf(7)) {
Expression(out e);
- exprOptional = e; - } else SynErr(108);
+ exprOptional = e;
+ } else SynErr(105);
}
void CallOutIdent(out IToken id) {
id = null;
IToken! p;
- if (la.kind == 44) {
+ if (la.kind == 42) {
Get();
} else if (la.kind == 1) {
Ident(out p);
- id = p; - } else SynErr(109);
+ id = p;
+ } else SynErr(106);
}
void Expressions(out ExprSeq! es) {
- Expr! e; es = new ExprSeq(); + Expr! e; es = new ExprSeq();
Expression(out e);
- es.Add(e); + es.Add(e);
while (la.kind == 11) {
Get();
Expression(out e);
- es.Add(e); + es.Add(e);
}
}
void ImpliesExpression(bool noExplies, out Expr! e0) {
- IToken! x; Expr! e1; + IToken! x; Expr! e1;
LogicalExpression(out e0);
if (StartOf(9)) {
- if (la.kind == 54 || la.kind == 55) {
+ if (la.kind == 52 || la.kind == 53) {
ImpliesOp();
- x = t; + x = t;
ImpliesExpression(true, out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1); + e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e0, e1);
} else {
ExpliesOp();
if (noExplies)
this.SemErr("illegal mixture of ==> and <==, use parentheses to disambiguate");
- x = t; + x = t;
LogicalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); - while (la.kind == 56 || la.kind == 57) {
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
+ while (la.kind == 54 || la.kind == 55) {
ExpliesOp();
- x = t; + x = t;
LogicalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0); + e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
}
}
}
}
void EquivOp() {
- if (la.kind == 52) {
+ if (la.kind == 50) {
Get();
- } else if (la.kind == 53) {
+ } else if (la.kind == 51) {
Get();
- } else SynErr(110);
+ } else SynErr(107);
}
void LogicalExpression(out Expr! e0) {
- IToken! x; Expr! e1; BinaryOperator.Opcode op; + IToken! x; Expr! e1; BinaryOperator.Opcode op;
RelationalExpression(out e0);
if (StartOf(10)) {
- if (la.kind == 58 || la.kind == 59) {
+ if (la.kind == 56 || la.kind == 57) {
AndOp();
- x = t; + x = t;
RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); - while (la.kind == 58 || la.kind == 59) {
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
+ while (la.kind == 56 || la.kind == 57) {
AndOp();
- x = t; + x = t;
RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1); + e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
}
} else {
OrOp();
- x = t; + x = t;
RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); - while (la.kind == 60 || la.kind == 61) {
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
+ while (la.kind == 58 || la.kind == 59) {
OrOp();
- x = t; + x = t;
RelationalExpression(out e1);
- e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1); + e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
}
}
}
}
void ImpliesOp() {
- if (la.kind == 54) {
+ if (la.kind == 52) {
Get();
- } else if (la.kind == 55) {
+ } else if (la.kind == 53) {
Get();
- } else SynErr(111);
+ } else SynErr(108);
}
void ExpliesOp() {
- if (la.kind == 56) {
+ if (la.kind == 54) {
Get();
- } else if (la.kind == 57) {
+ } else if (la.kind == 55) {
Get();
- } else SynErr(112);
+ } else SynErr(109);
}
void RelationalExpression(out Expr! e0) {
- IToken! x; Expr! e1; BinaryOperator.Opcode op; + IToken! x; Expr! e1; BinaryOperator.Opcode op;
BvTerm(out e0);
if (StartOf(11)) {
RelOp(out x, out op);
BvTerm(out e1);
- e0 = Expr.Binary(x, op, e0, e1); + e0 = Expr.Binary(x, op, e0, e1);
}
}
void AndOp() {
- if (la.kind == 58) {
+ if (la.kind == 56) {
Get();
- } else if (la.kind == 59) {
+ } else if (la.kind == 57) {
Get();
- } else SynErr(113);
+ } else SynErr(110);
}
void OrOp() {
- if (la.kind == 60) {
+ if (la.kind == 58) {
Get();
- } else if (la.kind == 61) {
+ } else if (la.kind == 59) {
Get();
- } else SynErr(114);
+ } else SynErr(111);
}
void BvTerm(out Expr! e0) {
- IToken! x; Expr! e1; + IToken! x; Expr! e1;
Term(out e0);
- while (la.kind == 70) {
+ while (la.kind == 68) {
Get();
- x = t; + x = t;
Term(out e1);
- e0 = new BvConcatExpr(x, e0, e1); + e0 = new BvConcatExpr(x, e0, e1);
}
}
void RelOp(out IToken! x, out BinaryOperator.Opcode op) {
- x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; + x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 62: {
+ case 60: {
Get();
- x = t; op=BinaryOperator.Opcode.Eq; + x = t; op=BinaryOperator.Opcode.Eq;
break;
}
case 17: {
Get();
- x = t; op=BinaryOperator.Opcode.Lt; + x = t; op=BinaryOperator.Opcode.Lt;
break;
}
case 18: {
Get();
- x = t; op=BinaryOperator.Opcode.Gt; + x = t; op=BinaryOperator.Opcode.Gt;
break;
}
- case 63: {
+ case 61: {
Get();
- x = t; op=BinaryOperator.Opcode.Le; + x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 64: {
+ case 62: {
Get();
- x = t; op=BinaryOperator.Opcode.Ge; + x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- case 65: {
+ case 63: {
Get();
- x = t; op=BinaryOperator.Opcode.Neq; + x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 66: {
+ case 64: {
Get();
- x = t; op=BinaryOperator.Opcode.Subtype; + x = t; op=BinaryOperator.Opcode.Subtype;
break;
}
- case 67: {
+ case 65: {
Get();
- x = t; op=BinaryOperator.Opcode.Neq; + x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 68: {
+ case 66: {
Get();
- x = t; op=BinaryOperator.Opcode.Le; + x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 69: {
+ case 67: {
Get();
- x = t; op=BinaryOperator.Opcode.Ge; + x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- default: SynErr(115); break;
+ default: SynErr(112); break;
}
}
void Term(out Expr! e0) {
- IToken! x; Expr! e1; BinaryOperator.Opcode op; + IToken! x; Expr! e1; BinaryOperator.Opcode op;
Factor(out e0);
- while (la.kind == 71 || la.kind == 72) {
+ while (la.kind == 69 || la.kind == 70) {
AddOp(out x, out op);
Factor(out e1);
- e0 = Expr.Binary(x, op, e0, e1); + e0 = Expr.Binary(x, op, e0, e1);
}
}
void Factor(out Expr! e0) {
- IToken! x; Expr! e1; BinaryOperator.Opcode op; + IToken! x; Expr! e1; BinaryOperator.Opcode op;
UnaryExpression(out e0);
- while (la.kind == 44 || la.kind == 73 || la.kind == 74) {
+ while (la.kind == 42 || la.kind == 71 || la.kind == 72) {
MulOp(out x, out op);
UnaryExpression(out e1);
- e0 = Expr.Binary(x, op, e0, e1); + e0 = Expr.Binary(x, op, e0, e1);
}
}
void AddOp(out IToken! x, out BinaryOperator.Opcode op) {
- x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 71) {
+ x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
+ if (la.kind == 69) {
Get();
- x = t; op=BinaryOperator.Opcode.Add; - } else if (la.kind == 72) {
+ x = t; op=BinaryOperator.Opcode.Add;
+ } else if (la.kind == 70) {
Get();
- x = t; op=BinaryOperator.Opcode.Sub; - } else SynErr(116);
+ x = t; op=BinaryOperator.Opcode.Sub;
+ } else SynErr(113);
}
void UnaryExpression(out Expr! e) {
IToken! x;
e = dummyExpr;
- if (la.kind == 72) {
+ if (la.kind == 70) {
Get();
- x = t; + x = t;
UnaryExpression(out e);
- e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); - } else if (la.kind == 75 || la.kind == 76) {
+ e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e);
+ } else if (la.kind == 73 || la.kind == 74) {
NegOp();
- x = t; + x = t;
UnaryExpression(out e);
- e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); + e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
} else if (StartOf(12)) {
CoercionExpression(out e);
- } else SynErr(117);
+ } else SynErr(114);
}
void MulOp(out IToken! x, out BinaryOperator.Opcode op) {
- x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/; - if (la.kind == 44) {
+ x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
+ if (la.kind == 42) {
Get();
- x = t; op=BinaryOperator.Opcode.Mul; - } else if (la.kind == 73) {
+ x = t; op=BinaryOperator.Opcode.Mul;
+ } else if (la.kind == 71) {
Get();
- x = t; op=BinaryOperator.Opcode.Div; - } else if (la.kind == 74) {
+ x = t; op=BinaryOperator.Opcode.Div;
+ } else if (la.kind == 72) {
Get();
- x = t; op=BinaryOperator.Opcode.Mod; - } else SynErr(118);
+ x = t; op=BinaryOperator.Opcode.Mod;
+ } else SynErr(115);
}
void NegOp() {
- if (la.kind == 75) {
+ if (la.kind == 73) {
Get();
- } else if (la.kind == 76) {
+ } else if (la.kind == 74) {
Get();
- } else SynErr(119);
+ } else SynErr(116);
}
void CoercionExpression(out Expr! e) {
@@ -1666,10 +1556,10 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { ArrayExpression(out e);
while (la.kind == 10) {
Get();
- x = t; + x = t;
if (StartOf(2)) {
Type(out coercedTo);
- e = Expr.CoerceType(x, e, coercedTo); + e = Expr.CoerceType(x, e, coercedTo);
} else if (la.kind == 3) {
Nat(out bn);
if (!(e is LiteralExpr) || !((LiteralExpr)e).isBigNum) {
@@ -1679,7 +1569,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(120);
+ } else SynErr(117);
}
}
@@ -1694,9 +1584,9 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Get();
x = t; allArgs = new ExprSeq ();
allArgs.Add(e);
- store = false; bvExtract = false; + store = false; bvExtract = false;
if (StartOf(13)) {
- if (StartOf(5)) {
+ if (StartOf(7)) {
Expression(out index0);
if (index0 is BvBounds)
bvExtract = true;
@@ -1711,7 +1601,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { allArgs.Add(e1);
}
- if (la.kind == 49) {
+ if (la.kind == 47) {
Get();
Expression(out e1);
if (bvExtract || e1 is BvBounds)
@@ -1722,7 +1612,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { } else {
Get();
Expression(out e1);
- allArgs.Add(e1); store = true; + allArgs.Add(e1); store = true;
}
}
Expect(16);
@@ -1733,7 +1623,7 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { ((BvBounds)index0).Upper.ToIntSafe,
((BvBounds)index0).Lower.ToIntSafe);
else
- e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs); + e = new NAryExpr(x, new MapSelect(x, allArgs.Length - 1), allArgs);
}
}
@@ -1757,88 +1647,95 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { Bpl.Type! ty;
QKeyValue kv;
e = dummyExpr;
+ VariableSeq! locals;
+ List<Block!>! blocks;
switch (la.kind) {
- case 77: {
+ case 75: {
Get();
- e = new LiteralExpr(t, false); + e = new LiteralExpr(t, false);
break;
}
- case 78: {
+ case 76: {
Get();
- e = new LiteralExpr(t, true); + e = new LiteralExpr(t, true);
break;
}
case 3: {
Nat(out bn);
- e = new LiteralExpr(t, bn); + e = new LiteralExpr(t, bn);
break;
}
case 2: {
BvLit(out bn, out n);
- e = new LiteralExpr(t, bn, n); + e = new LiteralExpr(t, bn, n);
break;
}
case 1: {
Ident(out x);
- id = new IdentifierExpr(x, x.val); e = id; + id = new IdentifierExpr(x, x.val); e = id;
if (la.kind == 8) {
Get();
- if (StartOf(5)) {
+ if (StartOf(7)) {
Expressions(out es);
- e = new NAryExpr(x, new FunctionCall(id), es); + e = new NAryExpr(x, new FunctionCall(id), es);
} else if (la.kind == 9) {
- e = new NAryExpr(x, new FunctionCall(id), new ExprSeq()); - } else SynErr(121);
+ e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
+ } else SynErr(118);
Expect(9);
}
break;
}
- case 79: {
+ case 77: {
Get();
- x = t; + x = t;
Expect(8);
Expression(out e);
Expect(9);
- e = new OldExpr(x, e); + e = new OldExpr(x, e);
break;
}
case 8: {
Get();
- if (StartOf(5)) {
+ if (StartOf(7)) {
Expression(out e);
if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
- "are not allowed"); - } else if (la.kind == 51 || la.kind == 81) {
+ "are not allowed");
+ } else if (la.kind == 49 || la.kind == 81) {
Forall();
- x = t; + x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
- e = new ForallExpr(x, typeParams, ds, kv, trig, e); + e = new ForallExpr(x, typeParams, ds, kv, trig, e);
} else if (la.kind == 82 || la.kind == 83) {
Exists();
- x = t; + x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
- e = new ExistsExpr(x, typeParams, ds, kv, trig, e); + e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
} else if (la.kind == 84 || la.kind == 85) {
Lambda();
- x = t; + x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (trig != null)
SemErr("triggers not allowed in lambda expressions");
if (typeParams.Length + ds.Length > 0)
- e = new LambdaExpr(x, typeParams, ds, kv, e); - } else SynErr(122);
+ e = new LambdaExpr(x, typeParams, ds, kv, e);
+ } else SynErr(119);
Expect(9);
break;
}
- case 40: {
+ case 38: {
IfThenElseExpression(out e);
break;
}
- default: SynErr(123); break;
+ case 78: {
+ CodeExpression(out locals, out blocks);
+ e = new CodeExpr(locals, blocks);
+ break;
+ }
+ default: SynErr(120); break;
}
}
@@ -1859,11 +1756,11 @@ out VariableSeq! ins, out VariableSeq! outs, out QKeyValue kv) { }
void Forall() {
- if (la.kind == 51) {
+ if (la.kind == 49) {
Get();
} else if (la.kind == 81) {
Get();
- } else SynErr(124);
+ } else SynErr(121);
}
void QuantifierBody(IToken! q, out TypeVariableSeq! typeParams, out VariableSeq! ds,
@@ -1880,7 +1777,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { }
} else if (la.kind == 1) {
BoundVars(q, out ds);
- } else SynErr(125);
+ } else SynErr(122);
QSep();
while (la.kind == 25) {
AttributeOrTrigger(ref kv, ref trig);
@@ -1893,7 +1790,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { Get();
} else if (la.kind == 83) {
Get();
- } else SynErr(126);
+ } else SynErr(123);
}
void Lambda() {
@@ -1901,21 +1798,75 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { Get();
} else if (la.kind == 85) {
Get();
- } else SynErr(127);
+ } else SynErr(124);
}
void IfThenElseExpression(out Expr! e) {
IToken! tok;
- Expr! e0, e1, e2; - e = dummyExpr; - Expect(40);
- tok = t; + Expr! e0, e1, e2;
+ e = dummyExpr;
+ Expect(38);
+ tok = t;
Expression(out e0);
Expect(80);
Expression(out e1);
- Expect(41);
+ Expect(39);
Expression(out e2);
- e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2)); + e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2));
+ }
+
+ void CodeExpression(out VariableSeq! locals, out List<Block!>! blocks) {
+ locals = new VariableSeq(); Block! b;
+ blocks = new List<Block!>();
+
+ Expect(78);
+ while (la.kind == 6) {
+ LocalVars(locals);
+ }
+ SpecBlock(out b);
+ blocks.Add(b);
+ while (la.kind == 1) {
+ SpecBlock(out b);
+ blocks.Add(b);
+ }
+ Expect(79);
+ }
+
+ void SpecBlock(out Block! b) {
+ IToken! x; IToken! y;
+ Cmd c; IToken label;
+ CmdSeq cs = new CmdSeq();
+ TokenSeq! xs;
+ StringSeq ss = new StringSeq();
+ b = dummyBlock;
+ Expr! e;
+
+ Ident(out x);
+ Expect(10);
+ while (StartOf(6)) {
+ LabelOrCmd(out c, out label);
+ if (c != null) {
+ assert label == null;
+ cs.Add(c);
+ } else {
+ assert label != null;
+ SemErr("SpecBlock's can only have one label");
+ }
+
+ }
+ if (la.kind == 36) {
+ Get();
+ y = t;
+ Idents(out xs);
+ foreach (IToken! s in xs) { ss.Add(s.val); }
+ b = new Block(x,x.val,cs,new GotoCmd(y,ss));
+
+ } else if (la.kind == 37) {
+ Get();
+ Expression(out e);
+ b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
+ } else SynErr(125);
+ Expect(7);
}
void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
@@ -1924,18 +1875,18 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { List<object!> parameters; object! param;
Expect(25);
- tok = t; + tok = t;
if (la.kind == 10) {
Get();
Expect(1);
- key = t.val; parameters = new List<object!>(); + key = t.val; parameters = new List<object!>();
if (StartOf(14)) {
AttributeParameter(out param);
- parameters.Add(param); + parameters.Add(param);
while (la.kind == 11) {
Get();
AttributeParameter(out param);
- parameters.Add(param); + parameters.Add(param);
}
}
if (key == "nopats") {
@@ -1957,13 +1908,13 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { }
}
- } else if (StartOf(5)) {
+ } else if (StartOf(7)) {
Expression(out e);
- es = new ExprSeq(e); + es = new ExprSeq(e);
while (la.kind == 11) {
Get();
Expression(out e);
- es.Add(e); + es.Add(e);
}
if (trig==null) {
trig = new Trigger(tok, true, es, null);
@@ -1971,7 +1922,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { trig.AddLast(new Trigger(tok, true, es, null));
}
- } else SynErr(128);
+ } else SynErr(126);
Expect(26);
}
@@ -1981,11 +1932,11 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { if (la.kind == 4) {
Get();
- o = t.val.Substring(1, t.val.Length-2); - } else if (StartOf(5)) {
+ o = t.val.Substring(1, t.val.Length-2);
+ } else if (StartOf(7)) {
Expression(out e);
- o = e; - } else SynErr(129);
+ o = e;
+ } else SynErr(127);
}
void QSep() {
@@ -1993,7 +1944,7 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { Get();
} else if (la.kind == 87) {
Get();
- } else SynErr(130);
+ } else SynErr(128);
}
@@ -2013,16 +1964,16 @@ out QKeyValue kv, out Trigger trig, out Expr! body) { {x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x}
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}
};
} // end Parser
@@ -2075,50 +2026,50 @@ public class Errors { case 33: s = "\"free\" expected"; break;
case 34: s = "\"requires\" expected"; break;
case 35: s = "\"ensures\" expected"; break;
- case 36: s = "\"{{\" expected"; break;
- case 37: s = "\"}}\" expected"; break;
- case 38: s = "\"goto\" expected"; break;
- case 39: s = "\"return\" expected"; break;
- case 40: s = "\"if\" expected"; break;
- case 41: s = "\"else\" expected"; break;
- case 42: s = "\"while\" expected"; break;
- case 43: s = "\"invariant\" expected"; break;
- case 44: s = "\"*\" expected"; break;
- case 45: s = "\"break\" expected"; break;
- case 46: s = "\"assert\" expected"; break;
- case 47: s = "\"assume\" expected"; break;
- case 48: s = "\"havoc\" expected"; break;
- case 49: s = "\":=\" expected"; break;
- case 50: s = "\"call\" expected"; break;
- case 51: s = "\"forall\" expected"; break;
- case 52: s = "\"<==>\" expected"; break;
- case 53: s = "\"\\u21d4\" expected"; break;
- case 54: s = "\"==>\" expected"; break;
- case 55: s = "\"\\u21d2\" expected"; break;
- case 56: s = "\"<==\" expected"; break;
- case 57: s = "\"\\u21d0\" expected"; break;
- case 58: s = "\"&&\" expected"; break;
- case 59: s = "\"\\u2227\" expected"; break;
- case 60: s = "\"||\" expected"; break;
- case 61: s = "\"\\u2228\" expected"; break;
- case 62: s = "\"==\" expected"; break;
- case 63: s = "\"<=\" expected"; break;
- case 64: s = "\">=\" expected"; break;
- case 65: s = "\"!=\" expected"; break;
- case 66: s = "\"<:\" expected"; break;
- case 67: s = "\"\\u2260\" expected"; break;
- case 68: s = "\"\\u2264\" expected"; break;
- case 69: s = "\"\\u2265\" expected"; break;
- case 70: s = "\"++\" expected"; break;
- case 71: s = "\"+\" expected"; break;
- case 72: s = "\"-\" expected"; break;
- case 73: s = "\"/\" expected"; break;
- case 74: s = "\"%\" expected"; break;
- case 75: s = "\"!\" expected"; break;
- case 76: s = "\"\\u00ac\" expected"; break;
- case 77: s = "\"false\" expected"; break;
- case 78: s = "\"true\" expected"; break;
- case 79: s = "\"old\" expected"; break;
+ case 36: s = "\"goto\" expected"; break;
+ case 37: s = "\"return\" expected"; break;
+ case 38: s = "\"if\" expected"; break;
+ case 39: s = "\"else\" expected"; break;
+ case 40: s = "\"while\" expected"; break;
+ case 41: s = "\"invariant\" expected"; break;
+ case 42: s = "\"*\" expected"; break;
+ case 43: s = "\"break\" expected"; break;
+ case 44: s = "\"assert\" expected"; break;
+ case 45: s = "\"assume\" expected"; break;
+ case 46: s = "\"havoc\" expected"; break;
+ case 47: s = "\":=\" expected"; break;
+ case 48: s = "\"call\" expected"; break;
+ case 49: s = "\"forall\" expected"; break;
+ case 50: s = "\"<==>\" expected"; break;
+ case 51: s = "\"\\u21d4\" expected"; break;
+ case 52: s = "\"==>\" expected"; break;
+ case 53: s = "\"\\u21d2\" expected"; break;
+ case 54: s = "\"<==\" expected"; break;
+ case 55: s = "\"\\u21d0\" expected"; break;
+ case 56: s = "\"&&\" expected"; break;
+ case 57: s = "\"\\u2227\" expected"; break;
+ case 58: s = "\"||\" expected"; break;
+ case 59: s = "\"\\u2228\" expected"; break;
+ case 60: s = "\"==\" expected"; break;
+ case 61: s = "\"<=\" expected"; break;
+ case 62: s = "\">=\" expected"; break;
+ case 63: s = "\"!=\" expected"; break;
+ case 64: s = "\"<:\" expected"; break;
+ case 65: s = "\"\\u2260\" expected"; break;
+ case 66: s = "\"\\u2264\" expected"; break;
+ case 67: s = "\"\\u2265\" expected"; break;
+ case 68: s = "\"++\" expected"; break;
+ case 69: s = "\"+\" expected"; break;
+ case 70: s = "\"-\" expected"; break;
+ case 71: s = "\"/\" expected"; break;
+ case 72: s = "\"%\" expected"; break;
+ case 73: s = "\"!\" expected"; break;
+ case 74: s = "\"\\u00ac\" expected"; break;
+ case 75: s = "\"false\" expected"; break;
+ case 76: s = "\"true\" expected"; break;
+ case 77: s = "\"old\" expected"; break;
+ case 78: s = "\"|{\" expected"; break;
+ case 79: s = "\"}|\" expected"; break;
case 80: s = "\"then\" expected"; break;
case 81: s = "\"\\u2200\" expected"; break;
case 82: s = "\"exists\" expected"; break;
@@ -2136,40 +2087,38 @@ public class Errors { case 94: s = "invalid TypeArgs"; break;
case 95: s = "invalid Spec"; break;
case 96: s = "invalid SpecPrePost"; break;
- case 97: s = "invalid SpecPrePost"; break;
- case 98: s = "invalid SpecPrePost"; break;
- case 99: s = "invalid SpecBlock"; break;
- case 100: s = "invalid LabelOrCmd"; break;
- case 101: s = "invalid StructuredCmd"; break;
- case 102: s = "invalid TransferCmd"; break;
- case 103: s = "invalid IfCmd"; break;
- case 104: s = "invalid Guard"; break;
- case 105: s = "invalid LabelOrAssign"; break;
- case 106: s = "invalid CallCmd"; break;
- case 107: s = "invalid CallCmd"; break;
- case 108: s = "invalid CallForallArg"; break;
- case 109: s = "invalid CallOutIdent"; break;
- case 110: s = "invalid EquivOp"; break;
- case 111: s = "invalid ImpliesOp"; break;
- case 112: s = "invalid ExpliesOp"; break;
- case 113: s = "invalid AndOp"; break;
- case 114: s = "invalid OrOp"; break;
- case 115: s = "invalid RelOp"; break;
- case 116: s = "invalid AddOp"; break;
- case 117: s = "invalid UnaryExpression"; break;
- case 118: s = "invalid MulOp"; break;
- case 119: s = "invalid NegOp"; break;
- case 120: s = "invalid CoercionExpression"; break;
- case 121: s = "invalid AtomExpression"; break;
- case 122: s = "invalid AtomExpression"; break;
- case 123: s = "invalid AtomExpression"; break;
- case 124: s = "invalid Forall"; break;
- case 125: s = "invalid QuantifierBody"; break;
- case 126: s = "invalid Exists"; break;
- case 127: s = "invalid Lambda"; break;
- case 128: s = "invalid AttributeOrTrigger"; break;
- case 129: s = "invalid AttributeParameter"; break;
- case 130: s = "invalid QSep"; break;
+ case 97: s = "invalid LabelOrCmd"; break;
+ case 98: s = "invalid StructuredCmd"; break;
+ case 99: s = "invalid TransferCmd"; break;
+ case 100: s = "invalid IfCmd"; break;
+ case 101: s = "invalid Guard"; break;
+ case 102: s = "invalid LabelOrAssign"; break;
+ case 103: s = "invalid CallCmd"; break;
+ case 104: s = "invalid CallCmd"; break;
+ case 105: s = "invalid CallForallArg"; break;
+ case 106: s = "invalid CallOutIdent"; break;
+ case 107: s = "invalid EquivOp"; break;
+ case 108: s = "invalid ImpliesOp"; break;
+ case 109: s = "invalid ExpliesOp"; break;
+ case 110: s = "invalid AndOp"; break;
+ case 111: s = "invalid OrOp"; break;
+ case 112: s = "invalid RelOp"; break;
+ case 113: s = "invalid AddOp"; break;
+ case 114: s = "invalid UnaryExpression"; break;
+ case 115: s = "invalid MulOp"; break;
+ case 116: s = "invalid NegOp"; break;
+ case 117: s = "invalid CoercionExpression"; break;
+ case 118: s = "invalid AtomExpression"; break;
+ case 119: s = "invalid AtomExpression"; break;
+ case 120: s = "invalid AtomExpression"; break;
+ case 121: s = "invalid Forall"; break;
+ case 122: s = "invalid QuantifierBody"; break;
+ case 123: s = "invalid Exists"; break;
+ case 124: s = "invalid Lambda"; break;
+ case 125: s = "invalid SpecBlock"; break;
+ case 126: s = "invalid AttributeOrTrigger"; break;
+ case 127: s = "invalid AttributeParameter"; break;
+ case 128: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Core/ResolutionContext.ssc b/Source/Core/ResolutionContext.ssc index bb1fc7c6..10ff7d87 100644 --- a/Source/Core/ResolutionContext.ssc +++ b/Source/Core/ResolutionContext.ssc @@ -410,26 +410,36 @@ namespace Microsoft.Boogie // ------------------------------ Blocks ------------------------------
- // blocks
- [Microsoft.Contracts.SpecPublic]
- /*maybe null*/ Hashtable /*string->Block*/ blocks;
+ class ProcedureContext {
+ public readonly Hashtable! /*string->Block!*/ Blocks;
+ public readonly ProcedureContext Next;
+ public ProcedureContext(ProcedureContext next) {
+ Blocks = new Hashtable /*string->Block!*/ ();
+ Next = next;
+ }
+ }
+ /*maybe null*/ ProcedureContext procedureContext; // stack of procedure contexts
+ public bool HasProcedureContext {
+ get { return procedureContext != null; }
+ }
/// <summary>
- /// Requires there not to be a procedure context. Creates one.
+ /// Pushes a new procedure context.
/// </summary>
- public void StartProcedureContext()
+ public void PushProcedureContext()
+ ensures HasProcedureContext;
{
- System.Diagnostics.Debug.Assert(blocks == null);
- blocks = new Hashtable /*string->Block*/ ();
+ procedureContext = new ProcedureContext(procedureContext);
}
/// <summary>
- /// Requires there to be a procedure context. Removes it.
+ /// Requires there to be a procedure context. Pops it.
/// </summary>
- public void EndProcedureContext()
+ public void PopProcedureContext()
+ requires HasProcedureContext;
{
- System.Diagnostics.Debug.Assert(blocks != null);
- blocks = null;
+ assert procedureContext != null; // follows from precondition
+ procedureContext = procedureContext.Next;
}
/// <summary>
@@ -437,8 +447,10 @@ namespace Microsoft.Boogie /// </summary>
/// <param name="block"></param>
public void AddBlock(Block! block)
- requires this.blocks != null;
+ requires HasProcedureContext;
{
+ assert procedureContext != null; // follows from precondition
+ Hashtable! /*string->Block!*/ blocks = procedureContext.Blocks;
if (blocks[block.Label] != null)
{
Error(block, "more than one declaration of block name: {0}", block.Label);
@@ -457,8 +469,10 @@ namespace Microsoft.Boogie /// <param name="name"></param>
/// <returns></returns>
public Block LookUpBlock(string! name)
- requires this.blocks != null;
+ requires HasProcedureContext;
{
+ assert procedureContext != null; // follows from precondition
+ Hashtable! /*string->Block!*/ blocks = procedureContext.Blocks;
return (Block)blocks[name];
}
diff --git a/Source/Core/Scanner.ssc b/Source/Core/Scanner.ssc index 97a2dfea..870720d3 100644 --- a/Source/Core/Scanner.ssc +++ b/Source/Core/Scanner.ssc @@ -237,40 +237,40 @@ public class Scanner { for (int i = 126; i <= 126; ++i) start[i] = 2;
for (int i = 48; i <= 57; ++i) start[i] = 9;
for (int i = 34; i <= 34; ++i) start[i] = 6;
- start[92] = 1; - start[59] = 10; - start[40] = 11; - start[41] = 12; - start[58] = 47; - start[44] = 13; - start[91] = 14; - start[93] = 15; - start[60] = 48; - start[62] = 49; - start[123] = 50; - start[125] = 51; - start[61] = 52; - start[42] = 18; - start[8660] = 21; - start[8658] = 23; - start[8656] = 24; - start[38] = 25; - start[8743] = 27; - start[124] = 28; - start[8744] = 30; - start[33] = 53; - start[8800] = 34; - start[8804] = 35; - start[8805] = 36; - start[43] = 54; - start[45] = 38; - start[47] = 39; - start[37] = 40; - start[172] = 41; - start[8704] = 42; - start[8707] = 43; - start[955] = 44; - start[8226] = 46; + start[92] = 1;
+ start[59] = 10;
+ start[40] = 11;
+ start[41] = 12;
+ start[58] = 47;
+ start[44] = 13;
+ start[91] = 14;
+ start[93] = 15;
+ start[60] = 48;
+ start[62] = 49;
+ start[123] = 16;
+ start[125] = 50;
+ start[61] = 51;
+ start[42] = 17;
+ start[8660] = 20;
+ start[8658] = 22;
+ start[8656] = 23;
+ start[38] = 24;
+ start[8743] = 26;
+ start[124] = 52;
+ start[8744] = 28;
+ start[33] = 53;
+ start[8800] = 32;
+ start[8804] = 33;
+ start[8805] = 34;
+ start[43] = 54;
+ start[45] = 36;
+ start[47] = 37;
+ start[37] = 38;
+ start[172] = 39;
+ start[8704] = 42;
+ start[8707] = 43;
+ start[955] = 44;
+ start[8226] = 46;
start[Buffer.EOF] = -1;
}
@@ -351,7 +351,7 @@ public class Scanner { // eol handling uniform across Windows, Unix and Mac
if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;
if (ch == EOL) {
- line++; col = 0; + line++; col = 0;
} else if (ch == '#' && col == 1) {
int prLine = line;
int prColumn = 0;
@@ -480,21 +480,21 @@ public class Scanner { case "free": t.kind = 33; break;
case "requires": t.kind = 34; break;
case "ensures": t.kind = 35; break;
- case "goto": t.kind = 38; break;
- case "return": t.kind = 39; break;
- case "if": t.kind = 40; break;
- case "else": t.kind = 41; break;
- case "while": t.kind = 42; break;
- case "invariant": t.kind = 43; break;
- case "break": t.kind = 45; break;
- case "assert": t.kind = 46; break;
- case "assume": t.kind = 47; break;
- case "havoc": t.kind = 48; break;
- case "call": t.kind = 50; break;
- case "forall": t.kind = 51; break;
- case "false": t.kind = 77; break;
- case "true": t.kind = 78; break;
- case "old": t.kind = 79; break;
+ case "goto": t.kind = 36; break;
+ case "return": t.kind = 37; break;
+ case "if": t.kind = 38; break;
+ case "else": t.kind = 39; break;
+ case "while": t.kind = 40; break;
+ case "invariant": t.kind = 41; break;
+ case "break": t.kind = 43; break;
+ case "assert": t.kind = 44; break;
+ case "assume": t.kind = 45; break;
+ case "havoc": t.kind = 46; break;
+ case "call": t.kind = 48; break;
+ case "forall": t.kind = 49; break;
+ case "false": t.kind = 75; break;
+ case "true": t.kind = 76; break;
+ case "old": t.kind = 77; break;
case "then": t.kind = 80; break;
case "exists": t.kind = 82; break;
case "lambda": t.kind = 84; break;
@@ -510,7 +510,7 @@ public class Scanner { int recKind = noSym;
int recEnd = pos;
t = new Token();
- t.pos = pos; t.col = col; t.line = line; + t.pos = pos; t.col = col; t.line = line;
t.filename = this.Filename;
int state;
if (start.ContainsKey(ch)) { state = (int) (!) start[ch]; }
@@ -572,37 +572,36 @@ public class Scanner { case 15:
{t.kind = 16; break;}
case 16:
- {t.kind = 36; break;}
+ {t.kind = 25; break;}
case 17:
- {t.kind = 37; break;}
+ {t.kind = 42; break;}
case 18:
- {t.kind = 44; break;}
+ {t.kind = 47; break;}
case 19:
- {t.kind = 49; break;}
+ {t.kind = 50; break;}
case 20:
- {t.kind = 52; break;}
+ {t.kind = 51; break;}
case 21:
- {t.kind = 53; break;}
+ {t.kind = 52; break;}
case 22:
- {t.kind = 54; break;}
+ {t.kind = 53; break;}
case 23:
{t.kind = 55; break;}
case 24:
- {t.kind = 57; break;}
- case 25:
- if (ch == '&') {AddCh(); goto case 26;}
+ if (ch == '&') {AddCh(); goto case 25;}
else {goto case 0;}
+ case 25:
+ {t.kind = 56; break;}
case 26:
- {t.kind = 58; break;}
+ {t.kind = 57; break;}
case 27:
- {t.kind = 59; break;}
+ {t.kind = 58; break;}
case 28:
- if (ch == '|') {AddCh(); goto case 29;}
- else {goto case 0;}
+ {t.kind = 59; break;}
case 29:
- {t.kind = 60; break;}
+ {t.kind = 62; break;}
case 30:
- {t.kind = 61; break;}
+ {t.kind = 63; break;}
case 31:
{t.kind = 64; break;}
case 32:
@@ -614,17 +613,17 @@ public class Scanner { case 35:
{t.kind = 68; break;}
case 36:
- {t.kind = 69; break;}
- case 37:
{t.kind = 70; break;}
+ case 37:
+ {t.kind = 71; break;}
case 38:
{t.kind = 72; break;}
case 39:
- {t.kind = 73; break;}
- case 40:
{t.kind = 74; break;}
+ case 40:
+ {t.kind = 78; break;}
case 41:
- {t.kind = 76; break;}
+ {t.kind = 79; break;}
case 42:
{t.kind = 81; break;}
case 43:
@@ -637,50 +636,50 @@ public class Scanner { {t.kind = 87; break;}
case 47:
recEnd = pos; recKind = 10;
- if (ch == '=') {AddCh(); goto case 19;}
+ if (ch == '=') {AddCh(); goto case 18;}
else if (ch == ':') {AddCh(); goto case 45;}
else {t.kind = 10; break;}
case 48:
recEnd = pos; recKind = 17;
if (ch == '=') {AddCh(); goto case 55;}
- else if (ch == ':') {AddCh(); goto case 33;}
+ else if (ch == ':') {AddCh(); goto case 31;}
else {t.kind = 17; break;}
case 49:
recEnd = pos; recKind = 18;
- if (ch == '=') {AddCh(); goto case 31;}
+ if (ch == '=') {AddCh(); goto case 29;}
else {t.kind = 18; break;}
case 50:
- recEnd = pos; recKind = 25;
- if (ch == '{') {AddCh(); goto case 16;}
- else {t.kind = 25; break;}
- case 51:
recEnd = pos; recKind = 26;
- if (ch == '}') {AddCh(); goto case 17;}
+ if (ch == '|') {AddCh(); goto case 41;}
else {t.kind = 26; break;}
- case 52:
+ case 51:
recEnd = pos; recKind = 29;
if (ch == '=') {AddCh(); goto case 56;}
else {t.kind = 29; break;}
+ case 52:
+ if (ch == '|') {AddCh(); goto case 27;}
+ else if (ch == '{') {AddCh(); goto case 40;}
+ else {goto case 0;}
case 53:
- recEnd = pos; recKind = 75;
- if (ch == '=') {AddCh(); goto case 32;}
- else {t.kind = 75; break;}
+ recEnd = pos; recKind = 73;
+ if (ch == '=') {AddCh(); goto case 30;}
+ else {t.kind = 73; break;}
case 54:
- recEnd = pos; recKind = 71;
- if (ch == '+') {AddCh(); goto case 37;}
- else {t.kind = 71; break;}
+ recEnd = pos; recKind = 69;
+ if (ch == '+') {AddCh(); goto case 35;}
+ else {t.kind = 69; break;}
case 55:
- recEnd = pos; recKind = 63;
+ recEnd = pos; recKind = 61;
if (ch == '=') {AddCh(); goto case 57;}
- else {t.kind = 63; break;}
+ else {t.kind = 61; break;}
case 56:
- recEnd = pos; recKind = 62;
- if (ch == '>') {AddCh(); goto case 22;}
- else {t.kind = 62; break;}
+ recEnd = pos; recKind = 60;
+ if (ch == '>') {AddCh(); goto case 21;}
+ else {t.kind = 60; break;}
case 57:
- recEnd = pos; recKind = 56;
- if (ch == '>') {AddCh(); goto case 20;}
- else {t.kind = 56; break;}
+ recEnd = pos; recKind = 54;
+ if (ch == '>') {AddCh(); goto case 19;}
+ else {t.kind = 54; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Core/StandardVisitor.ssc b/Source/Core/StandardVisitor.ssc index be39fb8f..10984ff3 100644 --- a/Source/Core/StandardVisitor.ssc +++ b/Source/Core/StandardVisitor.ssc @@ -58,12 +58,12 @@ namespace Microsoft.Boogie }
public virtual AIVariableExpr! VisitAIVariableExpr(AIVariableExpr! node)
{
- return node; + return node;
}
public virtual Cmd! VisitAssertCmd(AssertCmd! node)
{
node.Expr = this.VisitExpr(node.Expr);
- return node; + return node;
}
public virtual Cmd! VisitAssignCmd(AssignCmd! node)
{
@@ -76,21 +76,21 @@ namespace Microsoft.Boogie public virtual Cmd! VisitAssumeCmd(AssumeCmd! node)
{
node.Expr = this.VisitExpr(node.Expr);
- return node; + return node;
}
public virtual AtomicRE! VisitAtomicRE(AtomicRE! node)
{
node.b = this.VisitBlock(node.b);
- return node; + return node;
}
public virtual Axiom! VisitAxiom(Axiom! node)
{
node.Expr = this.VisitExpr(node.Expr);
- return node; + return node;
}
public virtual Type! VisitBasicType(BasicType! node)
{
- return this.VisitType(node); + return this.VisitType(node);
}
public virtual BvConcatExpr! VisitBvConcatExpr(BvConcatExpr! node)
{
@@ -100,7 +100,7 @@ namespace Microsoft.Boogie }
public virtual Type! VisitBvType(BvType! node)
{
- return this.VisitType(node); + return this.VisitType(node);
}
public virtual Type! VisitBvTypeProxy(BvTypeProxy! node)
{
@@ -113,14 +113,14 @@ namespace Microsoft.Boogie public virtual Block! VisitBlock(Block! node)
{
node.Cmds = this.VisitCmdSeq(node.Cmds);
- node.TransferCmd = this.VisitTransferCmd((!)node.TransferCmd);
- return node; + node.TransferCmd = (TransferCmd)this.Visit((!)node.TransferCmd);
+ return node;
}
- public virtual Expr! VisitBlockExpr(BlockExpr! node)
+ public virtual Expr! VisitCodeExpr(CodeExpr! node)
{
node.LocVars = this.VisitVariableSeq(node.LocVars);
- node.Blocks = this.VisitBlockSeq(node.Blocks);
- return node; + node.Blocks = this.VisitBlockList(node.Blocks);
+ return node;
}
public virtual BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)
{
@@ -138,7 +138,7 @@ namespace Microsoft.Boogie public virtual BoundVariable! VisitBoundVariable(BoundVariable! node)
{
node = (BoundVariable) this.VisitVariable(node);
- return node; + return node;
}
public virtual Cmd! VisitCallCmd(CallCmd! node)
{
@@ -148,7 +148,7 @@ namespace Microsoft.Boogie for (int i = 0; i < node.Outs.Count; ++i)
if (node.Outs[i] != null)
node.Outs[i] = (IdentifierExpr)this.VisitIdentifierExpr((!)node.Outs[i]);
- return node; + return node;
}
public virtual Cmd! VisitCallForallCmd(CallForallCmd! node)
{
@@ -162,7 +162,7 @@ namespace Microsoft.Boogie }
node.Ins = elist;
node.Proc = this.VisitProcedure((!)node.Proc);
- return node; + return node;
}
public virtual CmdSeq! VisitCmdSeq(CmdSeq! cmdSeq)
{
@@ -173,7 +173,7 @@ namespace Microsoft.Boogie public virtual Choice! VisitChoice(Choice! node)
{
node.rs = this.VisitRESeq(node.rs);
- return node; + return node;
}
public virtual Cmd! VisitCommentCmd(CommentCmd! node)
{
@@ -181,7 +181,7 @@ namespace Microsoft.Boogie }
public virtual Constant! VisitConstant(Constant! node)
{
- return node; + return node;
}
public virtual CtorType! VisitCtorType(CtorType! node)
{
@@ -191,29 +191,29 @@ namespace Microsoft.Boogie }
public virtual Declaration! VisitDeclaration(Declaration! node)
{
- return node; + return node;
}
public virtual List<Declaration!>! VisitDeclarationList(List<Declaration!>! declarationList)
{
for (int i = 0, n = declarationList.Count; i < n; i++)
declarationList[i] = (Declaration!) this.Visit(declarationList[i]);
- return declarationList; + return declarationList;
}
public virtual DeclWithFormals! VisitDeclWithFormals(DeclWithFormals! node)
{
node.InParams = this.VisitVariableSeq(node.InParams);
node.OutParams = this.VisitVariableSeq(node.OutParams);
- return node; + return node;
}
public virtual ExistsExpr! VisitExistsExpr(ExistsExpr! node)
{
node = (ExistsExpr) this.VisitQuantifierExpr(node);
- return node; + return node;
}
public virtual BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)
{
node.Bitvector = this.VisitExpr(node.Bitvector);
- return node; + return node;
}
public virtual Expr! VisitExpr(Expr! node)
{
@@ -224,7 +224,7 @@ namespace Microsoft.Boogie {
for (int i = 0, n = exprSeq.Length; i < n; i++)
exprSeq[i] = this.VisitExpr( (!)exprSeq[i]);
- return exprSeq; + return exprSeq;
}
public virtual Requires! VisitRequires(Requires! @requires)
{
@@ -251,50 +251,50 @@ namespace Microsoft.Boogie public virtual ForallExpr! VisitForallExpr(ForallExpr! node)
{
node = (ForallExpr) this.VisitQuantifierExpr(node);
- return node; + return node;
}
public virtual LambdaExpr! VisitLambdaExpr(LambdaExpr! node)
{
node = (LambdaExpr) this.VisitBinderExpr(node);
- return node; + return node;
}
public virtual Formal! VisitFormal(Formal! node)
{
- return node; + return node;
}
public virtual Function! VisitFunction(Function! node)
{
node = (Function) this.VisitDeclWithFormals(node);
if (node.Body != null)
node.Body = this.VisitExpr(node.Body);
- return node; + return node;
}
public virtual GlobalVariable! VisitGlobalVariable(GlobalVariable! node)
{
node = (GlobalVariable) this.VisitVariable(node);
- return node; + return node;
}
public virtual GotoCmd! VisitGotoCmd(GotoCmd! node)
{
- node.labelTargets = this.VisitBlockSeq((!)node.labelTargets);
- return node; + // do not visit the labelTargets, or control-flow loops will lead to a looping visitor
+ return node;
}
public virtual Cmd! VisitHavocCmd(HavocCmd! node)
{
node.Vars = this.VisitIdentifierExprSeq(node.Vars);
- return node; + return node;
}
public virtual Expr! VisitIdentifierExpr(IdentifierExpr! node)
{
if (node.Decl != null)
node.Decl = this.VisitVariable(node.Decl);
- return node; + return node;
}
public virtual IdentifierExprSeq! VisitIdentifierExprSeq(IdentifierExprSeq! identifierExprSeq)
{
for (int i = 0, n = identifierExprSeq.Length; i < n; i++)
identifierExprSeq[i] = (IdentifierExpr) this.VisitIdentifierExpr( (!)identifierExprSeq[i]);
- return identifierExprSeq; + return identifierExprSeq;
}
public virtual Implementation! VisitImplementation(Implementation! node)
{
@@ -302,16 +302,16 @@ namespace Microsoft.Boogie node.Blocks = this.VisitBlockList(node.Blocks);
node.Proc = this.VisitProcedure((!)node.Proc);
node = (Implementation) this.VisitDeclWithFormals(node); // do this first or last?
- return node; + return node;
}
public virtual LiteralExpr! VisitLiteralExpr(LiteralExpr! node)
{
- return node; + return node;
}
public virtual LocalVariable! VisitLocalVariable(LocalVariable! node)
{
- return node; + return node;
}
public virtual AssignLhs! VisitMapAssignLhs(MapAssignLhs! node)
@@ -319,7 +319,7 @@ namespace Microsoft.Boogie node.Map = (AssignLhs!)this.Visit(node.Map);
for (int i = 0; i < node.Indexes.Count; ++i)
node.Indexes[i] = (Expr!)this.Visit(node.Indexes[i]);
- return node; + return node;
}
public virtual MapType! VisitMapType(MapType! node)
{
@@ -345,12 +345,12 @@ namespace Microsoft.Boogie public virtual Expr! VisitNAryExpr(NAryExpr! node)
{
node.Args = this.VisitExprSeq(node.Args);
- return node; + return node;
}
public virtual Expr! VisitOldExpr(OldExpr! node)
{
node.Expr = this.VisitExpr(node.Expr);
- return node; + return node;
}
public virtual Procedure! VisitProcedure(Procedure! node)
{
@@ -359,19 +359,19 @@ namespace Microsoft.Boogie node.Modifies = this.VisitIdentifierExprSeq(node.Modifies);
node.OutParams = this.VisitVariableSeq(node.OutParams);
node.Requires = this.VisitRequiresSeq(node.Requires);
- return node; + return node;
}
public virtual Program! VisitProgram(Program! node)
{
node.TopLevelDeclarations = this.VisitDeclarationList(node.TopLevelDeclarations);
- return node; + return node;
}
public virtual BinderExpr! VisitBinderExpr(BinderExpr! node)
{
node.Body = this.VisitExpr(node.Body);
node.Dummies = this.VisitVariableSeq(node.Dummies);
//node.Type = this.VisitType(node.Type);
- return node; + return node;
}
public virtual QuantifierExpr! VisitQuantifierExpr(QuantifierExpr! node)
{
@@ -379,7 +379,7 @@ namespace Microsoft.Boogie if (node.Triggers != null) {
node.Triggers = this.VisitTrigger(node.Triggers);
}
- return node; + return node;
}
public virtual Cmd! VisitRE(RE! node)
{
@@ -389,11 +389,11 @@ namespace Microsoft.Boogie {
for (int i = 0, n = reSeq.Length; i < n; i++)
reSeq[i] = (RE) this.VisitRE( (!)reSeq[i]);
- return reSeq; + return reSeq;
}
public virtual ReturnCmd! VisitReturnCmd(ReturnCmd! node)
{
- return (ReturnCmd) this.VisitTransferCmd(node); + return (ReturnCmd) this.VisitTransferCmd(node);
}
public virtual ReturnExprCmd! VisitReturnExprCmd(ReturnExprCmd! node)
{
@@ -404,23 +404,23 @@ namespace Microsoft.Boogie {
node.first = (RE) this.VisitRE(node.first);
node.second = (RE) this.VisitRE(node.second);
- return node; + return node;
}
public virtual AssignLhs! VisitSimpleAssignLhs(SimpleAssignLhs! node)
{
node.AssignedVariable =
(IdentifierExpr) this.VisitIdentifierExpr(node.AssignedVariable);
- return node; + return node;
}
public virtual Cmd! VisitStateCmd(StateCmd! node)
{
node.Locals = this.VisitVariableSeq(node.Locals);
node.Cmds = this.VisitCmdSeq(node.Cmds);
- return node; + return node;
}
public virtual TransferCmd! VisitTransferCmd(TransferCmd! node)
{
- return node; + return node;
}
public virtual Trigger! VisitTrigger(Trigger! node)
{
@@ -433,17 +433,17 @@ namespace Microsoft.Boogie }
}
node.Tr = this.VisitExprSeq(node.Tr);
- return node; + return node;
}
// called by default for all nullary type constructors and type variables
public virtual Type! VisitType(Type! node)
{
- return node; + return node;
}
public virtual TypedIdent! VisitTypedIdent(TypedIdent! node)
{
node.Type = (Type)this.Visit(node.Type);
- return node; + return node;
}
public virtual Declaration! VisitTypeCtorDecl(TypeCtorDecl! node)
{
@@ -462,7 +462,7 @@ namespace Microsoft.Boogie }
public virtual Type! VisitTypeVariable(TypeVariable! node)
{
- return this.VisitType(node); + return this.VisitType(node);
}
public virtual Type! VisitTypeProxy(TypeProxy! node)
{
@@ -474,30 +474,30 @@ namespace Microsoft.Boogie }
public virtual Type! VisitUnresolvedTypeIdentifier(UnresolvedTypeIdentifier! node)
{
- return this.VisitType(node); + return this.VisitType(node);
}
public virtual Variable! VisitVariable(Variable! node)
{
node.TypedIdent = this.VisitTypedIdent(node.TypedIdent);
- return node; + return node;
}
public virtual VariableSeq! VisitVariableSeq(VariableSeq! variableSeq)
{
for (int i = 0, n = variableSeq.Length; i < n; i++)
variableSeq[i] = this.VisitVariable( (!)variableSeq[i]);
- return variableSeq; + return variableSeq;
}
public virtual Cmd! VisitAssertEnsuresCmd(AssertEnsuresCmd! node)
{
node.Ensures = this.VisitEnsures(node.Ensures);
node.Expr = this.VisitExpr(node.Expr);
- return node; + return node;
}
public virtual Cmd! VisitAssertRequiresCmd(AssertRequiresCmd! node)
{
node.Requires = this.VisitRequires(node.Requires);
node.Expr = this.VisitExpr(node.Expr);
- return node; + return node;
}
}
}
diff --git a/Source/Dafny.sln b/Source/Dafny.sln index e900840a..e3bc28cd 100644 --- a/Source/Dafny.sln +++ b/Source/Dafny.sln @@ -27,6 +27,7 @@ Global {63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU
{63400D1F-05B2-453E-9592-1EAB74B2C9CC}.Release|Mixed Platforms.Build.0 = Release|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.ActiveCfg = Debug|Any CPU
+ {FE44674A-1633-4917-99F4-57635E6FA740}.Debug|.NET.Build.0 = Debug|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Any CPU.Build.0 = Debug|Any CPU
{FE44674A-1633-4917-99F4-57635E6FA740}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU
diff --git a/Source/Provers/Isabelle/Prover.cs b/Source/Provers/Isabelle/Prover.cs index 5fb9404d..dedfbc09 100644 --- a/Source/Provers/Isabelle/Prover.cs +++ b/Source/Provers/Isabelle/Prover.cs @@ -961,6 +961,31 @@ namespace Microsoft.Boogie.Isabelle { return Write(b2i, B2I.Kind.IfThenElse, node);
}
+ public bool VisitCustomOp(VCExprNAry node, B2I b2i) {
+ Contract.Requires(node != null);
+ Contract.Requires(b2i != null);
+ VCExprCustomOp op = (VCExprCustomOp)node.Op;
+
+ Contract.Assert(op.Arity == node.Length);
+ b2i.Write(B2I.Kind.Function, op.Name + " " + node.Length);
+ if (b2i.Context.AllTypes) {
+ b2i.Indent(2);
+
+ // pick the types from the actual arguments
+ foreach (VCExpr arg in node) {
+ Contract.Assert(arg != null);
+ b2i.Write(arg.Type);
+ }
+ b2i.Unindent();
+ }
+ if (b2i.Context.AllTypes) {
+ b2i.Indent(2);
+ b2i.Write(op.Type);
+ b2i.Unindent();
+ }
+ WriteArguments(b2i, node);
+ return true;
+ }
public bool VisitHeapSuccessionOp(VCExprNAry node, B2I b2i) {
Contract.Requires(node != null);
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 376e93df..73ae55a9 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -642,6 +642,15 @@ void ObjectInvariant() return true;
}
+ public bool VisitCustomOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(node != null);
+ Contract.Requires(options != null);
+
+ VCExprCustomOp op = (VCExprCustomOp)node.Op;
+ WriteApplicationTermOnly(op.Name, node, options);
+ return true;
+ }
+
public bool VisitDistinctOp (VCExprNAry node, LineariserOptions options) {
Contract.Requires(node != null);
Contract.Requires(options != null);
diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc index 4e848c82..df966c2d 100644 --- a/Source/VCExpr/Boogie2VCExpr.ssc +++ b/Source/VCExpr/Boogie2VCExpr.ssc @@ -40,6 +40,8 @@ namespace Microsoft.Boogie.VCExprAST }
}
+ public delegate VCExpr! CodeExprConverter(CodeExpr! codeExpr, Hashtable/*<Block, VCExprVar!>*/! blockVariables, List<VCExprLetBinding!>! bindings);
+
public class Boogie2VCExprTranslator : StandardVisitor, ICloneable {
// Stack on which the various Visit-methods put the result of the translation
private readonly Stack<VCExpr!>! SubExpressions = new Stack<VCExpr!> ();
@@ -477,9 +479,19 @@ namespace Microsoft.Boogie.VCExprAST {
assert false;
}
- public override Expr! VisitBlockExpr(BlockExpr! node)
+ CodeExprConverter codeExprConverter = null;
+ public void SetCodeExprConverter(CodeExprConverter f){
+ this.codeExprConverter = f;
+ }
+ public override Expr! VisitCodeExpr(CodeExpr! codeExpr)
{
- assert false;
+ assume codeExprConverter != null;
+
+ Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
+ List<VCExprLetBinding!> bindings = new List<VCExprLetBinding!>();
+ VCExpr e = codeExprConverter(codeExpr, blockVariables, bindings);
+ Push(e);
+ return codeExpr;
}
public override BlockSeq! VisitBlockSeq(BlockSeq! blockSeq)
{
diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc index 52c51c3e..30779f22 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.ssc +++ b/Source/VCExpr/SimplifyLikeLineariser.ssc @@ -262,7 +262,7 @@ namespace Microsoft.Boogie.VCExprAST internal const string! eqName = "EQ"; // equality
internal const string! neqName = "NEQ"; // inequality
internal const string! lessName = "<";
- internal const string! greaterName = ">"; + internal const string! greaterName = ">";
internal const string! atmostName = "<=";
internal const string! atleastName = ">=";
internal const string! TRUEName = "TRUE"; // nullary predicate that is always true
@@ -377,7 +377,7 @@ namespace Microsoft.Boogie.VCExprAST } else {
wr.Write("({0} ", eqName);
WriteId(printedName);
- wr.Write(" {0})", boolTrueName); + wr.Write(" {0})", boolTrueName);
}
return true;
@@ -663,7 +663,7 @@ namespace Microsoft.Boogie.VCExprAST ExprLineariser.Linearise(node[0], options);
wr.Write("))");
} else {
- WriteApplication(impliesName, node, options); + WriteApplication(impliesName, node, options);
}
return true;
}
@@ -740,6 +740,17 @@ namespace Microsoft.Boogie.VCExprAST return true;
}
+ public bool VisitCustomOp (VCExprNAry! node, LineariserOptions! options) {
+ VCExprCustomOp op = (VCExprCustomOp)node.Op;
+ wr.Write("({0}", op.Name);
+ foreach (VCExpr arg in node) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(arg, options);
+ }
+ wr.Write(")");
+ return true;
+ }
+
public bool VisitAddOp (VCExprNAry! node, LineariserOptions! options) {
if (CommandLineOptions.Clo.ReflectAdd) {
WriteTermApplication(intAddNameReflect, node, options);
diff --git a/Source/VCExpr/TypeErasure.ssc b/Source/VCExpr/TypeErasure.ssc index 8ea6ff81..e0852071 100644 --- a/Source/VCExpr/TypeErasure.ssc +++ b/Source/VCExpr/TypeErasure.ssc @@ -131,7 +131,7 @@ namespace Microsoft.Boogie.TypeErasure List<VCExprVar!>! res = new List<VCExprVar!> (types.Count);
for (int i = 0; i < types.Count; ++i)
res.Add(gen.Variable(baseName + i, types[i]));
- return res; + return res;
}
}
@@ -318,7 +318,7 @@ namespace Microsoft.Boogie.TypeErasure Typed2UntypedVariables.Add(var, res);
AddVarTypeAxiom(res, var.Type);
}
- return (!)res; + return (!)res;
}
protected abstract void AddVarTypeAxiom(VCExprVar! var, Type! originalType);
@@ -371,7 +371,7 @@ namespace Microsoft.Boogie.TypeErasure CurrentCtorNum = BigNum.ZERO;
TypeCtorReprs = new Dictionary<TypeCtorDecl!, TypeCtorRepr> ();
TypeVariableMapping = new Dictionary<TypeVariable!, VCExprVar!> ();
- Typed2UntypedVariables = new Dictionary<VCExprVar!, VCExprVar!> (); + Typed2UntypedVariables = new Dictionary<VCExprVar!, VCExprVar!> ();
TypeCtorDecl! uDecl = new TypeCtorDecl(Token.NoToken, "U", 0);
UDecl = uDecl;
@@ -847,7 +847,7 @@ namespace Microsoft.Boogie.TypeErasure VCExprVar res;
if (!bindings.VCExprVarBindings.TryGetValue(node, out res))
return AxBuilder.Typed2Untyped(node);
- return (!)res; + return (!)res;
}
////////////////////////////////////////////////////////////////////////////
@@ -863,7 +863,7 @@ namespace Microsoft.Boogie.TypeErasure VariableBindings! bindings) {
List<VCExprVar!>! newBoundVars = new List<VCExprVar!> (oldBoundVars.Count);
foreach (VCExprVar! var in oldBoundVars) {
- Type! newType = AxBuilder.TypeAfterErasure(var.Type); + Type! newType = AxBuilder.TypeAfterErasure(var.Type);
VCExprVar! newVar = Gen.Variable(var.Name, newType);
newBoundVars.Add(newVar);
bindings.VCExprVarBindings.Add(var, newVar);
@@ -899,7 +899,7 @@ namespace Microsoft.Boogie.TypeErasure foreach (VCExprVar! var in node.BoundVars) {
Type! newType =
castVariables.Contains(var) ? AxBuilder.U
- : AxBuilder.TypeAfterErasure(var.Type); + : AxBuilder.TypeAfterErasure(var.Type);
VCExprVar! newVar = Gen.Variable(var.Name, newType);
newBoundVars.Add(newVar);
newBindings.VCExprVarBindings.Add(var, newVar);
@@ -985,7 +985,7 @@ namespace Microsoft.Boogie.TypeErasure forall{int i in (1:node.Arity); node[i].Type.Equals(oldType)})
return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, oldType));
else
- return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U)); + return Gen.Function(node.Op, AxBuilder.CastSeq(newArgs, AxBuilder.U));
}
///////////////////////////////////////////////////////////////////////////
@@ -1027,6 +1027,10 @@ namespace Microsoft.Boogie.TypeErasure newArgs[2] = AxBuilder.Cast(newArgs[2], t);
return Gen.Function(node.Op, newArgs);
}
+ public override VCExpr! VisitCustomOp (VCExprNAry! node, VariableBindings! bindings) {
+ List<VCExpr!>! newArgs = MutateSeq(node, bindings, 0);
+ return Gen.Function(node.Op, newArgs);
+ }
public override VCExpr! VisitAddOp (VCExprNAry! node, VariableBindings! bindings) {
return CastArguments(node, Type.Int, bindings, 0);
}
diff --git a/Source/VCExpr/VCExprAST.ssc b/Source/VCExpr/VCExprAST.ssc index 1a81d4a0..7e5b31f1 100644 --- a/Source/VCExpr/VCExprAST.ssc +++ b/Source/VCExpr/VCExprAST.ssc @@ -240,6 +240,8 @@ namespace Microsoft.Boogie // the type of the compared terms
public static readonly VCExprOp! Subtype3Op = new VCExprNAryOp (3, Type.Bool);
public static readonly VCExprOp! IfThenElseOp = new VCExprIfThenElseOp();
+
+ public static readonly VCExprOp! TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);
public VCExprOp! BoogieFunctionOp(Function! func) {
return new VCExprBoogieFunctionOp(func);
@@ -1036,6 +1038,33 @@ namespace Microsoft.Boogie.VCExprAST return visitor.VisitIfThenElseOp(expr, arg);
}
}
+
+ public class VCExprCustomOp : VCExprOp {
+ public readonly string! Name;
+ int arity;
+ public readonly Type! Type;
+ public VCExprCustomOp(string! name, int arity, Type! type) {
+ this.Name = name;
+ this.arity = arity;
+ this.Type = type;
+ }
+ [Pure][Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ VCExprCustomOp t = that as VCExprCustomOp;
+ if (t == null)
+ return false;
+ return this.Name == t.Name && this.arity == t.arity && this.Type == t.Type;
+ }
+ public override int Arity { get { return arity; } }
+ public override int TypeParamArity { get { return 0; } }
+ public override Type! InferType(List<VCExpr!>! args, List<Type!>! typeArgs) { return Type; }
+ public override Result Accept<Result, Arg>
+ (VCExprNAry! expr, IVCExprOpVisitor<Result, Arg>! visitor, Arg arg) {
+ return visitor.VisitCustomOp(expr, arg);
+ }
+ }
/////////////////////////////////////////////////////////////////////////////////
// Bitvector operators
diff --git a/Source/VCExpr/VCExprASTPrinter.ssc b/Source/VCExpr/VCExprASTPrinter.ssc index ca8ec11a..796a2b4e 100644 --- a/Source/VCExpr/VCExprASTPrinter.ssc +++ b/Source/VCExpr/VCExprASTPrinter.ssc @@ -196,6 +196,10 @@ namespace Microsoft.Boogie.VCExprAST public bool VisitIfThenElseOp(VCExprNAry! node, TextWriter! wr) {
return PrintNAry("if-then-else", node, wr);
}
+ public bool VisitCustomOp(VCExprNAry! node, TextWriter! wr) {
+ VCExprCustomOp op = (VCExprCustomOp)node.Op;
+ return PrintNAry(op.Name, node, wr);
+ }
public bool VisitAddOp (VCExprNAry! node, TextWriter! wr) {
if (CommandLineOptions.Clo.ReflectAdd) {
return PrintNAry("Reflect$Add", node, wr);
diff --git a/Source/VCExpr/VCExprASTVisitors.ssc b/Source/VCExpr/VCExprASTVisitors.ssc index e1885f3a..c9d56962 100644 --- a/Source/VCExpr/VCExprASTVisitors.ssc +++ b/Source/VCExpr/VCExprASTVisitors.ssc @@ -52,6 +52,7 @@ namespace Microsoft.Boogie.VCExprAST Result VisitSubtype3Op (VCExprNAry! node, Arg arg);
Result VisitBoogieFunctionOp (VCExprNAry! node, Arg arg);
Result VisitIfThenElseOp (VCExprNAry! node, Arg arg);
+ Result VisitCustomOp (VCExprNAry! node, Arg arg);
}
//////////////////////////////////////////////////////////////////////////////
@@ -959,6 +960,9 @@ namespace Microsoft.Boogie.VCExprAST public virtual Result VisitIfThenElseOp (VCExprNAry! node, Arg arg) {
return StandardResult(node, arg);
}
+ public virtual Result VisitCustomOp (VCExprNAry! node, Arg arg) {
+ return StandardResult(node, arg);
+ }
public virtual Result VisitAddOp (VCExprNAry! node, Arg arg) {
return StandardResult(node, arg);
}
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index b5f35b1e..dea7a445 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -278,7 +278,7 @@ namespace VC { }
protected readonly List<Checker>/*!>!*/ checkers = new List<Checker>();
- protected Implementation current_impl = null;
+ protected VariableSeq CurrentLocalVariables = null;
// shared across each implementation; created anew for each implementation
protected Hashtable /*Variable -> int*/ variable2SequenceNumber;
@@ -357,20 +357,20 @@ namespace VC { #region Methods for injecting pre- and postconditions
private static void
- ThreadInBlockExpr(Implementation impl,
- Block targetBlock,
- BlockExpr blockExpr,
- bool replaceWithAssert,
- TokenTextWriter debugWriter) {
+ ThreadInCodeExpr(Implementation impl,
+ Block targetBlock,
+ CodeExpr codeExpr,
+ bool replaceWithAssert,
+ TokenTextWriter debugWriter) {
Contract.Requires(impl != null);
- Contract.Requires(blockExpr != null);
+ Contract.Requires(codeExpr != null);
Contract.Requires(targetBlock != null);
- // Go through blockExpr and for all blocks that have a "return e"
+ // Go through codeExpr and for all blocks that have a "return e"
// as their transfer command:
// Replace all "return e" with "assert/assume e"
// Change the transfer command to "goto targetBlock"
- // Then add all of the blocks in blockExpr to the implementation (at the end)
- foreach (Block b in blockExpr.Blocks) {
+ // Then add all of the blocks in codeExpr to the implementation (at the end)
+ foreach (Block b in codeExpr.Blocks) {
Contract.Assert(b != null);
ReturnExprCmd rec = b.TransferCmd as ReturnExprCmd;
if (rec != null) { // otherwise it is a goto command
@@ -391,7 +391,7 @@ namespace VC { impl.Blocks.Add(b);
}
if (debugWriter != null) {
- blockExpr.Emit(debugWriter, 1, false);
+ codeExpr.Emit(debugWriter, 1, false);
}
return;
}
@@ -442,31 +442,10 @@ namespace VC { {
Contract.Assert(req != null);
Expr e = Substituter.Apply(formalProcImplSubst, req.Condition);
- BlockExpr be = e as BlockExpr;
- if (be == null) {
- // This is the normal case, where the precondition is an ordinary expression
- Cmd c = new AssumeCmd(req.tok, e);
- insertionPoint.Cmds.Add(c);
- if (debugWriter != null) {
- c.Emit(debugWriter, 1);
- }
- } else {
- // This is a BlockExpr, so append all of its blocks (changing return expressions
- // to assume statements), make the insertion-point block goto the head block of the
- // BlockExpr, and create a new empty block as the current insertion point.
- // Here goes: First, create the new block, which will become the new insertion
- // point and which will serve as a target for the BlockExpr. Move the goto's from
- // the current insertion point to this new block.
- Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);
- k++;
- // Second, append the BlockExpr blocks to the implementation's blocks
- ThreadInBlockExpr(impl, nextIP, be, false, debugWriter);
- // Third, make the old insertion-point block goto the entry block of the BlockExpr
- Block beEntry = cce.NonNull(be.Blocks[0]);
- insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));
- beEntry.Predecessors.Add(insertionPoint);
- // Fourth, update the insertion point
- insertionPoint = nextIP;
+ Cmd c = new AssumeCmd(req.tok, e);
+ insertionPoint.Cmds.Add(c);
+ if (debugWriter != null) {
+ c.Emit(debugWriter, 1);
}
}
origStartBlock.Predecessors.Add(insertionPoint);
@@ -512,7 +491,7 @@ namespace VC { Contract.Assert(ens != null);
if (!ens.Free) { // skip free ensures clauses
Expr e = Substituter.Apply(formalProcImplSubst, ens.Condition);
- BlockExpr be = ens.Condition as BlockExpr;
+ CodeExpr be = ens.Condition as CodeExpr;
if (be == null) {
// This is the normal case, where the postcondition is an ordinary expression
Ensures ensCopy = (Ensures)cce.NonNull(ens.Clone());
@@ -524,17 +503,17 @@ namespace VC { c.Emit(debugWriter, 1);
}
} else {
- // This is a BlockExpr, so append all of its blocks (changing return expressions
+ // This is a CodeExpr, so append all of its blocks (changing return expressions
// to assert statements), insert a goto to its head block from the current insertion
// point, and create a new empty block as the current insertion point.
// Here goes: First, create the new block, which will become the new insertion
- // point and which will serve as a target for the BlockExpr. Steal the TransferCmd
+ // point and which will serve as a target for the CodeExpr. Steal the TransferCmd
// from insertionPoint, since insertionPoint's TransferCmd will soon be replaced anyhow.
Block nextIP = new Block(new Token(-17, -4), LabelPrefix + k, new CmdSeq(), insertionPoint.TransferCmd);
k++;
- // Second, append the BlockExpr blocks to the implementation's blocks
- ThreadInBlockExpr(impl, nextIP, be, true, debugWriter);
- // Third, make the old insertion-point block goto the entry block of the BlockExpr
+ // Second, append the CodeExpr blocks to the implementation's blocks
+ ThreadInCodeExpr(impl, nextIP, be, true, debugWriter);
+ // Third, make the old insertion-point block goto the entry block of the CodeExpr
Block beEntry = cce.NonNull(be.Blocks[0]);
insertionPoint.TransferCmd = new GotoCmd(Token.NoToken, new StringSeq(beEntry.Label), new BlockSeq(beEntry));
beEntry.Predecessors.Add(insertionPoint);
@@ -691,6 +670,14 @@ namespace VC { return whereClauses;
}
+ protected static void RestoreParamWhereClauses(Implementation impl) {
+ Contract.Requires(impl != null);
+ // We no longer need the where clauses on the out parameters, so we remove them to restore the situation from before VC generation
+ foreach (Formal f in impl.OutParams) {
+ Contract.Assert(f != null);
+ f.TypedIdent.WhereExpr = null;
+ }
+ }
#endregion
@@ -848,7 +835,7 @@ namespace VC { protected Variable CreateIncarnation(Variable x, Absy a) {
Contract.Requires(this.variable2SequenceNumber != null);
- Contract.Requires(this.current_impl != null);
+ Contract.Requires(this.CurrentLocalVariables != null);
Contract.Requires(a is Block || a is AssignCmd || a is HavocCmd);
Contract.Requires(x != null);
@@ -862,8 +849,7 @@ namespace VC { -1;
Variable v = new Incarnation(x, currentIncarnationNumber + 1);
variable2SequenceNumber[x] = currentIncarnationNumber + 1;
- Contract.Assert(current_impl != null); // otherwise, the field current_impl wasn't set
- current_impl.LocVars.Add(v);
+ CurrentLocalVariables.Add(v);
incarnationOriginMap.Add((Incarnation)v, a);
return v;
}
@@ -962,12 +948,7 @@ namespace VC { IdentifierExpr v_prime_exp = new IdentifierExpr(v_prime.tok, v_prime);
#endregion
#region Create the assume command itself
- Expr e = Expr.Binary(Token.NoToken,
- BinaryOperator.Opcode.Eq,
- v_prime_exp,
- pred_incarnation_exp
- );
- AssumeCmd ac = new AssumeCmd(v.tok, e);
+ AssumeCmd ac = new AssumeCmd(v.tok, TypedExprEq(v_prime_exp, pred_incarnation_exp));
pred.Cmds.Add(ac);
#endregion
#endregion
@@ -989,22 +970,46 @@ namespace VC { CmdSeq passiveCmds = new CmdSeq();
foreach (Cmd c in b.Cmds) {
- Contract.Assert(b != null); // walk forward over the commands because the map gets modified in a forward direction
+ Contract.Assert(c != null); // walk forward over the commands because the map gets modified in a forward direction
TurnIntoPassiveCmd(c, incarnationMap, oldFrameSubst, passiveCmds);
}
b.Cmds = passiveCmds;
+ if (b.TransferCmd is ReturnExprCmd) {
+ ReturnExprCmd rec = (ReturnExprCmd)b.TransferCmd.Clone();
+ Substitution incarnationSubst = Substituter.SubstitutionFromHashtable(incarnationMap);
+ rec.Expr = Substituter.ApplyReplacingOldExprs(incarnationSubst, oldFrameSubst, rec.Expr);
+ b.TransferCmd = rec;
+ }
#endregion
}
protected Hashtable /*Variable -> Expr*/ Convert2PassiveCmd(Implementation impl) {
Contract.Requires(impl != null);
+
+ Hashtable r = ConvertBlocks2PassiveCmd(impl.Blocks, impl.Proc.Modifies);
+
+ RestoreParamWhereClauses(impl);
+
+ #region Debug Tracing
+ if (CommandLineOptions.Clo.TraceVerify) {
+ Console.WriteLine("after conversion to passive commands");
+ EmitImpl(impl, true);
+ }
+ #endregion
+
+ return r;
+ }
+
+ protected Hashtable /*Variable -> Expr*/ ConvertBlocks2PassiveCmd(List<Block> blocks, IdentifierExprSeq modifies) {
+ Contract.Requires(blocks != null);
+ Contract.Requires(modifies != null);
#region Convert to Passive Commands
#region Topological sort -- need to process in a linearization of the partial order
Graph<Block> dag = new Graph<Block>();
- dag.AddSource(cce.NonNull(impl.Blocks[0])); // there is always at least one node in the graph
- foreach (Block b in impl.Blocks) {
+ dag.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph
+ foreach (Block b in blocks) {
GotoCmd gtc = b.TransferCmd as GotoCmd;
if (gtc != null) {
Contract.Assume(gtc.labelTargets != null);
@@ -1016,13 +1021,11 @@ namespace VC { }
IEnumerable sortedNodes = dag.TopologicalSort();
Contract.Assert(sortedNodes != null);
- // assume sortedNodes != null;
#endregion
// Create substitution for old expressions
Hashtable/*Variable!->Expr!*/ oldFrameMap = new Hashtable();
- Contract.Assume(impl.Proc != null);
- foreach (IdentifierExpr ie in impl.Proc.Modifies) {
+ foreach (IdentifierExpr ie in modifies) {
Contract.Assert(ie != null);
if (!oldFrameMap.Contains(cce.NonNull(ie.Decl)))
oldFrameMap.Add(ie.Decl, ie);
@@ -1049,21 +1052,8 @@ namespace VC { // Verify that exitBlock is indeed the unique exit block
Contract.Assert(exitBlock != null);
Contract.Assert(exitBlock.TransferCmd is ReturnCmd);
-
- // We no longer need the where clauses on the out parameters, so we remove them to restore the situation from before VC generation
- foreach (Formal f in impl.OutParams) {
- Contract.Assert(f != null);
- f.TypedIdent.WhereExpr = null;
- }
#endregion Convert to Passive Commands
- #region Debug Tracing
- if (CommandLineOptions.Clo.TraceVerify) {
- Console.WriteLine("after conversion to passive commands");
- EmitImpl(impl, true);
- }
- #endregion
-
return (Hashtable)block2Incarnation[exitBlock];
}
@@ -1095,7 +1085,7 @@ namespace VC { }
#endregion
#region x1 := E1, x2 := E2, ... |--> assume x1' = E1[in] & x2' = E2[in], out := in( x |-> x' ) [except as noted below]
- else if (c is AssignCmd) {
+ else if (c is AssignCmd) {
AssignCmd assign = ((AssignCmd)c).AsSimpleAssignCmd; // first remove map assignments
Contract.Assert(assign != null);
#region Substitute all variables in E with the current map
@@ -1143,7 +1133,7 @@ namespace VC { }
#endregion
#region Create an assume command with the new variable
- assumptions.Add(Expr.Eq(x_prime_exp, copies[i]));
+ assumptions.Add(TypedExprEq(x_prime_exp, copies[i]));
#endregion
}
}
@@ -1165,7 +1155,7 @@ namespace VC { }
#endregion
#region havoc w |--> assume whereClauses, out := in( w |-> w' )
- else if (c is HavocCmd) {
+ else if (c is HavocCmd) {
if (this.preHavocIncarnationMap == null) // Save a copy of the incarnation map (at the top of a sequence of havoc statements)
this.preHavocIncarnationMap = (Hashtable)incarnationMap.Clone();
@@ -1196,7 +1186,7 @@ namespace VC { }
}
#endregion
- else if (c is CommentCmd) {
+ else if (c is CommentCmd) {
// comments are just for debugging and don't affect verification
} else if (c is SugaredCmd) {
SugaredCmd sug = (SugaredCmd)c;
@@ -1228,7 +1218,7 @@ namespace VC { }
}
#region There shouldn't be any other types of commands at this point
- else {
+ else {
Debug.Fail("Internal Error: Passive transformation handed a command that is not one of assert,assume,havoc,assign.");
}
#endregion
@@ -1242,6 +1232,15 @@ namespace VC { #endregion
}
+ NAryExpr TypedExprEq(Expr e0, Expr e1) {
+ Contract.Requires(e0 != null);
+ Contract.Requires(e1 != null);
+ NAryExpr e = Expr.Eq(e0, e1);
+ e.Type = Bpl.Type.Bool;
+ e.TypeParameters = SimpleTypeParamInstantiation.EMPTY;
+ return e;
+ }
+
/// <summary>
/// Creates a new block to add to impl.Blocks, where impl is the implementation that contains
/// succ. Caller must do the add to impl.Blocks.
@@ -1295,11 +1294,11 @@ namespace VC { return newBlock;
}
- protected void AddBlocksBetween(Implementation impl) {
- Contract.Requires(impl != null);
+ protected void AddBlocksBetween(List<Block> blocks) {
+ Contract.Requires(blocks != null);
#region Introduce empty blocks between join points and their multi-successor predecessors
List<Block> tweens = new List<Block>();
- foreach (Block b in impl.Blocks) {
+ foreach (Block b in blocks) {
int nPreds = b.Predecessors.Length;
if (nPreds > 1) {
// b is a join point (i.e., it has more than one predecessor)
@@ -1311,9 +1310,9 @@ namespace VC { }
}
}
- impl.Blocks.AddRange(tweens); // must wait until iteration is done before changing the list
+ blocks.AddRange(tweens); // must wait until iteration is done before changing the list
#endregion
}
}
-}
\ No newline at end of file +}
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs index 287d3a27..8ea18f3b 100644 --- a/Source/VCGeneration/VC.cs +++ b/Source/VCGeneration/VC.cs @@ -40,11 +40,8 @@ namespace VC { this.GenerateVCsForLazyInlining(program);
}
if (CommandLineOptions.Clo.StratifiedInlining > 0) {
-
this.GenerateVCsForStratifiedInlining(program);
-
}
- // base();
}
private static AssumeCmd AssertTurnedIntoAssume(AssertCmd assrt) {
@@ -143,7 +140,7 @@ namespace VC { Contract.Assert(v != null);
functionInterfaceVars.Add(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, v.Name, v.TypedIdent.Type), true));
}
- TypedIdent ti = new TypedIdent(Token.NoToken, "", Microsoft.Boogie.Type.Bool);
+ TypedIdent ti = new TypedIdent(Token.NoToken, "", Bpl.Type.Bool);
Contract.Assert(ti != null);
Formal returnVar = new Formal(Token.NoToken, ti, false);
Contract.Assert(returnVar != null);
@@ -650,7 +647,7 @@ namespace VC { System.Console.WriteLine(" --- smoke #{0}, before passify", id);
Emit();
}
- parent.current_impl = impl;
+ parent.CurrentLocalVariables = impl.LocVars;
parent.PassifyImpl(impl, program);
Hashtable label2Absy;
Checker ch = parent.FindCheckerFor(impl, CommandLineOptions.Clo.SmokeTimeout);
@@ -666,7 +663,7 @@ namespace VC { ch.BeginCheck(cce.NonNull(impl.Name + "_smoke" + id++), vc, new ErrorHandler(label2Absy, this.callback));
ch.ProverDone.WaitOne();
ProverInterface.Outcome outcome = ch.ReadOutcome();
- parent.current_impl = null;
+ parent.CurrentLocalVariables = null;
DateTime end = DateTime.Now;
TimeSpan elapsed = end - start;
@@ -1150,7 +1147,7 @@ namespace VC { if (allow_small) {
foreach (Block ch in Exits(b)) {
- Contract.Assert(b != null);
+ Contract.Assert(ch != null);
if (b == split_block && assumized_branches.Contains(ch))
continue;
ComputeBlockSetsHelper(ch, allow_small);
@@ -1541,9 +1538,52 @@ namespace VC { impl.Blocks = blocks;
checker = parent.FindCheckerFor(impl, timeout);
+ Hashtable/*<int, Absy!>*/ label2absy = new Hashtable/*<int, Absy!>*/();
+
+ ProverInterface tp = checker.TheoremProver;
+ ProverContext ctx = tp.Context;
+ Boogie2VCExprTranslator bet = ctx.BoogieExprTranslator;
+ bet.SetCodeExprConverter(
+ new CodeExprConverter(
+ delegate (CodeExpr codeExpr, Hashtable/*<Block, VCExprVar!>*/ blockVariables, List<VCExprLetBinding/*!*/> bindings) {
+ VCGen vcgen = new VCGen(new Program(), null, false);
+ vcgen.variable2SequenceNumber = new Hashtable/*Variable -> int*/();
+ vcgen.incarnationOriginMap = new Dictionary<Incarnation, Absy>();
+ vcgen.CurrentLocalVariables = codeExpr.LocVars;
+ // codeExpr.Blocks.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
+
+ vcgen.ComputePredecessors(codeExpr.Blocks);
+ vcgen.AddBlocksBetween(codeExpr.Blocks);
+ Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = vcgen.ConvertBlocks2PassiveCmd(codeExpr.Blocks, new IdentifierExprSeq());
+ VCExpr startCorrect = VCGen.LetVC(
+ codeExpr.Blocks[0],
+ null,
+ label2absy,
+ blockVariables,
+ bindings,
+ ctx);
+ VCExpr vce = ctx.ExprGen.Let(bindings, startCorrect);
+
+ if (vcgen.CurrentLocalVariables.Length != 0) {
+ Boogie2VCExprTranslator translator = checker.TheoremProver.Context.BoogieExprTranslator;
+ List<VCExprVar> boundVars = new List<VCExprVar>();
+ foreach (Variable v in vcgen.CurrentLocalVariables) {
+ Contract.Assert(v != null);
+ VCExprVar ev = translator.LookupVariable(v);
+ Contract.Assert(ev != null);
+ boundVars.Add(ev);
+ if (v.TypedIdent.Type.Equals(Bpl.Type.Bool)) {
+ // add an antecedent (tickleBool ev) to help the prover find a possible trigger
+ vce = checker.VCExprGen.Implies(checker.VCExprGen.Function(VCExpressionGenerator.TickleBoolOp, ev), vce);
+ }
+ }
+ vce = checker.VCExprGen.Forall(boundVars, new List<VCTrigger>(), vce);
+ }
+ return vce;
+ }
+ ));
- Hashtable/*<int, Absy!>*/ label2absy;
- VCExpr vc = parent.GenerateVC(impl, null, out label2absy, checker);
+ VCExpr vc = parent.GenerateVCAux(impl, null, label2absy, checker);
Contract.Assert(vc != null);
if (CommandLineOptions.Clo.vcVariety == CommandLineOptions.VCVariety.Local) {
@@ -1618,17 +1658,25 @@ namespace VC { #endregion
- protected VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch) {
+ protected VCExpr GenerateVC(Implementation/*!*/ impl, Variable controlFlowVariable, out Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch)
+ {
Contract.Requires(impl != null);
Contract.Requires(ch != null);
Contract.Ensures(Contract.ValueAtReturn(out label2absy) != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ label2absy = new Hashtable/*<int, Absy!>*/();
+ return GenerateVCAux(impl, controlFlowVariable, label2absy, ch);
+ }
+
+ protected VCExpr GenerateVCAux(Implementation/*!*/ impl, Variable controlFlowVariable, Hashtable/*<int, Absy!>*//*!*/ label2absy, Checker/*!*/ ch) {
+ Contract.Requires(impl != null);
+ Contract.Requires(ch != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
TypecheckingContext tc = new TypecheckingContext(null);
impl.Typecheck(tc);
- label2absy = new Hashtable/*<int, Absy!>*/();
VCExpr vc;
switch (CommandLineOptions.Clo.vcVariety) {
case CommandLineOptions.VCVariety.Structured:
@@ -1676,9 +1724,9 @@ namespace VC { public override Outcome VerifyImplementation(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback){
Contract.Requires(impl != null);
- Contract.Requires(program != null);
+ Contract.Requires(program != null);
Contract.Requires(callback != null);
- Contract.EnsuresOnThrow< UnexpectedProverOutputException>(true);
+ Contract.EnsuresOnThrow<UnexpectedProverOutputException>(true);
if (impl.SkipVerification) {
return Outcome.Inconclusive; // not sure about this one
}
@@ -2140,7 +2188,7 @@ namespace VC { }
// Return the VC for the impl (don't pass it to the theorem prover).
- // GetVC is a cheap imitation of VerifyImplementatio, except that the VC is not passed to the theorem prover.
+ // GetVC is a cheap imitation of VerifyImplementation, except that the VC is not passed to the theorem prover.
private void GetVC(Implementation/*!*/ impl, Program/*!*/ program, VerifierCallback/*!*/ callback, out VCExpr/*!*/ vc, out Hashtable/*<int, Absy!>*//*!*/ label2absy, out StratifiedInliningErrorReporter/*!*/ reporter) {
Contract.Requires(impl != null);
Contract.Requires(program != null);
@@ -2914,7 +2962,7 @@ namespace VC { Contract.Requires(program != null);
impl.PruneUnreachableBlocks(); // This is needed for VCVariety.BlockNested, and is otherwise just an optimization
- current_impl = impl;
+ CurrentLocalVariables = impl.LocVars;
variable2SequenceNumber = new Hashtable/*Variable -> int*/();
incarnationOriginMap = new Dictionary<Incarnation, Absy>();
@@ -3124,7 +3172,7 @@ namespace VC { {
Contract.Requires(impl != null);
Contract.Requires(program != null);
- Contract.Ensures(Contract.Result<Hashtable>() != null);
+ Contract.Ensures(Contract.Result<Hashtable>() != null);
Hashtable/*TransferCmd->ReturnCmd*/ gotoCmdOrigins = new Hashtable/*TransferCmd->ReturnCmd*/();
Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
@@ -3157,7 +3205,6 @@ namespace VC { cc.Add(c);
}
}
-
// add cc and the preconditions to new blocks preceding impl.Blocks[0]
InjectPreconditions(impl, cc);
@@ -3192,7 +3239,7 @@ namespace VC { }
#endregion
- AddBlocksBetween(impl);
+ AddBlocksBetween(impl.Blocks);
#region Debug Tracing
if (CommandLineOptions.Clo.TraceVerify)
@@ -3207,6 +3254,7 @@ namespace VC { }
Hashtable exitIncarnationMap = Convert2PassiveCmd(impl);
+
if (implName2LazyInliningInfo != null && implName2LazyInliningInfo.ContainsKey(impl.Name))
{
LazyInliningInfo info = implName2LazyInliningInfo[impl.Name];
@@ -3296,7 +3344,7 @@ namespace VC { Contract.Requires(program != null);
Contract.Requires(implName != null);
Contract.Requires(values != null);
- Contract.Ensures(Contract.Result<Counterexample>() != null);
+ Contract.Ensures(Contract.Result<Counterexample>() != null);
VCExprTranslator vcExprTranslator = cce.NonNull(context.exprTranslator);
Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;
@@ -4280,15 +4328,14 @@ namespace VC { // }
static VCExpr LetVC(Block startBlock,
- Variable controlFlowVariable,
- Hashtable/*<int, Absy!>*/ label2absy,
- ProverContext proverCtxt) {
+ Variable controlFlowVariable,
+ Hashtable/*<int, Absy!>*/ label2absy,
+ ProverContext proverCtxt) {
Contract.Requires(startBlock != null);
Contract.Requires(controlFlowVariable != null);
Contract.Requires(label2absy != null);
Contract.Requires(proverCtxt != null);
-
Contract.Ensures(Contract.Result<VCExpr>() != null);
Hashtable/*<Block, LetVariable!>*/ blockVariables = new Hashtable/*<Block, LetVariable!!>*/();
@@ -4298,11 +4345,11 @@ namespace VC { }
static VCExpr LetVC(Block block,
- Variable controlFlowVariable,
- Hashtable/*<int, Absy!>*/ label2absy,
- Hashtable/*<Block, VCExprVar!>*/ blockVariables,
- List<VCExprLetBinding/*!*/>/*!*/ bindings,
- ProverContext proverCtxt)
+ Variable controlFlowVariable,
+ Hashtable/*<int, Absy!>*/ label2absy,
+ Hashtable/*<Block, VCExprVar!>*/ blockVariables,
+ List<VCExprLetBinding/*!*/>/*!*/ bindings,
+ ProverContext proverCtxt)
{
Contract.Requires(block != null);
Contract.Requires(controlFlowVariable != null);
@@ -4311,7 +4358,7 @@ namespace VC { Contract.Requires(cce.NonNullElements(bindings));
Contract.Requires(proverCtxt != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExpressionGenerator gen = proverCtxt.ExprGen;
Contract.Assert(gen != null);
@@ -4326,7 +4373,12 @@ namespace VC { VCExpr SuccCorrect;
GotoCmd gotocmd = block.TransferCmd as GotoCmd;
if (gotocmd == null) {
- SuccCorrect = VCExpressionGenerator.True;
+ ReturnExprCmd re = block.TransferCmd as ReturnExprCmd;
+ if (re == null) {
+ SuccCorrect = VCExpressionGenerator.True;
+ } else {
+ SuccCorrect = proverCtxt.BoogieExprTranslator.Translate(re.Expr);
+ }
} else {
Contract.Assert( gotocmd.labelTargets != null);
List<VCExpr> SuccCorrectVars = new List<VCExpr>(gotocmd.labelTargets.Length);
@@ -4364,7 +4416,7 @@ namespace VC { Contract.Requires(label2absy != null);
Contract.Requires(blockEquations != null);
Contract.Requires(proverCtxt != null);
- Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExpressionGenerator gen = proverCtxt.ExprGen;
Contract.Assert(gen != null);
@@ -4807,9 +4859,17 @@ namespace VC { Contract.Ensures(Contract.Result<Graph<Block>>() != null);
+ return GraphFromBlocks(impl.Blocks);
+ }
+
+ static Graph<Block> GraphFromBlocks(List<Block> blocks) {
+ Contract.Requires(blocks != null);
+
+ Contract.Ensures(Contract.Result<Graph<Block>>() != null);
+
Graph<Block> g = new Graph<Block>();
- g.AddSource(cce.NonNull(impl.Blocks[0])); // there is always at least one node in the graph
- foreach (Block b in impl.Blocks) {
+ g.AddSource(cce.NonNull(blocks[0])); // there is always at least one node in the graph
+ foreach (Block b in blocks) {
Contract.Assert(b != null);
GotoCmd gtc = b.TransferCmd as GotoCmd;
if (gtc != null) {
diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs index d44547a8..12543cd5 100644 --- a/Source/VCGeneration/VCDoomed.cs +++ b/Source/VCGeneration/VCDoomed.cs @@ -331,7 +331,6 @@ namespace VC { PassifyProgram(impl);
-
#endregion
//EmitImpl(impl,false);
@@ -1284,7 +1283,7 @@ namespace VC { Block exitBlock = GenerateUnifiedExit(impl, gotoCmdOrigins);
Contract.Assert(exitBlock != null);
- AddBlocksBetween(impl);
+ AddBlocksBetween(impl.Blocks);
#region Insert pre- and post-conditions and where clauses as assume and assert statements
{
@@ -1323,9 +1322,8 @@ namespace VC { Contract.Requires(impl != null);
Contract.Ensures(Contract.Result<Hashtable>() != null);
- current_impl = impl;
+ CurrentLocalVariables = impl.LocVars;
Convert2PassiveCmd(impl);
- impl = current_impl;
return new Hashtable();
}
diff --git a/Source/VCGeneration/Wlp.cs b/Source/VCGeneration/Wlp.cs index 64cc5c09..d29223a9 100644 --- a/Source/VCGeneration/Wlp.cs +++ b/Source/VCGeneration/Wlp.cs @@ -15,11 +15,11 @@ namespace VC { public class VCContext
{
[ContractInvariantMethod]
-void ObjectInvariant()
-{
- Contract.Invariant(Label2absy!=null);
+ void ObjectInvariant()
+ {
+ Contract.Invariant(Label2absy!=null);
Contract.Invariant(Ctxt != null);
-}
+ }
[Rep] public readonly Hashtable/*<int, Absy!>*/ Label2absy;
[Rep] public readonly ProverContext Ctxt;
@@ -52,9 +52,9 @@ void ObjectInvariant() public static VCExpr Block(Block b, VCExpr N, VCContext ctxt)
//modifies ctxt.*;
{
- Contract.Requires(b != null);
- Contract.Requires(N != null);
- Contract.Requires(ctxt != null);
+ Contract.Requires(b != null);
+ Contract.Requires(N != null);
+ Contract.Requires(ctxt != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
VCExpressionGenerator gen = ctxt.Ctxt.ExprGen;
diff --git a/Test/alltests.txt b/Test/alltests.txt index 588a5eda..4b12e6fd 100644 --- a/Test/alltests.txt +++ b/Test/alltests.txt @@ -1,4 +1,4 @@ -sanity Use Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test)
+sanity Use Build stability test - makes sure the current build doesn't encounter a runtime error (a smoke test)
test0 Use Name resolution tests
test1 Use Typechecking tests
test2 Use VC generation
@@ -15,15 +15,16 @@ textbook Use Some textbook examples test15 Use Benchmarks for error messages
bitvectors Use Smoke tests for bitvectors
smoke Use Soundness smoke testing
-test16 Use Tests methodology of visible-state semantics and loop unrolling
+test16 Use Tests loop unrolling
+codeexpr Use Tests code expressions
test17 Postponed Tests inference of parameterized contracts
z3api Postponed Test for Z3 Managed .NET API prover
houdini Postponed Test for Houdini decision procedure
dafny0 Use Dafny functionality tests
-dafny1 Use Various Dafny examples
+dafny1 Use Various Dafny examples
havoc0 Use HAVOC-generated bpl files
VSI-Benchmarks Use Solutions to Verified Software Initiative verification challenges
vacid0 Use Dafny attempts to VACID Edition 0 benchmarks
-livevars Use STORM benchmarks for testing correctness of live variable analysis
-lazyinline Use Lazy inlining benchmarks
-stratifiedinline Use Stratified inlining benchmarks
+livevars Use STORM benchmarks for testing correctness of live variable analysis
+lazyinline Use Lazy inlining benchmarks
+stratifiedinline Use Stratified inlining benchmarks
diff --git a/Test/codeexpr/Answer b/Test/codeexpr/Answer new file mode 100644 index 00000000..55709034 --- /dev/null +++ b/Test/codeexpr/Answer @@ -0,0 +1,31 @@ +
+------------------------------ CodeExpr0.bpl ---------------------
+CodeExpr0.bpl(15,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ CodeExpr0.bpl(15,3): anon0
+CodeExpr0.bpl(20,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ CodeExpr0.bpl(20,3): anon0
+CodeExpr0.bpl(52,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ CodeExpr0.bpl(52,3): anon0
+
+Boogie program verifier finished with 3 verified, 3 errors
+
+------------------------------ CodeExpr1.bpl ---------------------
+CodeExpr1.bpl(44,5): Error BP5003: A postcondition might not hold at this return statement.
+CodeExpr1.bpl(40,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ CodeExpr1.bpl(42,3): start
+CodeExpr1.bpl(52,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ CodeExpr1.bpl(49,3): start
+CodeExpr1.bpl(66,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ CodeExpr1.bpl(57,3): start
+
+Boogie program verifier finished with 3 verified, 3 errors
+
+------------------------------ CodeExpr2.bpl ---------------------
+
+Boogie program verifier finished with 6 verified, 0 errors
diff --git a/Test/codeexpr/CodeExpr0.bpl b/Test/codeexpr/CodeExpr0.bpl new file mode 100644 index 00000000..62a4225f --- /dev/null +++ b/Test/codeexpr/CodeExpr0.bpl @@ -0,0 +1,53 @@ +procedure P()
+{
+ assert |{ A: return true; }|;
+}
+
+// ------------
+
+procedure Q()
+{
+ assert |{ var x: bool; A: x := true; return x; }|;
+}
+
+procedure R()
+{
+ assert |{ var x: bool; A: x := false; return x; }|; // error
+}
+
+procedure S()
+{
+ assert |{ var x: bool; A: return x; }|; // error
+}
+
+// ------------
+
+procedure T(x: int, y: int)
+ requires |{ var z: bool;
+ Start: goto A;
+ A: z := false; goto B, C;
+ B: assume 0 <= x; goto D;
+ C: assume x < 0; goto R;
+ D: goto E, F;
+ E: assume 0 <= y; z := true; goto R;
+ F: assume y < 0; goto R;
+ R: return z;
+ }|;
+{
+ assert 0 <= x + y;
+}
+
+procedure U(x: int, y: int)
+ requires |{ var z: bool;
+ Start: goto A;
+ A: z := false; goto B, C;
+ B: assume 0 <= x; goto D;
+ C: assume x < 0; goto R;
+ D: goto E, F;
+ E: assume 0 <= y; z := true; goto R;
+ F: assume y < 0; goto R;
+ R: return z;
+ }|;
+{
+ assert x <= y; // error
+}
diff --git a/Test/codeexpr/CodeExpr1.bpl b/Test/codeexpr/CodeExpr1.bpl new file mode 100644 index 00000000..3cc92333 --- /dev/null +++ b/Test/codeexpr/CodeExpr1.bpl @@ -0,0 +1,67 @@ +// ------ the good ------
+
+procedure F(x: int, y: int) returns (z: bool)
+ requires x < y;
+ ensures z == (x < 3);
+{
+ start:
+ z := |{ var a : bool, b : bool; B: a := x < 3; return a; }|;
+ return;
+}
+
+function r(int): bool;
+
+procedure F'(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: x < 3 + t ==> r(t));
+ assert r(y);
+}
+
+procedure F''(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: |{ var a: bool;
+ Start:
+ a := x < 3 + t;
+ goto X, Y;
+ X: assume a; return r(t);
+ Y: assume !a; return true;
+ }|);
+ assert r(y);
+}
+
+// ------ the bad ------
+
+procedure G(x: int, y: int) returns (z: bool)
+ requires x < y;
+ ensures z == (x < 3);
+{
+ start:
+ z := |{ var a : bool, b : bool; B: a := x < 3; return !a; }|;
+ return; // error: postcondition violation
+}
+
+procedure G'(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: x + 3 < t ==> r(t));
+ assert r(y); // error
+}
+
+procedure G''(x: int, y: int) returns (z: bool)
+{
+ start:
+ assume x < y;
+ assume (forall t: int :: |{ var a: bool;
+ Start:
+ a := x + 3 < t;
+ goto X, Y;
+ X: assume a; return r(t);
+ Y: assume !a; return true;
+ }|);
+ assert r(y); // error
+}
diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl new file mode 100644 index 00000000..61758d5a --- /dev/null +++ b/Test/codeexpr/CodeExpr2.bpl @@ -0,0 +1,50 @@ +type T;
+const zero: T;
+
+function IsProperIndex(i: int, size: int): bool;
+
+procedure P(a: [int]T, n: int)
+ requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+{
+ call Q(a, n);
+}
+
+procedure Q(a: [int]T, n: int)
+ requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+{
+ call P(a, n);
+}
+
+procedure A(a: [int]T, n: int)
+{
+ assert
+ (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
+ ==>
+ (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure B(a: [int]T, n: int)
+{
+ assert
+ (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
+ ==>
+ (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
+
+procedure C(a: [int]T, n: int)
+{
+ Start:
+ assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+ goto Next;
+ Next:
+ assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure D(a: [int]T, n: int)
+{
+ Start:
+ assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+ goto Next;
+ Next:
+ assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
diff --git a/Test/codeexpr/runtest.bat b/Test/codeexpr/runtest.bat new file mode 100644 index 00000000..502081b1 --- /dev/null +++ b/Test/codeexpr/runtest.bat @@ -0,0 +1,10 @@ +@echo off
+
+set BOOGIEDIR=..\..\Binaries
+set BPLEXE=%BOOGIEDIR%\Boogie.exe
+
+for %%f in (CodeExpr0.bpl CodeExpr1.bpl CodeExpr2.bpl) do (
+ echo.
+ echo ------------------------------ %%f ---------------------
+ %BPLEXE% %* %%f
+)
diff --git a/Test/test15/Answer b/Test/test15/Answer index 2054998f..8452acb6 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -19,6 +19,11 @@ $pow2 -> { *8 -> *9
else -> #unspecified
}
+tickleBool -> {
+ *1 -> *0
+ *0 -> *0
+ else -> #unspecified
+}
Ctor -> {
*4 -> *8
*5 -> *9
@@ -50,7 +55,7 @@ False : *1 End of model.
NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.
Execution trace:
- NullInModel.bpl(2,3): anon0
+ NullInModel.bpl(2,3): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -71,6 +76,11 @@ $pow2 -> { *6 -> *7
else -> #unspecified
}
+tickleBool -> {
+ *1 -> *0
+ *0 -> *0
+ else -> #unspecified
+}
Ctor -> {
*4 -> *6
*5 -> *7
@@ -94,7 +104,7 @@ False : *1 End of model.
IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.
Execution trace:
- IntInModel.bpl(2,3): anon0
+ IntInModel.bpl(2,3): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -121,6 +131,11 @@ $pow2 -> { *13 -> *9
else -> #unspecified
}
+tickleBool -> {
+ *1 -> *0
+ *0 -> *0
+ else -> #unspecified
+}
Ctor -> {
*4 -> *13
*5 -> *9
@@ -159,19 +174,19 @@ False : *1 End of model.
ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.
Execution trace:
- ModelTest.bpl(3,5): anon0
+ ModelTest.bpl(3,5): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- InterpretedFunctionTests --------------------
InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterpretedFunctionTests.bpl(2,3): anon0
+ InterpretedFunctionTests.bpl(2,3): anon0
InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterpretedFunctionTests.bpl(8,3): anon0
+ InterpretedFunctionTests.bpl(8,3): anon0
InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterpretedFunctionTests.bpl(14,3): anon0
+ InterpretedFunctionTests.bpl(14,3): anon0
Boogie program verifier finished with 0 verified, 3 errors
|