diff options
| -rw-r--r-- | BCT/BytecodeTranslator/HeapFactory.cs | 25 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 1 | ||||
| -rw-r--r-- | Source/Core/Absy.cs | 28 | ||||
| -rw-r--r-- | Source/Core/Parser.cs | 1 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 2 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 2 |
6 files changed, 35 insertions, 24 deletions
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs index f5f0bf61..d5556bba 100644 --- a/BCT/BytecodeTranslator/HeapFactory.cs +++ b/BCT/BytecodeTranslator/HeapFactory.cs @@ -77,7 +77,7 @@ namespace BytecodeTranslator { #region Boogie Types
- [RepresentationFor("Delegate", "type Delegate;")]
+ [RepresentationFor("Delegate", "type {:datatype} Delegate;")]
public Bpl.TypeCtorDecl DelegateTypeDecl = null;
public Bpl.CtorType DelegateType;
@@ -403,10 +403,6 @@ procedure {:inline 1} Wrapper_System.Threading.ThreadStart.Invoke(this: Ref) { }
procedure {:extern} System.Threading.ThreadStart.Invoke(this: Ref);
-axiom (forall m: int, o: Ref, t: Type :: {$DelegateCons(m, o, t)} $DelegateMethod($DelegateCons(m, o, t)) == m);
-axiom (forall m: int, o: Ref, t: Type :: {$DelegateCons(m, o, t)} $DelegateReceiver($DelegateCons(m, o, t)) == o);
-axiom (forall m: int, o: Ref, t: Type :: {$DelegateCons(m, o, t)} $DelegateTypeParameters($DelegateCons(m, o, t)) == t);
-
axiom (forall d: Delegate :: { MultisetEmpty[d] } MultisetEmpty[d] == 0);
axiom (forall x: Delegate :: { MultisetSingleton(x) } MultisetSingleton(x)[x] == 1);
axiom (forall x: Delegate, d: Delegate :: {MultisetSingleton(x)[d]} MultisetSingleton(x)[d] == (if (x == d) then 1 else 0));
@@ -514,17 +510,20 @@ implementation System.Windows.Controls.Primitives.ToggleButton.get_IsChecked($th [RepresentationFor("$Delegate", "function $Delegate(Ref): DelegateMultiset;")]
public Bpl.Function Delegate = null;
- [RepresentationFor("$DelegateCons", "function $DelegateCons(int, Ref, Type): Delegate;")]
- public Bpl.Function DelegateCons = null;
+ [RepresentationFor("$DelegateCons", "function {:constructor} $DelegateCons($Method: int, $Receiver: Ref, $TypeParameters: Type): Delegate;")]
+ public Bpl.DatatypeConstructor DelegateCons = null;
- [RepresentationFor("$DelegateMethod", "function $DelegateMethod(Delegate): int;")]
- public Bpl.Function DelegateMethod = null;
+ public Bpl.Function DelegateMethod {
+ get { return DelegateCons.selectors[0]; }
+ }
- [RepresentationFor("$DelegateReceiver", "function $DelegateReceiver(Delegate): Ref;")]
- public Bpl.Function DelegateReceiver = null;
+ public Bpl.Function DelegateReceiver {
+ get { return DelegateCons.selectors[1]; }
+ }
- [RepresentationFor("$DelegateTypeParameters", "function $DelegateTypeParameters(Delegate): Type;")]
- public Bpl.Function DelegateTypeParameters = null;
+ public Bpl.Function DelegateTypeParameters {
+ get { return DelegateCons.selectors[2]; }
+ }
[RepresentationFor("$Exception", "var {:thread_local} $Exception: Ref;")]
public Bpl.GlobalVariable ExceptionVariable = null;
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index eaef7e40..ddcb2c07 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -77,7 +77,6 @@ namespace BytecodeTranslator { static int Main(string[] args)
{
- int result = 0;
int errorReturnValue = -1;
#region Parse options and check for errors
diff --git a/Source/Core/Absy.cs b/Source/Core/Absy.cs index 500cb0ca..7ff0af6c 100644 --- a/Source/Core/Absy.cs +++ b/Source/Core/Absy.cs @@ -213,8 +213,8 @@ namespace Microsoft.Boogie { Emitter.Declarations(this.TopLevelDeclarations, stream);
}
- void CreateDatatypeSelectorsAndTesters() {
- Dictionary<string, Function> constructors = new Dictionary<string, Function>();
+ public void ProcessDatatypeConstructors() {
+ Dictionary<string, DatatypeConstructor> constructors = new Dictionary<string, DatatypeConstructor>();
List<Declaration> prunedTopLevelDeclarations = new List<Declaration>();
foreach (Declaration decl in TopLevelDeclarations) {
Function func = decl as Function;
@@ -223,17 +223,20 @@ namespace Microsoft.Boogie { continue;
}
if (constructors.ContainsKey(func.Name)) continue;
- constructors.Add(func.Name, func);
- prunedTopLevelDeclarations.Add(func);
+ DatatypeConstructor constructor = new DatatypeConstructor(func);
+ constructors.Add(func.Name, constructor);
+ prunedTopLevelDeclarations.Add(constructor);
}
TopLevelDeclarations = prunedTopLevelDeclarations;
-
- foreach (Function f in constructors.Values) {
+
+ foreach (DatatypeConstructor f in constructors.Values) {
for (int i = 0; i < f.InParams.Length; i++) {
DatatypeSelector selector = new DatatypeSelector(f, i);
+ f.selectors.Add(selector);
TopLevelDeclarations.Add(selector);
}
DatatypeMembership membership = new DatatypeMembership(f);
+ f.membership = membership;
TopLevelDeclarations.Add(membership);
}
}
@@ -256,8 +259,6 @@ namespace Microsoft.Boogie { //Contract.Requires(rc != null);
Helpers.ExtraTraceInformation("Starting resolution");
- CreateDatatypeSelectorsAndTesters();
-
foreach (Declaration d in TopLevelDeclarations) {
d.Register(rc);
}
@@ -1791,6 +1792,17 @@ namespace Microsoft.Boogie { }
}
+ public class DatatypeConstructor : Function {
+ public List<DatatypeSelector> selectors;
+ public DatatypeMembership membership;
+
+ public DatatypeConstructor(Function func)
+ : base(func.tok, func.Name, func.TypeParameters, func.InParams, func.OutParams[0], func.Comment, func.Attributes)
+ {
+ selectors = new List<DatatypeSelector>();
+ }
+ }
+
public class DatatypeSelector : Function {
public Function constructor;
public int index;
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 3602339e..fe77bcc1 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -85,6 +85,7 @@ Contract.Requires(cce.NonNullElements(defines,true)); if (parser.errors.count == 0)
{
program = Pgm;
+ program.ProcessDatatypeConstructors();
return 0;
}
else
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index dab0807f..e837b16f 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -841,7 +841,7 @@ namespace Microsoft.Boogie.SMTLib }
public override void DeclareFunction(Function f, string attributes) {
- if (QKeyValue.FindBoolAttribute(f.Attributes, "constructor")) {
+ if (f is DatatypeConstructor) {
CtorType datatype = (CtorType) f.OutParams[0].TypedIdent.Type;
if (!KnownDatatypeConstructors.ContainsKey(datatype))
KnownDatatypeConstructors[datatype] = new List<Function>();
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 4a4ecfb6..40dc7cf6 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -266,7 +266,7 @@ void ObjectInvariant() public static bool IsDatatypeFunction(Function f) {
return
- QKeyValue.FindBoolAttribute(f.Attributes, "constructor") ||
+ f is DatatypeConstructor ||
f is DatatypeSelector ||
f is DatatypeMembership;
}
|