diff options
Diffstat (limited to 'BCT/BytecodeTranslator')
| -rw-r--r-- | BCT/BytecodeTranslator/ExpressionTraverser.cs | 4 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Heap.cs | 141 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/Program.cs | 92 | ||||
| -rw-r--r-- | BCT/BytecodeTranslator/TranslationHelper.cs | 12 |
4 files changed, 195 insertions, 54 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs index 150518b0..dd6cbb66 100644 --- a/BCT/BytecodeTranslator/ExpressionTraverser.cs +++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs @@ -462,7 +462,7 @@ namespace BytecodeTranslator outvars.Add(new Bpl.IdentifierExpr(cloc, v));
TranslatedExpressions.Push(new Bpl.IdentifierExpr(cloc, v));
}
- string methodname = TranslationHelper.CreateUniqueMethodName(resolvedMethod);
+ string methodname = TranslationHelper.CreateUniqueMethodName(methodCall.MethodToCall);
Bpl.QKeyValue attrib = null;
@@ -626,7 +626,7 @@ namespace BytecodeTranslator }
Bpl.IdentifierExprSeq outvars = new Bpl.IdentifierExprSeq();
- string methodname = TranslationHelper.CreateUniqueMethodName(ctor.ResolvedMethod);
+ string methodname = TranslationHelper.CreateUniqueMethodName(ctor);
this.StmtTraverser.StmtBuilder.Add(new Bpl.CallCmd(cloc, methodname, inexpr, outvars));
diff --git a/BCT/BytecodeTranslator/Heap.cs b/BCT/BytecodeTranslator/Heap.cs index cfc30c97..33610930 100644 --- a/BCT/BytecodeTranslator/Heap.cs +++ b/BCT/BytecodeTranslator/Heap.cs @@ -213,6 +213,147 @@ procedure {:inline 1} Alloc() returns (x: int) }
+ /// <summary>
+ /// A heap representation that uses a global variable, $Heap, which is
+ /// a two-dimensional array indexed by objects and fields. Objects
+ /// are values of type "int", fields are unique constants, and the
+ /// elements of the heap are of type "box". Each value that is read/written
+ /// from/to the heap is wrapped in a type conversion function.
+ /// </summary>
+ public class TwoDBoxHeap : HeapFactory, IHeap {
+
+ #region Fields
+ [RepresentationFor("$Heap", "var $Heap: HeapType where IsGoodHeap($Heap);", true)]
+ private Bpl.Variable HeapVariable = null;
+
+ [RepresentationFor("Box2Int", "function Box2Int(box): int;")]
+ private Bpl.Function Box2Int = null;
+
+ [RepresentationFor("Box2Bool", "function Box2Bool(box): bool;")]
+ private Bpl.Function Box2Bool = null;
+
+ [RepresentationFor("Int2Box", "function Int2Box(int): box;")]
+ private Bpl.Function Int2Box = null;
+
+ [RepresentationFor("Bool2Box", "function Bool2Box(bool): box;")]
+ private Bpl.Function Bool2Box = null;
+
+ /// <summary>
+ /// Prelude text for which access to the ASTs is not needed
+ /// </summary>
+ private readonly string InitialPreludeText =
+ @"const null: int;
+type box;
+type HeapType = [int,int]box;
+function IsGoodHeap(HeapType): bool;
+var $ArrayContents: [int][int]int;
+var $ArrayLength: [int]int;
+
+var $Alloc: [int] bool;
+procedure {:inline 1} Alloc() returns (x: int)
+ free ensures x != 0;
+ modifies $Alloc;
+{
+ assume $Alloc[x] == false;
+ $Alloc[x] := true;
+}
+";
+ private Sink sink;
+
+ #endregion
+
+ public override bool MakeHeap(Sink sink, out IHeap heap, out Bpl.Program/*?*/ program) {
+ this.sink = sink;
+ heap = this;
+ program = null;
+ var b = RepresentationFor.ParsePrelude(this.InitialPreludeText, this, out program);
+ return b;
+ }
+
+ /// <summary>
+ /// Creates a fresh BPL variable to represent <paramref name="field"/>, deciding
+ /// on its type based on the heap representation.
+ /// </summary>
+ public Bpl.Variable CreateFieldVariable(IFieldReference field) {
+ Bpl.Variable v;
+ string fieldname = TypeHelper.GetTypeName(field.ContainingType) + "." + field.Name.Value;
+ Bpl.IToken tok = field.Token();
+ Bpl.Type t = TranslationHelper.CciTypeToBoogie(field.Type.ResolvedType);
+
+ if (field.IsStatic) {
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
+ v = new Bpl.GlobalVariable(tok, tident);
+ } else {
+ Bpl.TypedIdent tident = new Bpl.TypedIdent(tok, fieldname, t);
+ v = new Bpl.Constant(tok, tident, true);
+ }
+ return v;
+ }
+
+ /// <summary>
+ /// Returns the (typed) BPL expression that corresponds to the value of the field
+ /// <paramref name="f"/> belonging to the object <paramref name="o"/> (when
+ /// <paramref name="o"/> is non-null, otherwise the value of the static field.
+ /// </summary>
+ /// <param name="o">The expression that represents the object to be dereferenced.
+ /// Null if <paramref name="f"/> is a static field.
+ /// </param>
+ /// <param name="f">The field that is used to dereference the object <paramref name="o"/>, when
+ /// it is not null. Otherwise the static field whose value should be read.
+ /// </param>
+ public Bpl.Expr ReadHeap(Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f) {
+ // $Heap[o,f]
+ var selectExpr = Bpl.Expr.Select(new Bpl.IdentifierExpr(f.tok, HeapVariable), new Bpl.Expr[] { o, f });
+ // wrap it in the right conversion function
+ Bpl.Function conversion;
+ if (f.Type == Bpl.Type.Bool)
+ conversion = this.Box2Bool;
+ else if (f.Type == Bpl.Type.Int)
+ conversion = this.Box2Int;
+ else
+ throw new InvalidOperationException("Unknown Boogie type");
+ var callExpr = new Bpl.NAryExpr(
+ f.tok,
+ new Bpl.FunctionCall(conversion),
+ new Bpl.ExprSeq(selectExpr)
+ );
+ return callExpr;
+
+ }
+
+ /// <summary>
+ /// Returns the BPL command that corresponds to assigning the value <paramref name="value"/>
+ /// to the field <paramref name="f"/> of the object <paramref name="o"/> (when
+ /// <paramref name="o"/> is non-null, otherwise it is an assignment to the static
+ /// field.
+ /// </summary>
+ public Bpl.Cmd WriteHeap(Bpl.IToken tok, Bpl.Expr/*?*/ o, Bpl.IdentifierExpr f, Bpl.Expr value) {
+ if (o == null) {
+ return Bpl.Cmd.SimpleAssign(tok, f, value);
+ } else {
+ // wrap it in the right conversion function
+ Bpl.Function conversion;
+ if (f.Type == Bpl.Type.Bool)
+ conversion = this.Bool2Box;
+ else if (f.Type == Bpl.Type.Int)
+ conversion = this.Int2Box;
+ else
+ throw new InvalidOperationException("Unknown Boogie type");
+
+ // $Heap[o,f] := conversion(value)
+ var callExpr = new Bpl.NAryExpr(
+ f.tok,
+ new Bpl.FunctionCall(conversion),
+ new Bpl.ExprSeq(value)
+ );
+ return
+ Bpl.Cmd.MapAssign(tok,
+ new Bpl.IdentifierExpr(tok, this.HeapVariable), new Bpl.ExprSeq(o, f), callExpr);
+ }
+ }
+
+ }
+
internal class RepresentationFor : Attribute {
internal string name;
internal string declaration;
diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs index 12ed25a0..09a82009 100644 --- a/BCT/BytecodeTranslator/Program.cs +++ b/BCT/BytecodeTranslator/Program.cs @@ -16,64 +16,58 @@ using Microsoft.Cci.ILToCodeModel; using Bpl = Microsoft.Boogie;
namespace BytecodeTranslator {
- public class CommandLineOptions
- {
- public static bool SplitFields = false;
+
+ class Options : OptionParsing {
+
+ [OptionDescription("The name of the assembly to use as input", ShortForm = "a")]
+ public string assembly = null;
+
+ [OptionDescription("Search paths for assembly dependencies.", ShortForm = "lib")]
+ public List<string> libpaths = new List<string>();
+
+ public enum HeapRepresentation { splitFields, twoDInt, twoDBox }
+ [OptionDescription("Heap representation to use", ShortForm = "heap")]
+ public HeapRepresentation heapRepresentation = HeapRepresentation.twoDInt;
+
}
public class BCT {
public static IMetadataHost Host;
- public static bool Parse(string[] args, out string assemblyName)
- {
- assemblyName = "";
-
- foreach (string arg in args)
- {
- if (arg.StartsWith("/"))
- {
- if (arg == "/splitFields")
- {
- CommandLineOptions.SplitFields = true;
- }
- else
- {
- Console.WriteLine("Illegal option.");
- return false;
- }
- }
- else if (assemblyName == "")
- {
- assemblyName = arg;
- }
- else
- {
- Console.WriteLine("Must specify only one input assembly.");
- return false;
- }
- }
- if (assemblyName == "")
- {
- Console.WriteLine("Must specify an input assembly.");
- return false;
- }
- return true;
- }
-
static int Main(string[] args)
{
int result = 0;
- string assemblyName;
- if (!Parse(args, out assemblyName))
- return result;
+
+ #region Parse options
+ var options = new Options();
+ options.Parse(args);
+ if (options.HasErrors) {
+ if (options.HelpRequested)
+ options.PrintOptions("");
+ return 1;
+ }
+ #endregion
+
+ var assemblyName = String.IsNullOrEmpty(options.assembly) ? options.GeneralArguments[0] : options.assembly;
+
try {
HeapFactory heap;
- if (CommandLineOptions.SplitFields)
- heap = new SplitFieldsHeap();
- else
- heap = new TwoDIntHeap();
- result = TranslateAssembly(assemblyName, heap);
+ switch (options.heapRepresentation) {
+ case Options.HeapRepresentation.splitFields:
+ heap = new SplitFieldsHeap();
+ break;
+ case Options.HeapRepresentation.twoDInt:
+ heap = new TwoDIntHeap();
+ break;
+ case Options.HeapRepresentation.twoDBox:
+ heap = new TwoDBoxHeap();
+ break;
+ default:
+ Console.WriteLine("Unknown setting for /heap");
+ return 1;
+ }
+ result = TranslateAssembly(assemblyName, heap, options.libpaths);
} catch (Exception e) { // swallow everything and just return an error code
Console.WriteLine("The byte-code translator failed with uncaught exception: {0}", e.Message);
Console.WriteLine("Stack trace: {0}", e.StackTrace);
@@ -82,9 +76,9 @@ namespace BytecodeTranslator { return result;
}
- public static int TranslateAssembly(string assemblyName, HeapFactory heapFactory) {
+ public static int TranslateAssembly(string assemblyName, HeapFactory heapFactory, List<string>/*?*/ libPaths) {
- var host = new Microsoft.Cci.MutableContracts.CodeContractAwareHostEnvironment();
+ var host = new Microsoft.Cci.MutableContracts.CodeContractAwareHostEnvironment(libPaths != null ? libPaths : IteratorHelper.GetEmptyEnumerable<string>(), true, true);
Host = host;
IModule/*?*/ module = host.LoadUnitFrom(assemblyName) as IModule;
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs index 1a326440..9f90f94d 100644 --- a/BCT/BytecodeTranslator/TranslationHelper.cs +++ b/BCT/BytecodeTranslator/TranslationHelper.cs @@ -79,8 +79,9 @@ namespace BytecodeTranslator { return "$tmp" + (tmpVarCounter++).ToString();
}
- public static string CreateUniqueMethodName(IMethodDefinition method) {
- if (method.ContainingType.ToString() == "Poirot.Poirot")
+ public static string CreateUniqueMethodName(IMethodReference method) {
+ var containingTypeName = TypeHelper.GetTypeName(method.ContainingType, NameFormattingOptions.None);
+ if (containingTypeName == "Poirot.Poirot")
{
string name = method.Name.Value;
if (name == "BeginAtomic")
@@ -92,7 +93,12 @@ namespace BytecodeTranslator { else if (name == "Nondet")
return "poirot_nondet";
}
- return method.ContainingType.ToString() + "." + method.Name.Value + "$" + method.Type.ResolvedType.ToString();
+ var s = MemberHelper.GetMethodSignature(method, NameFormattingOptions.DocumentationId);
+ s = s.Substring(2);
+ s = s.Replace('(', '$');
+ s = s.Replace(',', '$');
+ s = s.TrimEnd(')');
+ return s;
}
#region Temp Stuff that must be replaced as soon as there is real code to deal with this
|