diff options
author | 2011-05-12 10:10:31 -0700 | |
---|---|---|
committer | 2011-05-12 10:10:31 -0700 | |
commit | 1deb713385b80b6100d9aeae4e108b56ab238df0 (patch) | |
tree | f2b51f27b79f339f531685e2c0560ddf4a4537c3 | |
parent | d608e9c2390fbd5e3e49685d5dd9fdeaeccf8f5a (diff) | |
parent | 746c28cd03e8840e8525352ff2aebcfeb76ca2a1 (diff) |
Merge
-rw-r--r-- | .hgignore | 4 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 264 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 7 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/MetadataTraverser.cs | 2 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/Sink.cs | 24 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 8 | ||||
-rw-r--r-- | BCT/BytecodeTranslator/WholeProgram.cs | 4 | ||||
-rw-r--r-- | BCT/Samples/Generics/GenericsExample.cs | 20 | ||||
-rw-r--r-- | BCT/Samples/Strings/StringsExample.cs | 20 | ||||
-rw-r--r-- | Binaries/DafnyRuntime.cs | 1 | ||||
-rw-r--r-- | Source/Dafny/Compiler.cs | 106 | ||||
-rw-r--r-- | Test/VSComp2010/runtest.bat | 4 | ||||
-rw-r--r-- | Test/VSI-Benchmarks/runtest.bat | 14 | ||||
-rw-r--r-- | Test/dafny1/runtest.bat | 9 | ||||
-rw-r--r-- | Test/vacid0/runtest.bat | 9 |
15 files changed, 273 insertions, 223 deletions
@@ -7,9 +7,11 @@ syntax: regexp ^.*(bin|obj)/([^/]*/)?(Debug|Release|Checked|Debug All|DEBUG ALL)/.*$
^Binaries/BytecodeTranslator$
^BCT/Binaries/.*$
+^Chalice/bin/
Test/([^/]*)/Output
Test/([^/]*)/([^/]*)\.sx
-Test/(dafny0|dafny1|VSI-Benchmarks|vacid0|VSComp2010)/out\.cs
+Test/(dafny0|dafny1|VSI-Benchmarks|vacid0|VSComp2010)/(out\.cs|.*\.dll|.*\.pdb|.*\.exe)
+Test/desktop/
^.*~$
syntax: glob
BCT/TestResults/
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index e4f8d1ff..2ec38e8b 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -424,18 +424,18 @@ namespace BytecodeTranslator /// </summary>
/// <param name="methodCall"></param>
/// <remarks>Stub, This one really needs comments!</remarks>
- public override void Visit(IMethodCall methodCall)
- {
- var resolvedMethod = methodCall.MethodToCall.ResolvedMethod;
+ public override void Visit(IMethodCall methodCall) {
+ var resolvedMethod = Sink.Unspecialize(methodCall.MethodToCall).ResolvedMethod;
+
if (resolvedMethod == Dummy.Method) {
throw new TranslationException(
ExceptionType.UnresolvedMethod,
MemberHelper.GetMethodSignature(methodCall.MethodToCall, NameFormattingOptions.None));
}
-
- #region Translate In Parameters
+ #region Translate In and Out Parameters
var inexpr = new List<Bpl.Expr>();
+ var outvars = new List<Bpl.IdentifierExpr>();
#region Create the 'this' argument for the function call
Bpl.IdentifierExpr thisExpr = null;
@@ -443,8 +443,7 @@ namespace BytecodeTranslator List<IFieldDefinition> args = null;
Bpl.Expr arrayExpr = null;
Bpl.Expr indexExpr = null;
- if (!methodCall.IsStaticCall)
- {
+ if (!methodCall.IsStaticCall) {
this.collectStructFields = true;
this.structFields = new List<IFieldDefinition>();
this.arrayExpr = null;
@@ -456,175 +455,145 @@ namespace BytecodeTranslator indexExpr = this.indexExpr;
var e = this.TranslatedExpressions.Pop();
- if (false && methodCall.MethodToCall.ContainingType.IsValueType)
- {
- // then the "this arg" was actually an AddressOf the struct
- // but we are going to ignore that and just get the identifier
- // that it was the address of
- var nAry = e as Bpl.NAryExpr;
- var nAryArgs = nAry.Args;
- e = nAryArgs[0] as Bpl.IdentifierExpr;
- }
inexpr.Add(e);
- if (e is Bpl.NAryExpr)
- {
+ if (e is Bpl.NAryExpr) {
e = ((Bpl.NAryExpr)e).Args[0];
}
thisExpr = e as Bpl.IdentifierExpr;
locals = new List<Bpl.Variable>();
Bpl.Variable x = thisExpr.Decl;
locals.Add(x);
- for (int i = 0; i < args.Count; i++)
- {
+ for (int i = 0; i < args.Count; i++) {
Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(args[i]));
Bpl.Variable y = this.sink.CreateFreshLocal(args[i].Type);
StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(y), this.sink.Heap.ReadHeap(Bpl.Expr.Ident(x), g, args[i].ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, y.TypedIdent.Type)));
x = y;
locals.Add(y);
}
- //thisExpr = Bpl.Expr.Ident(x);
- //inexpr.Add(thisExpr);
+ }
+ if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {
+ outvars.Add(thisExpr);
}
#endregion
- Dictionary<IParameterDefinition, Bpl.Expr> p2eMap = new Dictionary<IParameterDefinition, Bpl.Expr>();
+ Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr> toBoxed = new Dictionary<Bpl.IdentifierExpr, Bpl.IdentifierExpr>();
+ Dictionary<IParameterDefinition, Bpl.IdentifierExpr> p2eMap = new Dictionary<IParameterDefinition, Bpl.IdentifierExpr>();
IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
penum.MoveNext();
- foreach (IExpression exp in methodCall.Arguments)
- {
- if (penum.Current == null)
- {
- throw new TranslationException("More Arguments than Parameters in functioncall");
+ foreach (IExpression exp in methodCall.Arguments) {
+ if (penum.Current == null) {
+ throw new TranslationException("More arguments than parameters in method call");
}
this.Visit(exp);
Bpl.Expr e = this.TranslatedExpressions.Pop();
-
- p2eMap.Add(penum.Current, e);
- if (!penum.Current.IsOut)
- {
+ if (penum.Current.Type is IGenericTypeParameter)
+ inexpr.Add(sink.Heap.Box(methodCall.Token(), this.sink.CciTypeToBoogie(exp.Type), e));
+ else
inexpr.Add(e);
+ if (penum.Current.IsByReference) {
+ Bpl.IdentifierExpr unboxed = e as Bpl.IdentifierExpr;
+ if (unboxed == null) {
+ throw new TranslationException("Trying to pass a complex expression for an out or ref parameter");
+ }
+ if (penum.Current.Type is IGenericTypeParameter) {
+ Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(sink.CreateFreshLocal(this.sink.Heap.BoxType));
+ toBoxed[unboxed] = boxed;
+ outvars.Add(boxed);
+ }
+ else {
+ outvars.Add(unboxed);
+ }
}
-
penum.MoveNext();
}
#endregion
Bpl.IToken cloc = methodCall.Token();
-
- // meeting a constructor is always something special
- if (false && resolvedMethod.IsConstructor)
- {
- // Todo: do something with the constructor call
- }
- else
- {
- // Todo: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!
-
- #region Translate Out vars
- var outvars = new List<Bpl.IdentifierExpr>();
- if (!methodCall.IsStaticCall && methodCall.MethodToCall.ContainingType.ResolvedType.IsStruct) {
- outvars.Add(thisExpr);
+ if (resolvedMethod.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void) {
+ Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);
+ Bpl.IdentifierExpr unboxed = new Bpl.IdentifierExpr(cloc, v);
+ if (resolvedMethod.Type is IGenericTypeParameter) {
+ Bpl.IdentifierExpr boxed = Bpl.Expr.Ident(this.sink.CreateFreshLocal(this.sink.Heap.BoxType));
+ toBoxed[unboxed] = boxed;
+ outvars.Add(boxed);
}
- foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap)
- {
- if (kvp.Key.IsOut || kvp.Key.IsByReference)
- {
- Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;
- if (iexp == null)
- {
- throw new TranslationException("Trying to pass complex expression as out in functioncall");
- }
- outvars.Add(iexp);
- }
+ else {
+ outvars.Add(unboxed);
}
- #endregion
+ TranslatedExpressions.Push(unboxed);
+ }
+ var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
+ string methodname = proc.Name;
- if (methodCall.Type.ResolvedType.TypeCode != PrimitiveTypeCode.Void)
- {
- Bpl.Variable v = this.sink.CreateFreshLocal(methodCall.Type.ResolvedType);
- outvars.Add(new Bpl.IdentifierExpr(cloc, v));
- TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));
+ Bpl.QKeyValue attrib = null;
+ foreach (var a in resolvedMethod.Attributes) {
+ if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute")) {
+ attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);
}
- var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
- string methodname = proc.Name;
+ }
- Bpl.QKeyValue attrib = null;
- foreach (var a in resolvedMethod.Attributes)
- {
- if (TypeHelper.GetTypeName(a.Type).EndsWith("AsyncAttribute"))
- {
- attrib = new Bpl.QKeyValue(cloc, "async", new List<object>(), null);
- }
+ Bpl.CallCmd call;
+ bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
+ bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
+ if (isEventAdd || isEventRemove) {
+ var mName = resolvedMethod.Name.Value;
+ var eventName = mName.Substring(mName.IndexOf('_') + 1);
+ var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));
+ Contract.Assert(eventDef != Dummy.Event);
+ Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);
+ Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);
+
+ if (methodCall.IsStaticCall) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));
+ inexpr.Insert(0, Bpl.Expr.Ident(local));
+ }
+ else {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));
+ inexpr[0] = Bpl.Expr.Ident(local);
}
- Bpl.CallCmd call;
- bool isEventAdd = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("add_");
- bool isEventRemove = resolvedMethod.IsSpecialName && resolvedMethod.Name.Value.StartsWith("remove_");
- if (isEventAdd || isEventRemove)
- {
- var mName = resolvedMethod.Name.Value;
- var eventName = mName.Substring(mName.IndexOf('_')+1);
- var eventDef = TypeHelper.GetEvent(resolvedMethod.ContainingTypeDefinition, this.sink.host.NameTable.GetNameFor(eventName));
- Contract.Assert(eventDef != Dummy.Event);
- Bpl.Variable eventVar = this.sink.FindOrCreateEventVariable(eventDef);
- Bpl.Variable local = this.sink.CreateFreshLocal(eventDef.Type);
-
- if (methodCall.IsStaticCall)
- {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), Bpl.Expr.Ident(eventVar)));
- inexpr.Insert(0, Bpl.Expr.Ident(local));
- }
- else
- {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(local), this.sink.Heap.ReadHeap(thisExpr, Bpl.Expr.Ident(eventVar), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type)));
- inexpr[0] = Bpl.Expr.Ident(local);
- }
-
- System.Diagnostics.Debug.Assert(outvars.Count == 0);
- outvars.Add(Bpl.Expr.Ident(local));
- string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;
- call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);
- this.StmtTraverser.StmtBuilder.Add(call);
- if (methodCall.IsStaticCall)
- {
- this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
- }
- else
- {
- this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));
- }
+ System.Diagnostics.Debug.Assert(outvars.Count == 0);
+ outvars.Add(Bpl.Expr.Ident(local));
+ string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;
+ call = new Bpl.CallCmd(methodCall.Token(), methodName, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ if (methodCall.IsStaticCall) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local)));
}
- else
- {
- if (attrib != null)
- call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);
- else
- call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
- this.StmtTraverser.StmtBuilder.Add(call);
+ else {
+ this.StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), thisExpr, Bpl.Expr.Ident(eventVar), Bpl.Expr.Ident(local), resolvedMethod.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, local.TypedIdent.Type));
}
+ }
+ else {
+ if (attrib != null)
+ call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars, attrib);
+ else
+ call = new Bpl.CallCmd(cloc, methodname, inexpr, outvars);
+ this.StmtTraverser.StmtBuilder.Add(call);
+ }
- if (!methodCall.IsStaticCall) {
- Debug.Assert(args != null && locals != null);
- int count = args.Count;
- Bpl.Variable x = locals[count];
+ foreach (KeyValuePair<Bpl.IdentifierExpr, Bpl.IdentifierExpr> kv in toBoxed) {
+ this.StmtTraverser.StmtBuilder.Add(TranslationHelper.BuildAssignCmd(kv.Key, this.sink.Heap.Unbox(Bpl.Token.NoToken, kv.Key.Type, kv.Value)));
+ }
+
+ if (!methodCall.IsStaticCall) {
+ Debug.Assert(args != null && locals != null);
+ int count = args.Count;
+ Bpl.Variable x = locals[count];
+ count--;
+ while (0 <= count) {
+ IFieldDefinition currField = args[count];
+ Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));
+ Bpl.Variable y = locals[count];
+ StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, x.TypedIdent.Type));
+ x = y;
count--;
- while (0 <= count)
- {
- IFieldDefinition currField = args[count];
- Bpl.IdentifierExpr g = Bpl.Expr.Ident(this.sink.FindOrCreateFieldVariable(currField));
- Bpl.Variable y = locals[count];
- StmtTraverser.StmtBuilder.Add(this.sink.Heap.WriteHeap(methodCall.Token(), Bpl.Expr.Ident(y), g, Bpl.Expr.Ident(x), currField.ContainingType.ResolvedType.IsStruct ? AccessType.Struct : AccessType.Heap, x.TypedIdent.Type));
- x = y;
- count--;
- }
- if (indexExpr != null) {
- Debug.Assert(arrayExpr != null);
- StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, arrayExpr, indexExpr, Bpl.Expr.Ident(x), AccessType.Array, x.TypedIdent.Type));
- }
}
-
+ if (indexExpr != null) {
+ Debug.Assert(arrayExpr != null);
+ StmtTraverser.StmtBuilder.Add(sink.Heap.WriteHeap(Bpl.Token.NoToken, arrayExpr, indexExpr, Bpl.Expr.Ident(x), AccessType.Array, x.TypedIdent.Type));
+ }
}
-
}
#endregion
@@ -762,7 +731,7 @@ namespace BytecodeTranslator /// </summary>
public override void Visit(ICreateObjectInstance createObjectInstance)
{
- TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance.Type, createObjectInstance);
+ TranslateObjectCreation(createObjectInstance.MethodToCall, createObjectInstance.Arguments, createObjectInstance);
}
public override void Visit(ICreateArray createArrayInstance)
@@ -794,35 +763,32 @@ namespace BytecodeTranslator TranslatedExpressions.Push(Bpl.Expr.Ident(a));
}
- private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, ITypeReference ctorType, IExpression creationAST)
+ private void TranslateObjectCreation(IMethodReference ctor, IEnumerable<IExpression> arguments, IExpression creationAST)
{
+ var resolvedMethod = Sink.Unspecialize(ctor).ResolvedMethod;
Bpl.IToken token = creationAST.Token();
-
+
var a = this.sink.CreateFreshLocal(creationAST.Type);
// First generate an Alloc() call
this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(token, this.sink.AllocationMethodName, new Bpl.ExprSeq(), new Bpl.IdentifierExprSeq(Bpl.Expr.Ident(a))));
// Second, generate the call to the appropriate ctor
- var proc = this.sink.FindOrCreateProcedure(ctor.ResolvedMethod);
+ var proc = this.sink.FindOrCreateProcedure(resolvedMethod);
Bpl.ExprSeq inexpr = new Bpl.ExprSeq();
inexpr.Add(Bpl.Expr.Ident(a));
- IEnumerator<IParameterDefinition> penum = ctor.ResolvedMethod.Parameters.GetEnumerator();
+ IEnumerator<IParameterDefinition> penum = resolvedMethod.Parameters.GetEnumerator();
penum.MoveNext();
- foreach (IExpression exp in arguments)
- {
- if (penum.Current == null)
- {
+ foreach (IExpression exp in arguments) {
+ if (penum.Current == null) {
throw new TranslationException("More Arguments than Parameters in functioncall");
}
this.Visit(exp);
Bpl.Expr e = this.TranslatedExpressions.Pop();
-
- if (!penum.Current.IsOut)
- {
+ if (penum.Current.Type is IGenericTypeParameter)
+ inexpr.Add(sink.Heap.Box(ctor.Token(), this.sink.CciTypeToBoogie(exp.Type), e));
+ else
inexpr.Add(e);
- }
-
penum.MoveNext();
}
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index 812fddb1..6d03ef9f 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -148,6 +148,9 @@ namespace BytecodeTranslator { [RepresentationFor("Real2Box", "function Real2Box(Real): Box;")]
public Bpl.Function Real2Box = null;
+ [RepresentationFor("Box2Box", "function {:inline true} Box2Box(b: Box): Box { b }")]
+ public Bpl.Function Box2Box = null;
+
public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {
Bpl.Function conversion;
if (boogieType == Bpl.Type.Bool)
@@ -160,6 +163,8 @@ namespace BytecodeTranslator { conversion = this.Ref2Box;
else if (boogieType == RealType)
conversion = this.Real2Box;
+ else if (boogieType == BoxType)
+ conversion = this.Box2Box;
else
throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));
@@ -183,6 +188,8 @@ namespace BytecodeTranslator { conversion = this.Box2Ref;
else if (boogieType == RealType)
conversion = this.Box2Real;
+ else if (boogieType == BoxType)
+ conversion = this.Box2Box;
else
throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs index 1fa59767..58bec27f 100644 --- a/BCT/BytecodeTranslator/MetadataTraverser.cs +++ b/BCT/BytecodeTranslator/MetadataTraverser.cs @@ -262,7 +262,7 @@ namespace BytecodeTranslator { #region Create Local Vars For Implementation
List<Bpl.Variable> vars = new List<Bpl.Variable>();
foreach (MethodParameter mparam in formalMap.Values) {
- if (!(mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut))
+ if (!mparam.underlyingParameter.IsByReference)
vars.Add(mparam.outParameterCopy);
}
foreach (Bpl.Variable v in this.sink.LocalVarMap.Values) {
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs index 629e7e54..b8d8334d 100644 --- a/BCT/BytecodeTranslator/Sink.cs +++ b/BCT/BytecodeTranslator/Sink.cs @@ -99,6 +99,9 @@ namespace BytecodeTranslator { return Bpl.Expr.Ident(this.Heap.DefaultStruct);
} else if (bplType == this.Heap.RefType) {
return Bpl.Expr.Ident(this.Heap.NullRef);
+ }
+ else if (bplType == this.Heap.BoxType) {
+ return Bpl.Expr.Ident(this.Heap.DefaultBox);
} else {
throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(type)));
}
@@ -113,9 +116,11 @@ namespace BytecodeTranslator { return heap.RealType;
else if (type.ResolvedType.IsStruct)
return heap.StructType;
- else if (type.IsEnum) {
+ else if (type.IsEnum)
return Bpl.Type.Int; // The underlying type of an enum is always some kind of integer
- } else
+ else if (type is IGenericTypeParameter)
+ return heap.BoxType;
+ else
return heap.RefType;
}
@@ -134,6 +139,14 @@ namespace BytecodeTranslator { return v;
}
+ public Bpl.Variable CreateFreshLocal(Bpl.Type t) {
+ Bpl.IToken loc = Bpl.Token.NoToken; // Helper Variables do not have a location
+ Bpl.LocalVariable v = new Bpl.LocalVariable(loc, new Bpl.TypedIdent(loc, TranslationHelper.GenerateTempVarName(), t));
+ ILocalDefinition dummy = new LocalDefinition(); // Creates a dummy entry for the Dict, since only locals in the dict are translated to boogie
+ localVarMap.Add(dummy, v);
+ return v;
+ }
+
/// <summary>
/// State that gets re-initialized per method
/// </summary>
@@ -335,10 +348,9 @@ namespace BytecodeTranslator { MethodParameter mp;
var formalMap = new Dictionary<IParameterDefinition, MethodParameter>();
foreach (IParameterDefinition formal in method.Parameters) {
-
mp = new MethodParameter(formal, this.CciTypeToBoogie(formal.Type));
if (mp.inParameterCopy != null) in_count++;
- if (mp.outParameterCopy != null && (formal.IsByReference || formal.IsOut))
+ if (mp.outParameterCopy != null && formal.IsByReference)
out_count++;
formalMap.Add(formal, mp);
}
@@ -397,7 +409,7 @@ namespace BytecodeTranslator { invars[i++] = mparam.inParameterCopy;
}
if (mparam.outParameterCopy != null) {
- if (mparam.underlyingParameter.IsByReference || mparam.underlyingParameter.IsOut)
+ if (mparam.underlyingParameter.IsByReference)
outvars[j++] = mparam.outParameterCopy;
}
}
@@ -563,7 +575,7 @@ namespace BytecodeTranslator { this.FindOrCreateProcedure(method);
return this.declaredMethods[method.InternedKey];
}
- private static IMethodReference Unspecialize(IMethodReference method) {
+ public static IMethodReference Unspecialize(IMethodReference method) {
IMethodReference result = method;
var gmir = result as IGenericMethodInstanceReference;
if (gmir != null) {
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 42b1a4d0..54ed1700 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -37,22 +37,18 @@ namespace BytecodeTranslator { public IParameterDefinition underlyingParameter;
public MethodParameter(IParameterDefinition parameterDefinition, Bpl.Type ptype) {
-
this.underlyingParameter = parameterDefinition;
var parameterToken = parameterDefinition.Token();
var typeToken = parameterDefinition.Type.Token();
var parameterName = parameterDefinition.Name.Value;
- if (!parameterDefinition.IsOut) {
- this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);
- }
- if (parameterDefinition.IsByReference || parameterDefinition.IsOut) {
+ this.inParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$in", ptype), true);
+ if (parameterDefinition.IsByReference) {
this.outParameterCopy = new Bpl.Formal(parameterToken, new Bpl.TypedIdent(typeToken, parameterName + "$out", ptype), false);
} else {
this.outParameterCopy = new Bpl.LocalVariable(parameterToken, new Bpl.TypedIdent(typeToken, parameterName, ptype));
}
-
}
public override string ToString() {
diff --git a/BCT/BytecodeTranslator/WholeProgram.cs b/BCT/BytecodeTranslator/WholeProgram.cs index f4cc59af..92154020 100644 --- a/BCT/BytecodeTranslator/WholeProgram.cs +++ b/BCT/BytecodeTranslator/WholeProgram.cs @@ -149,13 +149,11 @@ namespace BytecodeTranslator { Bpl.IToken token = methodCall.Token();
- // TODO: if there is no stmttraverser we are visiting a contract and should use a boogie function instead of procedure!
-
#region Translate Out vars
var outvars = new List<Bpl.IdentifierExpr>();
foreach (KeyValuePair<IParameterDefinition, Bpl.Expr> kvp in p2eMap) {
- if (kvp.Key.IsOut || kvp.Key.IsByReference) {
+ if (kvp.Key.IsByReference) {
Bpl.IdentifierExpr iexp = kvp.Value as Bpl.IdentifierExpr;
if (iexp == null) {
throw new TranslationException("Trying to pass complex expression as out in functioncall");
diff --git a/BCT/Samples/Generics/GenericsExample.cs b/BCT/Samples/Generics/GenericsExample.cs new file mode 100644 index 00000000..c7016ceb --- /dev/null +++ b/BCT/Samples/Generics/GenericsExample.cs @@ -0,0 +1,20 @@ +using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using System.Text;
+
+/* Simple example of generics/dictionary support needed by Poirot */
+class GenericsExample
+{
+ public static void Main()
+ {
+ Dictionary<String, String> dict = new Dictionary<String, String>();
+ dict["foo"] = "bar";
+ Contract.Assert(dict.ContainsKey("foo"));
+ Contract.Assert(dict.ContainsValue("bar"));
+ Contract.Assert(dict["foo"] == "bar");
+ dict.Remove("foo");
+ Contract.Assert(dict["foo"] == "bar"); // should fail
+ }
+}
\ No newline at end of file diff --git a/BCT/Samples/Strings/StringsExample.cs b/BCT/Samples/Strings/StringsExample.cs new file mode 100644 index 00000000..a04fc9a0 --- /dev/null +++ b/BCT/Samples/Strings/StringsExample.cs @@ -0,0 +1,20 @@ +using System;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Linq;
+using System.Text;
+
+/* Example of string functionality needed by Poirot: concatenation and equality */
+class StringsExample
+{
+ public static void Main()
+ {
+ string foo = "delicious";
+ string bar = "cake";
+ Contract.Assert(!foo.Equals(bar));
+ string foo_bar = foo + bar;
+ Contract.Assert(foo_bar.Equals("deliciouscake"));
+ string delish = "delicious";
+ Contract.Assert(foo.Equals(delish));
+ }
+}
\ No newline at end of file diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs index 63cca64a..b10aeac9 100644 --- a/Binaries/DafnyRuntime.cs +++ b/Binaries/DafnyRuntime.cs @@ -122,6 +122,7 @@ namespace Dafny // return the first one
return t;
}
+ return default(T);
}
}
public class Sequence<T>
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs index 62270067..9495d64e 100644 --- a/Source/Dafny/Compiler.cs +++ b/Source/Dafny/Compiler.cs @@ -66,7 +66,7 @@ namespace Microsoft.Dafny { foreach (ModuleDecl m in program.Modules) {
int indent = 0;
if (!m.IsDefaultModule) {
- wr.WriteLine("namespace {0} {{", m.Name);
+ wr.WriteLine("namespace @{0} {{", m.Name);
indent += IndentAmount;
}
foreach (TopLevelDecl d in m.TopLevelDecls) {
@@ -84,7 +84,7 @@ namespace Microsoft.Dafny { } else {
ClassDecl cl = (ClassDecl)d;
Indent(indent);
- wr.Write("public class {0}", cl.Name);
+ wr.Write("public class @{0}", cl.Name);
if (cl.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(cl.TypeArgs));
}
@@ -199,17 +199,17 @@ namespace Microsoft.Dafny { wr.Write(">");
}
wr.Write(" : Base_{0}", dt.Name);
- wr.WriteLine(" {");
if (dt.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
}
+ wr.WriteLine(" {");
int ind = indent + IndentAmount;
int i = 0;
foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
Indent(ind);
- wr.WriteLine("public readonly {0} {1};", TypeName(arg.Type), FormalName(arg, i));
+ wr.WriteLine("public readonly {0} @{1};", TypeName(arg.Type), FormalName(arg, i));
i++;
}
}
@@ -222,7 +222,7 @@ namespace Microsoft.Dafny { foreach (Formal arg in ctor.Formals) {
if (!arg.IsGhost) {
Indent(ind + IndentAmount);
- wr.WriteLine("this.{0} = {0};", FormalName(arg, i));
+ wr.WriteLine("this.@{0} = @{0};", FormalName(arg, i));
i++;
}
}
@@ -232,10 +232,12 @@ namespace Microsoft.Dafny { }
}
- void CompileDatatypeStruct(DatatypeDecl dt, int indent) {Contract.Requires(dt != null);
+ void CompileDatatypeStruct(DatatypeDecl dt, int indent) {
+ Contract.Requires(dt != null);
+
// public struct Dt<T> {
// Base_Dt<T> d;
- // public Base_Dt<T> D {
+ // public Base_Dt<T> _D {
// get { if (d == null) { d = Default; } return d; }
// }
// public Dt(Base_Dt<T> d) { this.d = d; }
@@ -243,9 +245,9 @@ namespace Microsoft.Dafny { // get { return ...; }
// }
// public override bool Equals(object other) {
- // return other is Dt<T> && D.Equals(((Dt<T>)other).D);
+ // return other is Dt<T> && _D.Equals(((Dt<T>)other)._D);
// }
- // public override int GetHashCode() { return D.GetHashCode(); }
+ // public override int GetHashCode() { return _D.GetHashCode(); }
// }
string DtT = dt.Name;
if (dt.TypeArgs.Count != 0) {
@@ -253,27 +255,29 @@ namespace Microsoft.Dafny { }
Indent(indent);
- wr.WriteLine("public struct {0} {{", DtT);
+ wr.WriteLine("public struct @{0} {{", DtT);
int ind = indent + IndentAmount;
Indent(ind);
wr.WriteLine("Base_{0} d;", DtT);
Indent(ind);
- wr.WriteLine("public Base_{0} D {{", DtT);
+ wr.WriteLine("public Base_{0} _D {{", DtT);
Indent(ind + IndentAmount);
wr.WriteLine("get { if (d == null) { d = Default; } return d; }");
Indent(ind); wr.WriteLine("}");
Indent(ind);
- wr.WriteLine("public {0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT);
+ wr.WriteLine("public @{0}(Base_{1} d) {{ this.d = d; }}", dt.Name, DtT);
Indent(ind);
wr.WriteLine("public static Base_{0} Default {{", DtT);
Indent(ind + IndentAmount);
wr.Write("get { return ");
wr.Write("new {0}", DtCtorName(cce.NonNull(dt.DefaultCtor)));
- // todo: type parameters
+ if (dt.TypeArgs.Count != 0) {
+ wr.Write("<{0}>", TypeParameters(dt.TypeArgs));
+ }
wr.Write("(");
string sep = "";
foreach (Formal f in dt.DefaultCtor.Formals) {
@@ -288,11 +292,11 @@ namespace Microsoft.Dafny { Indent(ind); wr.WriteLine("public override bool Equals(object other) {");
Indent(ind + IndentAmount);
- wr.WriteLine("return other is {0} && D.Equals((({0})other).D);", DtT);
+ wr.WriteLine("return other is @{0} && _D.Equals(((@{0})other)._D);", DtT);
Indent(ind); wr.WriteLine("}");
Indent(ind);
- wr.WriteLine("public override int GetHashCode() { return D.GetHashCode(); }");
+ wr.WriteLine("public override int GetHashCode() { return _D.GetHashCode(); }");
Indent(indent);
wr.WriteLine("}");
@@ -306,7 +310,7 @@ namespace Microsoft.Dafny { foreach (Formal arg in formals) {
if (!arg.IsGhost) {
string name = FormalName(arg, i);
- wr.Write("{0}{1}{2} {3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);
+ wr.Write("{0}{1}{2} @{3}", sep, arg.InParam ? "" : "out ", TypeName(arg.Type), name);
sep = ", ";
i++;
}
@@ -314,7 +318,8 @@ namespace Microsoft.Dafny { }
string FormalName(Formal formal, int i) {
- Contract.Requires(formal != null);Contract.Ensures(Contract.Result<string>() != null);
+ Contract.Requires(formal != null);
+ Contract.Ensures(Contract.Result<string>() != null);
return formal.Name.StartsWith("#") ? "a" + i : formal.Name;
}
@@ -333,7 +338,7 @@ namespace Microsoft.Dafny { Field f = (Field)member;
if (!f.IsGhost) {
Indent(indent);
- wr.WriteLine("public {0} {1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type));
+ wr.WriteLine("public {0} @{1} = {2};", TypeName(f.Type), f.Name, DefaultValue(f.Type));
}
} else if (member is Function) {
@@ -344,7 +349,7 @@ namespace Microsoft.Dafny { Error("Function {0} has no body", f.FullName);
} else {
Indent(indent);
- wr.Write("public {0}{1} {2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.Name);
+ wr.Write("public {0}{1} @{2}", f.IsStatic ? "static " : "", TypeName(f.ResultType), f.Name);
if (f.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(f.TypeArgs));
}
@@ -354,8 +359,8 @@ namespace Microsoft.Dafny { if (f.Body is MatchExpr) {
MatchExpr me = (MatchExpr)f.Body;
// Type source = e;
- // if (source.D is Dt_Ctor0) {
- // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // if (source._D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source._D).a0;
// ...
// return Body0;
// } else if (...) {
@@ -397,7 +402,7 @@ namespace Microsoft.Dafny { Method m = (Method)member;
if (!m.IsGhost) {
Indent(indent);
- wr.Write("public {0}void {1}", m.IsStatic ? "static " : "", m.Name);
+ wr.Write("public {0}void @{1}", m.IsStatic ? "static " : "", m.Name);
if (m.TypeArgs.Count != 0) {
wr.Write("<{0}>", TypeParameters(m.TypeArgs));
}
@@ -412,7 +417,7 @@ namespace Microsoft.Dafny { foreach (Formal p in m.Outs) {
if (!p.IsGhost) {
Indent(indent + IndentAmount);
- wr.WriteLine("{0} = {1};", p.Name, DefaultValue(p.Type));
+ wr.WriteLine("@{0} = {1};", p.Name, DefaultValue(p.Type));
}
}
if (m.Body == null) {
@@ -428,7 +433,7 @@ namespace Microsoft.Dafny { wr.WriteLine("public static void Main(string[] args) {");
ClassDecl cl = cce.NonNull(m.EnclosingClass);
Indent(indent + IndentAmount);
- wr.Write("{0} b = new {0}", cl.Name);
+ wr.Write("@{0} b = new @{0}", cl.Name);
if (cl.TypeArgs.Count != 0) {
// instantiate every parameter, it doesn't particularly matter how
wr.Write("<");
@@ -493,7 +498,7 @@ namespace Microsoft.Dafny { return name + "]";
} else if (type is UserDefinedType) {
UserDefinedType udt = (UserDefinedType)type;
- string s = udt.Name;
+ string s = "@" + udt.Name;
if (udt.TypeArgs.Count != 0) {
if (Contract.Exists(udt.TypeArgs, argType =>argType is ObjectType)) {
Error("compilation does not support type 'object' as a type parameter; consider introducing a ghost");
@@ -538,7 +543,7 @@ namespace Microsoft.Dafny { string s = "";
string sep = "";
foreach (TypeParameter tp in targs) {
- s += sep + tp.Name;
+ s += sep + "@" + tp.Name;
sep = ",";
}
return s;
@@ -569,14 +574,14 @@ namespace Microsoft.Dafny { return "null";
} else if (type.IsDatatype) {
UserDefinedType udt = (UserDefinedType)type;
- string s = udt.Name;
+ string s = "@" + udt.Name;
if (udt.TypeArgs.Count != 0) {
s += "<" + TypeNames(udt.TypeArgs) + ">";
}
- return s + ".Default";
+ return string.Format("new {0}({0}.Default)", s);
} else if (type.IsTypeParameter) {
UserDefinedType udt = (UserDefinedType)type;
- return "default(" + udt.Name + ")";
+ return "default(@" + udt.Name + ")";
} else if (type is SetType) {
return DafnySetClass + "<" + TypeName(((SetType)type).Arg) + ">.Empty";
} else if (type is SeqType) {
@@ -667,12 +672,10 @@ namespace Microsoft.Dafny { string nw = "_nw" + tmpVarCount;
tmpVarCount++;
Indent(indent);
- wr.Write("{0} = ", nw);
+ wr.Write("var {0} = ", nw);
TrAssignmentRhs(s.Rhs);
wr.WriteLine(";");
- Indent(indent);
TrCallStmt(tRhs.InitCall, nw, indent);
- wr.WriteLine(";");
Indent(indent);
TrExpr(s.Lhs);
wr.WriteLine(" = {0};", nw);
@@ -709,7 +712,7 @@ namespace Microsoft.Dafny { }
TrStmt(s.Thn, indent);
- if (s.Els != null) {
+ if (s.Els != null && s.Guard != null) {
Indent(indent); wr.WriteLine("else");
TrStmt(s.Els, indent);
}
@@ -749,7 +752,7 @@ namespace Microsoft.Dafny { wr.WriteLine("List<Pair<{0},{1}>> {2} = new List<Pair<{0},{1}>>();", TType, RhsType, pu);
Indent(indent);
- wr.Write("foreach ({0} {1} in (", TType, s.BoundVar.Name);
+ wr.Write("foreach ({0} @{1} in (", TType, s.BoundVar.Name);
TrExpr(s.Collection);
wr.WriteLine(").Elements) {");
@@ -762,7 +765,7 @@ namespace Microsoft.Dafny { TrStmt(p, indent + 2*IndentAmount);
}
Indent(indent + 2*IndentAmount);
- wr.Write("{0}.Add(new Pair<{1},{2}>({3}, ", pu, TType, RhsType, s.BoundVar.Name);
+ wr.Write("{0}.Add(new Pair<{1},{2}>(@{3}, ", pu, TType, RhsType, s.BoundVar.Name);
ExprRhs rhsExpr = s.BodyAssign.Rhs as ExprRhs;
if (rhsExpr != null) {
TrExpr(rhsExpr.Expr);
@@ -783,8 +786,8 @@ namespace Microsoft.Dafny { } else if (stmt is MatchStmt) {
MatchStmt s = (MatchStmt)stmt;
// Type source = e;
- // if (source.D is Dt_Ctor0) {
- // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // if (source._D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source._D).a0;
// ...
// Body0;
// } else if (...) {
@@ -823,13 +826,13 @@ namespace Microsoft.Dafny { Contract.Assert(s.Method != null); // follows from the fact that stmt has been successfully resolved
Indent(indent);
if (receiverReplacement != null) {
- wr.Write(receiverReplacement);
+ wr.Write("@" + receiverReplacement);
} else if (s.Method.IsStatic) {
wr.Write(TypeName(cce.NonNull(s.Receiver.Type)));
} else {
TrParenExpr(s.Receiver);
}
- wr.Write(".{0}(", s.Method.Name);
+ wr.Write(".@{0}(", s.Method.Name);
string sep = "";
for (int i = 0; i < s.Method.Ins.Count; i++) {
@@ -921,8 +924,13 @@ namespace Microsoft.Dafny { void TrVarDecl(VarDecl s, bool alwaysInitialize, int indent) {
Contract.Requires(s != null);
+ if (s.IsGhost) {
+ // only emit non-ghosts (we get here only for local variables introduced implicitly by call statements)
+ return;
+ }
+
Indent(indent);
- wr.Write("{0} {1}", TypeName(s.Type), s.Name);
+ wr.Write("{0} @{1}", TypeName(s.Type), s.Name);
if (s.Rhs != null) {
wr.Write(" = ");
TrAssignmentRhs(s.Rhs);
@@ -943,15 +951,15 @@ namespace Microsoft.Dafny { Contract.Requires(source != null);
Contract.Requires(ctor != null);
Contract.Requires(cce.NonNullElements(arguments));
- // if (source.D is Dt_Ctor0) {
- // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // if (source._D is Dt_Ctor0) {
+ // FormalType f0 = ((Dt_Ctor0)source._D).a0;
// ...
Indent(indent);
wr.Write("{0}if (", caseIndex == 0 ? "" : "} else ");
if (caseIndex == caseCount - 1) {
wr.Write("true");
} else {
- wr.Write("{0}.D is {1}", source, DtCtorName(ctor));
+ wr.Write("{0}._D is {1}", source, DtCtorName(ctor));
}
wr.WriteLine(") {");
@@ -960,9 +968,9 @@ namespace Microsoft.Dafny { Formal arg = ctor.Formals[m];
if (!arg.IsGhost) {
BoundVar bv = arguments[m];
- // FormalType f0 = ((Dt_Ctor0)source.D).a0;
+ // FormalType f0 = ((Dt_Ctor0)source._D).a0;
Indent(indent + IndentAmount);
- wr.WriteLine("{0} {1} = (({2}){3}.D).{4};",
+ wr.WriteLine("{0} @{1} = (({2}){3}._D).@{4};",
TypeName(bv.Type), bv.Name, DtCtorName(ctor), source, FormalName(arg, k));
k++;
}
@@ -1022,7 +1030,7 @@ namespace Microsoft.Dafny { } else if (expr is IdentifierExpr) {
IdentifierExpr e = (IdentifierExpr)expr;
- wr.Write(cce.NonNull(e.Var).Name);
+ wr.Write("@" + e.Var.Name);
} else if (expr is SetDisplayExpr) {
SetDisplayExpr e = (SetDisplayExpr)expr;
@@ -1050,7 +1058,7 @@ namespace Microsoft.Dafny { }
} else {
TrParenExpr(e.Obj);
- wr.Write(".{0}", e.Field.Name);
+ wr.Write(".@{0}", e.Field.Name);
}
} else if (expr is SeqSelectExpr) {
@@ -1103,7 +1111,7 @@ namespace Microsoft.Dafny { } else {
TrParenExpr(e.Receiver);
}
- wr.Write(".{0}", f.Name);
+ wr.Write(".@{0}", f.Name);
wr.Write("(");
string sep = "";
for (int i = 0; i < e.Args.Count; i++) {
@@ -1325,7 +1333,7 @@ namespace Microsoft.Dafny { Contract.Assert(false); throw new cce.UnreachableException(); // unexpected BoundedPool type
}
wr.Write("{0}, ", expr is ForallExpr ? "true" : "false");
- wr.Write("{0} => ", bv.Name);
+ wr.Write("@{0} => ", bv.Name);
}
TrExpr(e.Body);
for (int i = 0; i < n; i++) {
diff --git a/Test/VSComp2010/runtest.bat b/Test/VSComp2010/runtest.bat index e39abe7d..e16eda13 100644 --- a/Test/VSComp2010/runtest.bat +++ b/Test/VSComp2010/runtest.bat @@ -4,7 +4,7 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set BPLEXE=%BOOGIEDIR%\Boogie.exe
-
+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy
Problem3-FindZero.dfy Problem4-Queens.dfy
@@ -12,4 +12,6 @@ for %%f in (Problem1-SumMax.dfy Problem2-Invert.dfy echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% %* %%f
+
+ IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
)
diff --git a/Test/VSI-Benchmarks/runtest.bat b/Test/VSI-Benchmarks/runtest.bat index 0cd898c4..a733a1c0 100644 --- a/Test/VSI-Benchmarks/runtest.bat +++ b/Test/VSI-Benchmarks/runtest.bat @@ -4,12 +4,16 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set BPLEXE=%BOOGIEDIR%\Boogie.exe
+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
-
-
-for %%f in ( b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy
- b8.dfy ) do (
+for %%f in (b1.dfy b2.dfy b3.dfy b4.dfy b5.dfy b6.dfy b7.dfy b8.dfy) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 %* %%f
+
+ REM The following line will just run the verifier
+ IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f
+
+ REM Alternatively, the following lines also produce C# code and compile it
+ IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
+ IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
)
diff --git a/Test/dafny1/runtest.bat b/Test/dafny1/runtest.bat index b6fc7f62..36b93883 100644 --- a/Test/dafny1/runtest.bat +++ b/Test/dafny1/runtest.bat @@ -4,6 +4,7 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set BPLEXE=%BOOGIEDIR%\Boogie.exe
+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
for %%f in (BQueue.bpl) do (
echo.
@@ -25,5 +26,11 @@ for %%f in (Queue.dfy PriorityQueue.dfy ExtensibleArray.dfy UltraFilter.dfy) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 %* %%f
+
+ REM The following line will just run the verifier
+ IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f
+
+ REM Alternatively, the following lines also produce C# code and compile it
+ IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
+ IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
)
diff --git a/Test/vacid0/runtest.bat b/Test/vacid0/runtest.bat index d6af7b71..32c6a984 100644 --- a/Test/vacid0/runtest.bat +++ b/Test/vacid0/runtest.bat @@ -4,9 +4,16 @@ setlocal set BOOGIEDIR=..\..\Binaries
set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set BPLEXE=%BOOGIEDIR%\Boogie.exe
+set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
for %%f in (LazyInitArray.dfy SparseArray.dfy Composite.dfy) do (
echo.
echo -------------------- %%f --------------------
- %DAFNY_EXE% /compile:0 %* %%f
+
+ REM The following line will just run the verifier
+ IF "%COMPILEDAFNY%"=="" %DAFNY_EXE% /compile:0 %* %%f
+
+ REM Alternatively, the following lines also produce C# code and compile it
+ IF NOT "%COMPILEDAFNY%"=="" %DAFNY_EXE% %* %%f
+ IF NOT "%COMPILEDAFNY%"=="" %CSC% /nologo /debug /t:library /out:out.dll /r:System.Numerics.dll out.cs
)
|