summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg2
-rw-r--r--Source/Dafny/DafnyAst.cs17
-rw-r--r--Source/Dafny/Parser.cs2
-rw-r--r--Source/Dafny/Resolver.cs98
-rw-r--r--Source/Dafny/Translator.cs102
-rw-r--r--Source/GPUVerify/CrossThreadInvariantProcessor.cs136
-rw-r--r--Source/GPUVerify/GPUVerifier.cs30
-rw-r--r--Source/GPUVerify/GPUVerify.csproj3
-rw-r--r--Source/GPUVerify/VariableDualiser.cs9
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs2
-rw-r--r--Source/VCGeneration/BlockPredicator.cs46
-rw-r--r--Source/VCGeneration/Check.cs6
12 files changed, 204 insertions, 249 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 4eeedcbf..7c8536a3 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -182,7 +182,7 @@ SubModuleDecl<ModuleDefinition parent, bool isOverallModuleGhost, out ModuleDecl
{ Attribute<ref attrs> }
NoUSIdent<out id>
((
- [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs); .)
+ [ "refines" QualifiedName<out idRefined> ] (. module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false); .)
"{" (. module.BodyStartTok = t; .)
{ (. isGhost = false; .)
[ "ghost" (. isGhost = true; .) ]
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index df6fc2a6..032891ce 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -39,7 +39,7 @@ namespace Microsoft.Dafny {
public class BuiltIns
{
- public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null);
+ public readonly ModuleDefinition SystemModule = new ModuleDefinition(Token.NoToken, "_System", false, false, null, null, true);
Dictionary<int, ClassDecl/*!*/> arrayTypeDecls = new Dictionary<int, ClassDecl>();
public readonly ClassDecl ObjectDecl;
public BuiltIns() {
@@ -840,6 +840,7 @@ namespace Microsoft.Dafny {
public readonly Dictionary<string, TopLevelDecl> TopLevels = new Dictionary<string, TopLevelDecl>();
public readonly Dictionary<string, Tuple<DatatypeCtor, bool>> Ctors = new Dictionary<string, Tuple<DatatypeCtor, bool>>();
+ public readonly Dictionary<string, MemberDecl> StaticMembers = new Dictionary<string, MemberDecl>();
public ModuleDefinition ModuleDef; // Note: this is null if this signature does not correspond to a specific definition (i.e.
// it is abstract). Otherwise, it points to that definition.
public ModuleSignature Refines;
@@ -868,14 +869,14 @@ namespace Microsoft.Dafny {
public int Height; // height in the topological sorting of modules; filled in during resolution
public readonly bool IsGhost;
public readonly bool IsAbstract; // True iff this module represents an abstract interface
-
+ private readonly bool IsBuiltinName; // true if this is something like _System that shouldn't have it's name mangled.
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(cce.NonNullElements(TopLevelDecls));
Contract.Invariant(CallGraph != null);
}
- public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase, Attributes attributes)
+ public ModuleDefinition(IToken tok, string name, bool isGhost, bool isAbstract, List<IToken> refinementBase, Attributes attributes, bool isBuiltinName)
: base(tok, name, attributes) {
Contract.Requires(tok != null);
Contract.Requires(name != null);
@@ -884,6 +885,7 @@ namespace Microsoft.Dafny {
IsAbstract = isAbstract;
RefinementBaseRoot = null;
RefinementBase = null;
+ IsBuiltinName = isBuiltinName;
}
public virtual bool IsDefaultModule {
get {
@@ -894,7 +896,10 @@ namespace Microsoft.Dafny {
new public string CompileName {
get {
if (compileName == null) {
- compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);
+ if (IsBuiltinName)
+ compileName = Name;
+ else
+ compileName = "_" + Height.ToString() + "_" + NonglobalVariable.CompilerizeName(Name);
}
return compileName;
}
@@ -916,7 +921,7 @@ namespace Microsoft.Dafny {
}
public class DefaultModuleDecl : ModuleDefinition {
- public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null) {
+ public DefaultModuleDecl() : base(Token.NoToken, "_module", false, false, null, null, false) {
}
public override bool IsDefaultModule {
get {
@@ -1093,7 +1098,7 @@ namespace Microsoft.Dafny {
Contract.Requires(EnclosingDatatype != null);
Contract.Ensures(Contract.Result<string>() != null);
- return "#" + EnclosingDatatype.FullName + "." + Name;
+ return "#" + EnclosingDatatype.FullCompileName + "." + Name;
}
}
}
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 5f4c1bf4..f82f5e88 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -249,7 +249,7 @@ bool IsAttribute() {
Get();
QualifiedName(out idRefined);
}
- module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs);
+ module = new ModuleDefinition(id, id.val, isOverallModuleGhost, false, idRefined == null ? null : idRefined, attrs, false);
Expect(6);
module.BodyStartTok = t;
while (StartOf(1)) {
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 9ab89223..325745f0 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -97,6 +97,7 @@ namespace Microsoft.Dafny {
readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>/*!*/ datatypeMembers = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, MemberDecl/*!*/>/*!*/>();
readonly Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>/*!*/ datatypeCtors = new Dictionary<DatatypeDecl/*!*/, Dictionary<string/*!*/, DatatypeCtor/*!*/>/*!*/>();
readonly Graph<ModuleDecl/*!*/>/*!*/ dependencies = new Graph<ModuleDecl/*!*/>();
+ ModuleSignature systemNameInfo = null;
public Resolver(Program prog) {
Contract.Requires(prog != null);
builtIns = prog.BuiltIns;
@@ -142,7 +143,7 @@ namespace Microsoft.Dafny {
var refinementTransformer = new RefinementTransformer(this);
IRewriter rewriter = new AutoContractsRewriter();
- var systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);
+ systemNameInfo = RegisterTopLevelDecls(prog.BuiltIns.SystemModule);
foreach (var decl in sortedDecls) {
if (decl is LiteralModuleDecl) {
// The declaration is a literal module, so it has members and such that we need
@@ -171,14 +172,9 @@ namespace Microsoft.Dafny {
}
literalDecl.Signature = RegisterTopLevelDecls(m);
literalDecl.Signature.Refines = refinedSig;
+ var sig = literalDecl.Signature;
// set up environment
- moduleInfo = MergeSignature(literalDecl.Signature, systemNameInfo);
- // resolve
- var datatypeDependencies = new Graph<IndDatatypeDecl>();
- int prevErrorCount = ErrorCount;
- ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
- if (ErrorCount == prevErrorCount)
- ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
+ ResolveModuleDefinition(m, sig);
refinementTransformer.PostResolve(m);
// give rewriter a chance to do processing
@@ -194,16 +190,11 @@ namespace Microsoft.Dafny {
}
} else if (decl is AbstractModuleDecl) {
var abs = (AbstractModuleDecl)decl;
- ModuleSignature p; ModuleDefinition mod;
+ ModuleSignature p;
if (ResolvePath(abs.Root, abs.Path, out p)) {
- abs.Signature = MakeAbstractSignature(p, abs.Name, abs.Height, out mod);
+ abs.Signature = MakeAbstractSignature(p, abs.FullCompileName, abs.Height, prog.Modules);
abs.OriginalSignature = p;
- moduleInfo = MergeSignature(abs.Signature, systemNameInfo);
// resolve
- var datatypeDependencies = new Graph<IndDatatypeDecl>();
- ResolveTopLevelDecls_Signatures(mod.TopLevelDecls, datatypeDependencies);
- ResolveTopLevelDecls_Meat(mod.TopLevelDecls, datatypeDependencies);
- prog.Modules.Add(mod);
} else {
abs.Signature = new ModuleSignature(); // there was an error, give it a valid but empty signature
}
@@ -224,6 +215,16 @@ namespace Microsoft.Dafny {
}
}
+ private void ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) {
+ moduleInfo = MergeSignature(sig, systemNameInfo);
+ // resolve
+ var datatypeDependencies = new Graph<IndDatatypeDecl>();
+ int prevErrorCount = ErrorCount;
+ ResolveTopLevelDecls_Signatures(m.TopLevelDecls, datatypeDependencies);
+ if (ErrorCount == prevErrorCount)
+ ResolveTopLevelDecls_Meat(m.TopLevelDecls, datatypeDependencies);
+ }
+
public class ModuleBindings {
private ModuleBindings parent;
@@ -355,6 +356,10 @@ namespace Microsoft.Dafny {
foreach (var kv in m.Ctors) {
info.Ctors[kv.Key] = kv.Value;
}
+ foreach (var kv in m.StaticMembers) {
+ info.StaticMembers[kv.Key] = kv.Value;
+ }
+
return info;
}
ModuleSignature RegisterTopLevelDecls(ModuleDefinition moduleDef) {
@@ -395,7 +400,13 @@ namespace Microsoft.Dafny {
}
}
cl.HasConstructor = hasConstructor;
-
+ if (cl.IsDefaultClass) {
+ foreach (MemberDecl m in cl.Members) {
+ if (!sig.StaticMembers.ContainsKey(m.Name) && m.IsStatic && (m is Function || m is Method)) {
+ sig.StaticMembers.Add(m.Name, m);
+ }
+ }
+ }
} else {
DatatypeDecl dt = (DatatypeDecl)d;
@@ -453,17 +464,19 @@ namespace Microsoft.Dafny {
return sig;
}
- private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, out ModuleDefinition mod) {
- mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null);
+ private ModuleSignature MakeAbstractSignature(ModuleSignature p, string Name, int Height, List<ModuleDefinition> mods) {
+ var mod = new ModuleDefinition(Token.NoToken, Name+".Abs", true, true, null, null, false);
mod.Height = Height;
foreach (var kv in p.TopLevels) {
- mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod));
+ mod.TopLevelDecls.Add(CloneDeclaration(kv.Value, mod, mods, Name));
}
var sig = RegisterTopLevelDecls(mod);
sig.Refines = p.Refines;
+ mods.Add(mod);
+ ResolveModuleDefinition(mod, sig);
return sig;
}
- TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m) {
+ TopLevelDecl CloneDeclaration(TopLevelDecl d, ModuleDefinition m, List<ModuleDefinition> mods, string Name) {
Contract.Requires(d != null);
Contract.Requires(m != null);
@@ -486,8 +499,9 @@ namespace Microsoft.Dafny {
var dd = (ClassDecl)d;
var tps = dd.TypeArgs.ConvertAll(CloneTypeParam);
var mm = dd.Members.ConvertAll(CloneMember);
- var cl = new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);
- return cl;
+ if (dd is DefaultClassDecl) {
+ return new DefaultClassDecl(m, mm);
+ } else return new ClassDecl(dd.tok, dd.Name, m, tps, mm, null);
} else if (d is ModuleDecl) {
if (d is LiteralModuleDecl) {
return new LiteralModuleDecl(((LiteralModuleDecl)d).ModuleDef, m);
@@ -497,9 +511,17 @@ namespace Microsoft.Dafny {
alias.ModuleReference = a.ModuleReference;
alias.Signature = a.Signature;
return alias;
+ } else if (d is AbstractModuleDecl) {
+ var abs = (AbstractModuleDecl)d;
+ var sig = MakeAbstractSignature(abs.OriginalSignature, Name + "." + abs.Name, abs.Height, mods);
+ var a = new AbstractModuleDecl(abs.Path, abs.tok, m);
+ a.Signature = sig;
+ a.OriginalSignature = abs.OriginalSignature;
+ return a;
+ } else {
+ Contract.Assert(false); // unexpected declaration
+ return null; // to please compiler
}
- Contract.Assert(false); // unexpected declaration
- return null; // to please compiler
} else {
Contract.Assert(false); // unexpected declaration
return null; // to please compiler
@@ -4473,9 +4495,9 @@ namespace Microsoft.Dafny {
// (if two imported types have the same name, an error message is produced here)
// - unambiguous constructor name of a datatype (if two constructors have the same name, an error message is produced here)
// - imported module name
- // - field name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")
- // Note, at present, modules do not give rise to new namespaces, which is something that should
- // be changed in the language when modules are given more attention.
+ // - field, function or method name (with implicit receiver) (if the field is occluded by anything above, one can use an explicit "this.")
+ // - static function or method in the enclosing module.
+
Expression r = null; // resolved version of e
CallRhs call = null;
@@ -4537,18 +4559,20 @@ namespace Microsoft.Dafny {
}
}
- } else if (classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member)) {
+ } else if ((classMembers.TryGetValue(currentClass, out members) && members.TryGetValue(id.val, out member))
+ || moduleInfo.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.
+ {
// ----- field, function, or method
Expression receiver;
if (member.IsStatic) {
- receiver = new StaticReceiverExpr(id, currentClass);
+ receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);
} else {
if (!scope.AllowInstance) {
Error(id, "'this' is not allowed in a 'static' context");
// nevertheless, set "receiver" to a value so we can continue resolution
}
receiver = new ImplicitThisExpr(id);
- receiver.Type = GetThisType(id, currentClass); // resolve here
+ receiver.Type = GetThisType(id, (ClassDecl)member.EnclosingClass); // resolve here
}
r = ResolveSuffix(receiver, e, 0, twoState, allowMethodCall, out call);
@@ -4569,10 +4593,11 @@ namespace Microsoft.Dafny {
return call;
}
- CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature info, bool twoState, bool allowMethodCall) {
+ CallRhs ResolveIdentifierSequenceModuleScope(IdentifierSequence e, int p, ModuleSignature sig, bool twoState, bool allowMethodCall) {
// Look up "id" as follows:
// - unamibugous type/module name (class, datatype, sub-module (including submodules of imports) or arbitrary-type)
// (if two imported types have the same name, an error message is produced here)
+ // - static function or method of sig.
// This is used to look up names that appear after a dot in a sequence identifier. For example, in X.M.*, M should be looked up in X, but
// should not consult the local scope. This distingushes this from the above, in that local scope, imported modules, etc. are ignored.
Contract.Requires(p < e.Tokens.Count);
@@ -4580,8 +4605,9 @@ namespace Microsoft.Dafny {
CallRhs call = null;
TopLevelDecl decl;
+ MemberDecl member;
var id = e.Tokens[p];
- if (info.TopLevels.TryGetValue(id.val, out decl)) {
+ if (sig.TopLevels.TryGetValue(id.val, out decl)) {
if (decl is AmbiguousTopLevelDecl) {
Error(id, "The name {0} ambiguously refers to a something in one of the modules {1}", id.val, ((AmbiguousTopLevelDecl)decl).ModuleNames());
} else if (decl is ClassDecl) {
@@ -4605,6 +4631,14 @@ namespace Microsoft.Dafny {
r = ResolveSuffix(r, e, p + 2, twoState, allowMethodCall, out call);
}
}
+ } else if (sig.StaticMembers.TryGetValue(id.val, out member)) // try static members of the current module too.
+ {
+ // ----- function, or method
+ Expression receiver;
+ Contract.Assert(member.IsStatic);
+ receiver = new StaticReceiverExpr(id, (ClassDecl)member.EnclosingClass);
+ r = ResolveSuffix(receiver, e, p, twoState, allowMethodCall, out call);
+
} else {
Error(id, "unresolved identifier: {0}", id.val);
// resolve arguments, if any
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 2cb54115..f50cae64 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -26,6 +26,7 @@ namespace Microsoft.Dafny {
readonly Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>/*!*/ classes = new Dictionary<TopLevelDecl/*!*/,Bpl.Constant/*!*/>();
readonly Dictionary<Field/*!*/,Bpl.Constant/*!*/>/*!*/ fields = new Dictionary<Field/*!*/,Bpl.Constant/*!*/>();
readonly Dictionary<Field/*!*/, Bpl.Function/*!*/>/*!*/ fieldFunctions = new Dictionary<Field/*!*/, Bpl.Function/*!*/>();
+ readonly Dictionary<string, Bpl.Constant> fieldConstants = new Dictionary<string,Constant>();
Program program;
[ContractInvariantMethod]
@@ -53,6 +54,7 @@ namespace Microsoft.Dafny {
public readonly Bpl.Type HeapType;
public readonly string HeapVarName;
public readonly Bpl.Type ClassNameType;
+ public readonly Bpl.Type NameFamilyType;
public readonly Bpl.Type DatatypeType;
public readonly Bpl.Type DtCtorId;
public readonly Bpl.Expr Null;
@@ -71,6 +73,7 @@ namespace Microsoft.Dafny {
Contract.Invariant(HeapType != null);
Contract.Invariant(HeapVarName != null);
Contract.Invariant(ClassNameType != null);
+ Contract.Invariant(NameFamilyType != null);
Contract.Invariant(DatatypeType != null);
Contract.Invariant(DtCtorId != null);
Contract.Invariant(Null != null);
@@ -126,7 +129,7 @@ namespace Microsoft.Dafny {
public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType,
Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType,
- Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType,
+ Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl nameFamilyType,
Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl dtCtorId,
Bpl.Constant allocField, Bpl.Constant classDotArray) {
#region Non-null preconditions on parameters
@@ -158,6 +161,7 @@ namespace Microsoft.Dafny {
this.HeapType = heap.TypedIdent.Type;
this.HeapVarName = heap.Name;
this.ClassNameType = new Bpl.CtorType(Token.NoToken, classNameType, new Bpl.TypeSeq());
+ this.NameFamilyType = new Bpl.CtorType(Token.NoToken, nameFamilyType, new Bpl.TypeSeq());
this.DatatypeType = new Bpl.CtorType(Token.NoToken, datatypeType, new Bpl.TypeSeq());
this.DtCtorId = new Bpl.CtorType(Token.NoToken, dtCtorId, new Bpl.TypeSeq());
this.allocField = allocField;
@@ -180,6 +184,7 @@ namespace Microsoft.Dafny {
Bpl.TypeCtorDecl seqTypeCtor = null;
Bpl.TypeCtorDecl fieldNameType = null;
Bpl.TypeCtorDecl classNameType = null;
+ Bpl.TypeCtorDecl nameFamilyType = null;
Bpl.TypeCtorDecl datatypeType = null;
Bpl.TypeCtorDecl dtCtorId = null;
Bpl.TypeCtorDecl boxType = null;
@@ -203,6 +208,8 @@ namespace Microsoft.Dafny {
dtCtorId = dt;
} else if (dt.Name == "ref") {
refType = dt;
+ } else if (dt.Name == "NameFamily") {
+ nameFamilyType = dt;
} else if (dt.Name == "BoxType") {
boxType = dt;
} else if (dt.Name == "TickType") {
@@ -250,6 +257,8 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of type Field");
} else if (classNameType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type ClassName");
+ } else if (nameFamilyType == null) {
+ Console.WriteLine("Error: Dafny prelude is missing declaration of type NameFamily");
} else if (datatypeType == null) {
Console.WriteLine("Error: Dafny prelude is missing declaration of type DatatypeType");
} else if (dtCtorId == null) {
@@ -268,7 +277,7 @@ namespace Microsoft.Dafny {
Console.WriteLine("Error: Dafny prelude is missing declaration of class._System.array");
} else {
return new PredefinedDecls(refType, boxType, tickType,
- setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, datatypeType, dtCtorId,
+ setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, heap, classNameType, nameFamilyType, datatypeType, dtCtorId,
allocField, classDotArray);
}
return null;
@@ -310,8 +319,9 @@ namespace Microsoft.Dafny {
public Bpl.Program Translate(Program p) {
Contract.Requires(p != null);
Contract.Ensures(Contract.Result<Bpl.Program>() != null);
+
program = p;
-
+
if (sink == null || predef == null) {
// something went wrong during construction, which reads the prelude; an error has
// already been printed, so just return an empty program here (which is non-null)
@@ -333,15 +343,18 @@ namespace Microsoft.Dafny {
// nothing to do--this is treated just like a type parameter
} else if (d is DatatypeDecl) {
AddDatatype((DatatypeDecl)d);
+ } else if (d is ModuleDecl) {
+ // submodules have already been added as a top level module, ignore this.
} else if (d is ClassDecl) {
AddClassMembers((ClassDecl)d);
- } else if (d is ModuleDecl) {
- // nop, sub-modules are handled in their own iteration.
} else {
Contract.Assert(false);
}
}
}
+ foreach(var c in fieldConstants.Values) {
+ sink.TopLevelDeclarations.Add(c);
+ }
return sink;
}
@@ -396,7 +409,7 @@ namespace Microsoft.Dafny {
if (bvs.Length != 0) {
q = new Bpl.ExistsExpr(ctor.tok, bvs, q);
}
- q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, dId), q);
+ q = Bpl.Expr.Imp(FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, dId), q);
q = new Bpl.ForallExpr(ctor.tok, new VariableSeq(dBv), q);
sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));
@@ -525,11 +538,11 @@ namespace Microsoft.Dafny {
var cases_dId = new Bpl.IdentifierExpr(dt.tok, cases_dBv.Name, predef.DatatypeType);
Bpl.Expr cases_body = null;
foreach (DatatypeCtor ctor in dt.Ctors) {
- var disj = FunctionCall(ctor.tok, ctor.QueryField.FullName, Bpl.Type.Bool, cases_dId);
+ var disj = FunctionCall(ctor.tok, ctor.QueryField.FullCompileName, Bpl.Type.Bool, cases_dId);
cases_body = cases_body == null ? disj : Bpl.Expr.Or(cases_body, disj);
}
var cases_resType = new Bpl.Formal(dt.tok, new Bpl.TypedIdent(dt.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.FullName, new Bpl.VariableSeq(cases_dBv), cases_resType);
+ var cases_fn = new Bpl.Function(dt.tok, "$IsA#" + dt.FullCompileName, new Bpl.VariableSeq(cases_dBv), cases_resType);
cases_fn.Body = cases_body;
sink.TopLevelDeclarations.Add(cases_fn);
}
@@ -852,7 +865,7 @@ namespace Microsoft.Dafny {
Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())),
etran.InMethodContext());
// useViaCanCall: f#canCall(args)
- Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullName + "#canCall", Bpl.Type.Bool);
+ Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);
Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), args);
// ante := useViaCanCall || (useViaContext && typeAnte && pre)
@@ -957,7 +970,7 @@ namespace Microsoft.Dafny {
Contract.Requires(0 <= layer && layer < 3);
Contract.Ensures(Contract.Result<string>() != null);
- string name = f.FullName;
+ string name = f.FullCompileName;
switch (layer) {
case 2: name += "#2"; break;
case 0: name += "#limited"; break;
@@ -1140,7 +1153,7 @@ namespace Microsoft.Dafny {
foreach (var inFormal in m.Ins) {
var dt = inFormal.Type.AsDatatype;
if (dt != null) {
- var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullName, Bpl.Type.Bool));
+ var funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(inFormal.tok, "$IsA#" + dt.FullCompileName, Bpl.Type.Bool));
var f = new Bpl.IdentifierExpr(inFormal.tok, inFormal.UniqueName, TrType(inFormal.Type));
builder.Add(new Bpl.AssumeCmd(inFormal.tok, new Bpl.NAryExpr(inFormal.tok, funcID, new Bpl.ExprSeq(f))));
}
@@ -1455,8 +1468,8 @@ namespace Microsoft.Dafny {
if (wh != null) { wellFormed = Bpl.Expr.And(wellFormed, wh); }
}
- string axiomComment = "frame axiom for " + f.FullName;
- Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
+ string axiomComment = "frame axiom for " + f.FullCompileName;
+ Bpl.FunctionCall fn = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType)));
while (fn != null) {
Bpl.Expr F0 = new Bpl.NAryExpr(f.tok, fn, f0args);
Bpl.Expr F1 = new Bpl.NAryExpr(f.tok, fn, f1args);
@@ -1578,7 +1591,7 @@ namespace Microsoft.Dafny {
}
}
}
- Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullName, typeParams, inParams, new Bpl.VariableSeq(),
+ Bpl.Procedure proc = new Bpl.Procedure(f.tok, "CheckWellformed$$" + f.FullCompileName, typeParams, inParams, new Bpl.VariableSeq(),
req, new Bpl.IdentifierExprSeq(), ens, etran.TrAttributes(f.Attributes, null));
sink.TopLevelDeclarations.Add(proc);
@@ -1640,7 +1653,7 @@ namespace Microsoft.Dafny {
// don't fall through to postcondition checks
bodyCheckBuilder.Add(new Bpl.AssumeCmd(f.tok, Bpl.Expr.False));
} else {
- Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullName, TrType(f.ResultType)));
+ Bpl.FunctionCall funcID = new Bpl.FunctionCall(new Bpl.IdentifierExpr(f.tok, f.FullCompileName, TrType(f.ResultType)));
Bpl.ExprSeq args = new Bpl.ExprSeq();
args.Add(etran.HeapExpr);
foreach (Variable p in implInParams) {
@@ -1732,7 +1745,7 @@ namespace Microsoft.Dafny {
t = BplAnd(t, Bpl.Expr.Neq(etran.TrExpr(e.Obj), predef.Null));
} else if (e.Field is DatatypeDestructor) {
var dtor = (DatatypeDestructor)e.Field;
- t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));
+ t = BplAnd(t, FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullCompileName, Bpl.Type.Bool, etran.TrExpr(e.Obj)));
}
return t;
}
@@ -1991,7 +2004,7 @@ namespace Microsoft.Dafny {
// check well-formedness of the other parameters
r = BplAnd(r, CanCallAssumption(e.Args, etran));
// get to assume canCall
- Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);
+ Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool);
ExprSeq args = etran.FunctionInvocationArguments(e);
Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
r = BplAnd(r, canCallFuncAppl);
@@ -2234,7 +2247,7 @@ namespace Microsoft.Dafny {
CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);
} else if (e.Field is DatatypeDestructor) {
var dtor = (DatatypeDestructor)e.Field;
- var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullName, Bpl.Type.Bool, etran.TrExpr(e.Obj));
+ var correctConstructor = FunctionCall(e.tok, dtor.EnclosingCtor.QueryField.FullCompileName, Bpl.Type.Bool, etran.TrExpr(e.Obj));
if (dtor.EnclosingCtor.EnclosingDatatype.Ctors.Count == 1) {
// There is only one constructor, so the value must be been constructed by it; might as well assume that here.
builder.Add(new Bpl.AssumeCmd(expr.tok, correctConstructor));
@@ -2423,7 +2436,7 @@ namespace Microsoft.Dafny {
}
}
// all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance.
- Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);
+ Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullCompileName + "#canCall", Bpl.Type.Bool);
ExprSeq args = etran.FunctionInvocationArguments(e);
Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl)));
@@ -2799,12 +2812,26 @@ namespace Microsoft.Dafny {
if (classes.TryGetValue(cl, out cc)) {
Contract.Assert(cc != null);
} else {
- cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullName, predef.ClassNameType), true);
+ cc = new Bpl.Constant(cl.tok, new Bpl.TypedIdent(cl.tok, "class." + cl.FullCompileName, predef.ClassNameType), !cl.Module.IsAbstract);
classes.Add(cl, cc);
}
return cc;
}
+ Bpl.Constant GetFieldNameFamily(string n) {
+ Contract.Requires(n != null);
+ Contract.Requires(predef != null);
+ Contract.Ensures(Contract.Result<Bpl.Constant>() != null);
+ Bpl.Constant cc;
+ if (fieldConstants.TryGetValue(n, out cc)) {
+ Contract.Assert(cc != null);
+ } else {
+ cc = new Bpl.Constant(Token.NoToken, new Bpl.TypedIdent(Token.NoToken, "field$" + n, predef.NameFamilyType), true);
+ fieldConstants.Add(n, cc);
+ }
+ return cc;
+ }
+
Bpl.Expr GetTypeExpr(IToken tok, Type type)
{
Contract.Requires(tok != null);
@@ -2864,13 +2891,13 @@ namespace Microsoft.Dafny {
if (fields.TryGetValue(f, out fc)) {
Contract.Assert(fc != null);
} else {
- // const unique f: Field ty;
+ // const f: Field ty;
Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));
- fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullName, ty), true);
+ fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullCompileName, ty), false);
fields.Add(f, fc);
- // axiom FDim(f) == 0 && DeclType(f) == C;
+ // axiom FDim(f) == 0 && FieldOfDecl(C, name) == f;
Bpl.Expr fdim = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FDim, ty, Bpl.Expr.Ident(fc)), Bpl.Expr.Literal(0));
- Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.DeclType, ty, Bpl.Expr.Ident(fc)), new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))));
+ Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FieldOfDecl, ty, new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))), new Bpl.IdentifierExpr(f.tok, GetFieldNameFamily(f.Name))), Bpl.Expr.Ident(fc));
Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fdim, declType));
sink.TopLevelDeclarations.Add(ax);
}
@@ -2897,7 +2924,7 @@ namespace Microsoft.Dafny {
Bpl.Type receiverType = f.EnclosingClass is ClassDecl ? predef.RefType : predef.DatatypeType;
args.Add(new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, "this", receiverType), true));
Bpl.Formal result = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, ty), false);
- ff = new Bpl.Function(f.tok, f.FullName, args, result);
+ ff = new Bpl.Function(f.tok, f.FullCompileName, args, result);
fieldFunctions.Add(f, ff);
// treat certain fields specially
if (f.EnclosingClass is ArrayClassDecl) {
@@ -2939,7 +2966,7 @@ namespace Microsoft.Dafny {
args.Add(new Bpl.Formal(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)), true));
}
Bpl.Formal res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, TrType(f.ResultType)), false);
- Bpl.Function func = new Bpl.Function(f.tok, f.FullName, typeParams, args, res);
+ Bpl.Function func = new Bpl.Function(f.tok, f.FullCompileName, typeParams, args, res);
sink.TopLevelDeclarations.Add(func);
if (f.IsRecursive) {
@@ -2948,7 +2975,7 @@ namespace Microsoft.Dafny {
}
res = new Bpl.Formal(f.tok, new Bpl.TypedIdent(f.tok, Bpl.TypedIdent.NoName, Bpl.Type.Bool), false);
- Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullName + "#canCall", args, res);
+ Bpl.Function canCallF = new Bpl.Function(f.tok, f.FullCompileName + "#canCall", args, res);
sink.TopLevelDeclarations.Add(canCallF);
}
@@ -3055,10 +3082,10 @@ namespace Microsoft.Dafny {
Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(m.TypeArgs);
string name;
switch (kind) {
- case 0: name = "CheckWellformed$$" + m.FullName; break;
- case 1: name = m.FullName; break;
- case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullName); break;
- case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullName); break;
+ case 0: name = "CheckWellformed$$" + m.FullCompileName; break;
+ case 1: name = m.FullCompileName; break;
+ case 2: name = string.Format("RefinementCall_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break;
+ case 3: name = string.Format("RefinementImpl_{0}$${1}", m.EnclosingClass.Module.Name, m.FullCompileName); break;
default: Contract.Assert(false); throw new cce.UnreachableException(); // unexpected kind
}
Bpl.Procedure proc = new Bpl.Procedure(m.tok, name, typeParams, inParams, outParams, req, mod, ens);
@@ -4435,9 +4462,9 @@ namespace Microsoft.Dafny {
// Make the call
string name;
if (RefinementToken.IsInherited(method.tok, currentModule)) {
- name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullName);
+ name = string.Format("RefinementCall_{0}$${1}", currentModule.Name, method.FullCompileName);
} else {
- name = method.FullName;
+ name = method.FullCompileName;
}
Bpl.CallCmd call = new Bpl.CallCmd(tok, name, ins, outs);
builder.Add(call);
@@ -5307,7 +5334,7 @@ namespace Microsoft.Dafny {
typeArgs.Add(tRhs.EType);
rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(tok, "class._System." + BuiltIns.ArrayClassName(tRhs.ArrayDimensions.Count), predef.ClassNameType), typeArgs, true);
} else if (tRhs.EType is ObjectType) {
- rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(Token.NoToken,GetClass(program.BuiltIns.ObjectDecl)), new List<Type>(), true);
+ rightType = etran.GoodRef_Ref(tok, nw, new Bpl.IdentifierExpr(Token.NoToken, GetClass(program.BuiltIns.ObjectDecl)), new List<Type>(), true);
} else {
rightType = etran.GoodRef_Class(tok, nw, (UserDefinedType)tRhs.EType, true);
}
@@ -6541,6 +6568,7 @@ namespace Microsoft.Dafny {
DtTypeParams, // type parameters of datatype
TypeTuple,
DeclType,
+ FieldOfDecl,
FDim, // field dimension (0 - named, 1 or more - indexed)
DatatypeCtorId,
@@ -6779,6 +6807,10 @@ namespace Microsoft.Dafny {
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation != null);
return FunctionCall(tok, "DeclType", predef.ClassNameType, args);
+ case BuiltinFunction.FieldOfDecl:
+ Contract.Assert(args.Length == 2);
+ Contract.Assert(typeInstantiation != null);
+ return FunctionCall(tok, "FieldOfDecl", predef.FieldName(tok, typeInstantiation) , args);
case BuiltinFunction.FDim:
Contract.Assert(args.Length == 1);
Contract.Assert(typeInstantiation != null);
@@ -7022,7 +7054,7 @@ namespace Microsoft.Dafny {
// Note that "body" does not contain limited calls.
// F#canCall(args)
- Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullName + "#canCall", Bpl.Type.Bool);
+ Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, f.FullCompileName + "#canCall", Bpl.Type.Bool);
ExprSeq args = etran.FunctionInvocationArguments(fexp);
Bpl.Expr canCall = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);
diff --git a/Source/GPUVerify/CrossThreadInvariantProcessor.cs b/Source/GPUVerify/CrossThreadInvariantProcessor.cs
deleted file mode 100644
index 3d64f8dc..00000000
--- a/Source/GPUVerify/CrossThreadInvariantProcessor.cs
+++ /dev/null
@@ -1,136 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Linq;
-using System.Text;
-using Microsoft.Boogie;
-using System.Diagnostics;
-
-namespace GPUVerify
-{
- class CrossThreadInvariantProcessor : StandardVisitor
- {
- private GPUVerifier verifier;
- private string procName;
-
- public CrossThreadInvariantProcessor(GPUVerifier verifier, string procName)
- {
- this.verifier = verifier;
- this.procName = procName;
- }
-
- public override Expr VisitNAryExpr(NAryExpr node)
- {
-
- if (node.Fun is FunctionCall)
- {
- FunctionCall call = node.Fun as FunctionCall;
-
- if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool"))
- {
- return Expr.Eq(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
- }
-
- if (call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool"))
- {
- return Expr.Neq(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
- }
-
- if (call.Func.Name.Equals("__all"))
- {
- return Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr));
- }
-
- if (call.Func.Name.Equals("__exclusive"))
- {
- return Expr.Not(Expr.And(new VariableDualiser(1, verifier.uniformityAnalyser, procName).VisitExpr(node.Args[0].Clone() as Expr),
- new VariableDualiser(2, verifier.uniformityAnalyser, procName)
- .VisitExpr(node.Args[0].Clone() as Expr)));
- }
-
-
- }
-
- return base.VisitNAryExpr(node);
- }
-
-
- internal EnsuresSeq ProcessCrossThreadInvariants(EnsuresSeq ensuresSeq)
- {
- EnsuresSeq result = new EnsuresSeq();
- foreach (Ensures e in ensuresSeq)
- {
- result.Add(new Ensures(e.Free, VisitExpr(e.Condition.Clone() as Expr)));
- }
- return result;
- }
-
- internal RequiresSeq ProcessCrossThreadInvariants(RequiresSeq requiresSeq)
- {
- RequiresSeq result = new RequiresSeq();
- foreach (Requires r in requiresSeq)
- {
- result.Add(new Requires(r.Free, VisitExpr(r.Condition.Clone() as Expr)));
- }
- return result;
- }
-
- internal void ProcessCrossThreadInvariants(StmtList stmtList)
- {
- foreach (BigBlock bb in stmtList.BigBlocks)
- {
- ProcessCrossThreadInvariants(bb);
- }
- }
-
- internal void ProcessCrossThreadInvariants(List<Block> blocks)
- {
- foreach (Block b in blocks)
- {
- b.Cmds = ProcessCrossThreadInvariants(b.Cmds);
- }
- }
-
- private void ProcessCrossThreadInvariants(BigBlock bb)
- {
- bb.simpleCmds = ProcessCrossThreadInvariants(bb.simpleCmds);
-
- if (bb.ec is WhileCmd)
- {
- WhileCmd whileCmd = bb.ec as WhileCmd;
- List<PredicateCmd> newInvariants = new List<PredicateCmd>();
- foreach (PredicateCmd p in whileCmd.Invariants)
- {
- newInvariants.Add(new AssertCmd(p.tok, VisitExpr(p.Expr)));
- }
- whileCmd.Invariants = newInvariants;
- ProcessCrossThreadInvariants(whileCmd.Body);
- }
- }
-
- private CmdSeq ProcessCrossThreadInvariants(CmdSeq cmds)
- {
- CmdSeq newCommands = new CmdSeq();
-
- foreach (Cmd c in cmds)
- {
- if (c is AssertCmd)
- {
- newCommands.Add(new AssertCmd(c.tok, VisitExpr((c as AssertCmd).Expr.Clone() as Expr)));
- }
- else if (c is AssumeCmd)
- {
- newCommands.Add(new AssumeCmd(c.tok, VisitExpr((c as AssumeCmd).Expr.Clone() as Expr)));
- }
- else
- {
- newCommands.Add(c);
- }
- }
- return newCommands;
- }
-
- }
-}
diff --git a/Source/GPUVerify/GPUVerifier.cs b/Source/GPUVerify/GPUVerifier.cs
index 79a73a29..fdefdebd 100644
--- a/Source/GPUVerify/GPUVerifier.cs
+++ b/Source/GPUVerify/GPUVerifier.cs
@@ -415,8 +415,6 @@ namespace GPUVerify
emitProgram(outputFilename + "_dualised");
}
- ProcessCrossThreadInvariants();
-
if (CommandLineOptions.ShowStages)
{
emitProgram(outputFilename + "_cross_thread_invariants");
@@ -621,34 +619,6 @@ namespace GPUVerify
return result;
}
- private void ProcessCrossThreadInvariants()
- {
- foreach (Declaration d in Program.TopLevelDeclarations)
- {
- if (d is Procedure)
- {
- Procedure p = d as Procedure;
- p.Requires = new CrossThreadInvariantProcessor(this, p.Name).ProcessCrossThreadInvariants(p.Requires);
- p.Ensures = new CrossThreadInvariantProcessor(this, p.Name).ProcessCrossThreadInvariants(p.Ensures);
- }
- if (d is Implementation)
- {
- Implementation impl = d as Implementation;
-
- if (CommandLineOptions.Unstructured)
- {
- new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.Blocks);
- }
- else
- {
- new CrossThreadInvariantProcessor(this, impl.Name).ProcessCrossThreadInvariants(impl.StructuredStmts);
- }
- }
-
- }
- }
-
-
private void emitProgram(string filename)
{
using (TokenTextWriter writer = new TokenTextWriter(filename + ".bpl"))
diff --git a/Source/GPUVerify/GPUVerify.csproj b/Source/GPUVerify/GPUVerify.csproj
index 0bf1cbc4..9b3b08cb 100644
--- a/Source/GPUVerify/GPUVerify.csproj
+++ b/Source/GPUVerify/GPUVerify.csproj
@@ -121,7 +121,6 @@
<Compile Include="LoopInvariantGenerator.cs" />
<Compile Include="MayBePowerOfTwoAnalyser.cs" />
<Compile Include="StructuredProgramVisitor.cs" />
- <Compile Include="CrossThreadInvariantProcessor.cs" />
<Compile Include="EnabledToPredicateVisitor.cs" />
<Compile Include="CommandLineOptions.cs" />
<Compile Include="GPUVerifier.cs" />
@@ -179,4 +178,4 @@
<Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project> \ No newline at end of file
diff --git a/Source/GPUVerify/VariableDualiser.cs b/Source/GPUVerify/VariableDualiser.cs
index 63720c13..ddaf2062 100644
--- a/Source/GPUVerify/VariableDualiser.cs
+++ b/Source/GPUVerify/VariableDualiser.cs
@@ -78,11 +78,12 @@ namespace GPUVerify
{
FunctionCall call = node.Fun as FunctionCall;
- if (call.Func.Name.Equals("__uniform_bv32") || call.Func.Name.Equals("__uniform_bool") ||
- call.Func.Name.Equals("__distinct_bv32") || call.Func.Name.Equals("__distinct_bool") ||
- call.Func.Name.Equals("__all") || call.Func.Name.Equals("__at_most_one"))
+ if (call.Func.Name.Equals("__other_bool") || call.Func.Name.Equals("__other_bv32"))
{
- return node;
+ Debug.Assert(id == 1 || id == 2);
+ int otherId = id == 1 ? 2 : 1;
+ return new VariableDualiser(otherId, uniformityAnalyser, procName).VisitExpr(
+ node.Args[0]);
}
}
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 31afbdfa..8c6ad875 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -425,7 +425,7 @@ namespace Microsoft.Boogie.SMTLib
xlabels = labels.Select(a => a.Replace("@", "").Replace("+", "")).ToList();
}
else {
- labels = CalculatePath(0);
+ labels = CalculatePath(handler.StartingProcId());
xlabels = labels;
}
Model model = GetErrorModel();
diff --git a/Source/VCGeneration/BlockPredicator.cs b/Source/VCGeneration/BlockPredicator.cs
index 226b05e7..9df1c086 100644
--- a/Source/VCGeneration/BlockPredicator.cs
+++ b/Source/VCGeneration/BlockPredicator.cs
@@ -77,7 +77,8 @@ public class BlockPredicator {
// the first statement in the block.
var assign = cmdSeq.Last();
cmdSeq.Truncate(cmdSeq.Length-1);
- aCmd.Expr = Expr.Imp(pExpr, aCmd.Expr);
+ Expr newExpr = new EnabledReplacementVisitor(pExpr).VisitExpr(aCmd.Expr);
+ aCmd.Expr = QKeyValue.FindBoolAttribute(aCmd.Attributes, "do_not_predicate") ? newExpr : Expr.Imp(pExpr, newExpr);
cmdSeq.Add(aCmd);
// cmdSeq.Add(new AssertCmd(aCmd.tok, Expr.Imp(pExpr, aCmd.Expr)));
cmdSeq.Add(assign);
@@ -307,7 +308,26 @@ public class BlockPredicator {
dwf.InParams = new VariableSeq(
(new Variable[] {fpVar}.Concat(dwf.InParams.Cast<Variable>()))
.ToArray());
+
+ if (dwf is Procedure)
+ {
+ var proc = (Procedure)dwf;
+ var newRequires = new RequiresSeq();
+ foreach (Requires r in proc.Requires)
+ {
+ newRequires.Add(new Requires(r.Free,
+ new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(r.Condition)));
+ }
+ var newEnsures = new EnsuresSeq();
+ foreach (Ensures e in proc.Ensures)
+ {
+ newEnsures.Add(new Ensures(e.Free,
+ new EnabledReplacementVisitor(new IdentifierExpr(Token.NoToken, fpVar)).VisitExpr(e.Condition)));
+ }
+ }
+
}
+
try {
var impl = decl as Implementation;
if (impl != null)
@@ -326,4 +346,28 @@ public class BlockPredicator {
}
+
+class EnabledReplacementVisitor : StandardVisitor
+{
+ private Expr pExpr;
+
+ internal EnabledReplacementVisitor(Expr pExpr)
+ {
+ this.pExpr = pExpr;
+ }
+
+ public override Expr VisitExpr(Expr node)
+ {
+ if (node is IdentifierExpr)
+ {
+ IdentifierExpr iExpr = node as IdentifierExpr;
+ if (iExpr.Decl is Constant && QKeyValue.FindBoolAttribute(iExpr.Decl.Attributes, "__enabled"))
+ {
+ return pExpr;
+ }
+ }
+ return base.VisitExpr(node);
+ }
+}
+
}
diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index e3b1cb2d..1f50d4a8 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -367,6 +367,12 @@ namespace Microsoft.Boogie {
Undetermined
}
public class ErrorHandler {
+ // Used in CheckOutcomeCore
+ public virtual int StartingProcId()
+ {
+ return 0;
+ }
+
public virtual void OnModel(IList<string> labels, Model model) {
Contract.Requires(cce.NonNullElements(labels));
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 15:50:00 +0000