various bug fixes related to running bct on phone apps

6 files changed, 142 insertions, 23 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 9c99d8fc..3067975d 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -530,7 +530,7 @@ namespace BytecodeTranslator
           inexpr[0] = Bpl.Expr.Ident(local);

         }

 

-        System.Diagnostics.Debug.Assert(outvars.Count == 1);

+        System.Diagnostics.Debug.Assert(outvars.Count == 0);

         outvars.Insert(0, Bpl.Expr.Ident(local));

         string methodName = isEventAdd ? this.sink.DelegateAddName : this.sink.DelegateRemoveName;

         call = new Bpl.CallCmd(methodCallToken, methodName, inexpr, outvars);

@@ -1063,7 +1063,23 @@ namespace BytecodeTranslator
       base.Visit(greaterThan);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Gt, lexp, rexp));

+

+      Bpl.Expr e;

+      switch (greaterThan.LeftOperand.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            greaterThan.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealGreaterThan),

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Gt, lexp, rexp);

+          break;

+      }

+

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(IGreaterThanOrEqual greaterEqual)

@@ -1071,7 +1087,23 @@ namespace BytecodeTranslator
       base.Visit(greaterEqual);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Ge, lexp, rexp));

+

+      Bpl.Expr e;

+      switch (greaterEqual.LeftOperand.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            greaterEqual.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealGreaterThanOrEqual),

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Ge, lexp, rexp);

+          break;

+      } 

+      

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(ILessThan lessThan)

@@ -1079,7 +1111,23 @@ namespace BytecodeTranslator
       base.Visit(lessThan);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Lt, lexp, rexp));

+

+      Bpl.Expr e;

+      switch (lessThan.LeftOperand.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            lessThan.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealLessThan),

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Lt, lexp, rexp);

+          break;

+      }

+

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(ILessThanOrEqual lessEqual)

@@ -1087,7 +1135,23 @@ namespace BytecodeTranslator
       base.Visit(lessEqual);

       Bpl.Expr rexp = TranslatedExpressions.Pop();

       Bpl.Expr lexp = TranslatedExpressions.Pop();

-      TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Le, lexp, rexp));

+

+      Bpl.Expr e;

+      switch (lessEqual.LeftOperand.Type.TypeCode) {

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          e = new Bpl.NAryExpr(

+            lessEqual.Token(),

+            new Bpl.FunctionCall(this.sink.Heap.RealLessThanOrEqual),

+            new Bpl.ExprSeq(lexp, rexp)

+            );

+          break;

+        default:

+          e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Le, lexp, rexp);

+          break;

+      }

+

+      TranslatedExpressions.Push(e);

     }

 

     public override void Visit(IEquality equal)

@@ -1393,6 +1457,16 @@ namespace BytecodeTranslator
     {

       base.Visit(logicalNot.Operand);

       Bpl.Expr exp = TranslatedExpressions.Pop();

+      Bpl.Type operandType = this.sink.CciTypeToBoogie(logicalNot.Operand.Type);

+      if (operandType == this.sink.Heap.RefType) {

+        exp = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      }

+      else if (operandType == Bpl.Type.Int) {

+        exp = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Literal(0));

+      }

+      else {

+        //System.Diagnostics.Debug.Assert(operandType == Bpl.Type.Bool);

+      }

       TranslatedExpressions.Push(Bpl.Expr.Unary(

           logicalNot.Token(),

           Bpl.UnaryOperator.Opcode.Not, exp));

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index c3e04902..c63791e2 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -225,7 +225,7 @@ namespace BytecodeTranslator {
     public Bpl.Function Real2Int = null;

     [RepresentationFor("Ref2Real", "function Ref2Real(Ref, Type, Type): Real;")]

     public Bpl.Function Ref2Real = null;

-    [RepresentationFor("Real2Ref", "function Real2Ref(Real, Type, Type): Ref;")]

+    [RepresentationFor("Real2Ref", "function Real2Ref(Real): Ref;")]

     public Bpl.Function Real2Ref = null;

     #endregion

 

@@ -238,6 +238,14 @@ namespace BytecodeTranslator {
     public Bpl.Function RealTimes = null;

     [RepresentationFor("RealDivide", "function RealDivide(Real, Real): Real;")]

     public Bpl.Function RealDivide = null;

+    [RepresentationFor("RealLessThan", "function RealLessThan(Real, Real): bool;")]

+    public Bpl.Function RealLessThan = null;

+    [RepresentationFor("RealLessThanOrEqual", "function RealLessThanOrEqual(Real, Real): bool;")]

+    public Bpl.Function RealLessThanOrEqual = null;

+    [RepresentationFor("RealGreaterThan", "function RealGreaterThan(Real, Real): bool;")]

+    public Bpl.Function RealGreaterThan = null;

+    [RepresentationFor("RealGreaterThanOrEqual", "function RealGreaterThanOrEqual(Real, Real): bool;")]

+    public Bpl.Function RealGreaterThanOrEqual = null;

     #endregion

 

     #region Bitwise operations

diff --git a/BCT/BytecodeTranslator/Program.cs b/BCT/BytecodeTranslator/Program.cs
index d447874a..cb0836f2 100644
--- a/BCT/BytecodeTranslator/Program.cs
+++ b/BCT/BytecodeTranslator/Program.cs
@@ -183,8 +183,8 @@ namespace BytecodeTranslator {
       MetadataTraverser translator = traverserFactory.MakeMetadataTraverser(sink, contractExtractors, pdbReaders);

       translator.TranslateAssemblies(modules);

 

-      foreach (ITypeDefinition type in sink.delegateTypeToDelegates.Keys) {

-        CreateDispatchMethod(sink, type);

+      foreach (var pair in sink.delegateTypeToDelegates.Values) {

+        CreateDispatchMethod(sink, pair.Item1, pair.Item2);

       }

 

       Microsoft.Boogie.TokenTextWriter writer = new Microsoft.Boogie.TokenTextWriter(primaryModule.Name + ".bpl");

@@ -230,7 +230,7 @@ namespace BytecodeTranslator {
       ifStmtBuilder.Add(new Bpl.ReturnCmd(b.tok));

       return new Bpl.IfCmd(b.tok, b, ifStmtBuilder.Collect(b.tok), null, null);

     }

-    private static void CreateDispatchMethod(Sink sink, ITypeDefinition type) {

+    private static void CreateDispatchMethod(Sink sink, ITypeDefinition type, HashSet<IMethodDefinition> delegates) {

       Contract.Assert(type.IsDelegate);

       IMethodDefinition invokeMethod = null;

       foreach (IMethodDefinition m in type.Methods) {

@@ -276,7 +276,7 @@ namespace BytecodeTranslator {
         sink.TranslatedProgram.TopLevelDeclarations.Add(dispatchProc);

 

         Bpl.IfCmd ifCmd = BuildIfCmd(Bpl.Expr.True, new Bpl.AssumeCmd(token, Bpl.Expr.False), null);

-        foreach (IMethodDefinition defn in sink.delegateTypeToDelegates[type]) {

+        foreach (IMethodDefinition defn in delegates) {

           Bpl.ExprSeq ins = new Bpl.ExprSeq();

           Bpl.IdentifierExprSeq outs = new Bpl.IdentifierExprSeq();

           if (!defn.IsStatic)

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 4d13d638..02a173b9 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -966,18 +966,22 @@ namespace BytecodeTranslator {
     }

     private IAssembly/*?*/ assemblyBeingTranslated;

 

-    public Dictionary<ITypeDefinition, HashSet<IMethodDefinition>> delegateTypeToDelegates = new Dictionary<ITypeDefinition, HashSet<IMethodDefinition>>();

+    public Dictionary<uint, Tuple<ITypeDefinition, HashSet<IMethodDefinition>>> delegateTypeToDelegates = 

+      new Dictionary<uint, Tuple<ITypeDefinition, HashSet<IMethodDefinition>>>();

 

     public void AddDelegate(ITypeDefinition type, IMethodDefinition defn)

     {

-      if (!delegateTypeToDelegates.ContainsKey(type))

-        delegateTypeToDelegates[type] = new HashSet<IMethodDefinition>();

-      delegateTypeToDelegates[type].Add(defn);

+      uint key = type.InternedKey;

+      if (!delegateTypeToDelegates.ContainsKey(key))

+        delegateTypeToDelegates[key] = new Tuple<ITypeDefinition, HashSet<IMethodDefinition>>(type, new HashSet<IMethodDefinition>());

+      FindOrCreateProcedure(defn);

+      delegateTypeToDelegates[key].Item2.Add(defn);

     }

 

     public void AddDelegateType(ITypeDefinition type) {

-      if (!delegateTypeToDelegates.ContainsKey(type))

-        delegateTypeToDelegates[type] = new HashSet<IMethodDefinition>();

+      uint key = type.InternedKey;

+      if (!delegateTypeToDelegates.ContainsKey(key))

+        delegateTypeToDelegates[key] = new Tuple<ITypeDefinition, HashSet<IMethodDefinition>>(type, new HashSet<IMethodDefinition>());

     }

 

     private Dictionary<IMethodDefinition, Bpl.Constant> delegateMethods = new Dictionary<IMethodDefinition, Bpl.Constant>();

diff --git a/BCT/BytecodeTranslator/StatementTraverser.cs b/BCT/BytecodeTranslator/StatementTraverser.cs
index c7b94f1a..09b0b13b 100644
--- a/BCT/BytecodeTranslator/StatementTraverser.cs
+++ b/BCT/BytecodeTranslator/StatementTraverser.cs
@@ -148,15 +148,33 @@ namespace BytecodeTranslator
     #region Basic Statements

 

     public override void Visit(IAssertStatement assertStatement) {

-      StmtBuilder.Add(

-        new Bpl.AssertCmd(assertStatement.Token(), ExpressionFor(assertStatement.Condition))

-        );

+      Bpl.Expr conditionExpr = ExpressionFor(assertStatement.Condition);

+      Bpl.Type conditionType = this.sink.CciTypeToBoogie(assertStatement.Condition.Type);

+      if (conditionType == this.sink.Heap.RefType) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      }

+      else if (conditionType == Bpl.Type.Int) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Literal(0));

+      }

+      else {

+        System.Diagnostics.Debug.Assert(conditionType == Bpl.Type.Bool);

+      }

+      StmtBuilder.Add(new Bpl.AssertCmd(assertStatement.Token(), conditionExpr));

     }

 

     public override void Visit(IAssumeStatement assumeStatement) {

-      StmtBuilder.Add(

-        new Bpl.AssumeCmd(assumeStatement.Token(), ExpressionFor(assumeStatement.Condition))

-        );

+      Bpl.Expr conditionExpr = ExpressionFor(assumeStatement.Condition);

+      Bpl.Type conditionType = this.sink.CciTypeToBoogie(assumeStatement.Condition.Type);

+      if (conditionType == this.sink.Heap.RefType) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      }

+      else if (conditionType == Bpl.Type.Int) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Literal(0));

+      }

+      else {

+        System.Diagnostics.Debug.Assert(conditionType == Bpl.Type.Bool);

+      }

+      StmtBuilder.Add(new Bpl.AssumeCmd(assumeStatement.Token(), conditionExpr));

     }

 

     /// <summary>

@@ -173,8 +191,20 @@ namespace BytecodeTranslator
       thenTraverser.Visit(conditionalStatement.TrueBranch);

       elseTraverser.Visit(conditionalStatement.FalseBranch);

 

+      Bpl.Expr conditionExpr = condTraverser.TranslatedExpressions.Pop();

+      Bpl.Type conditionType = this.sink.CciTypeToBoogie(conditionalStatement.Condition.Type);

+      if (conditionType == this.sink.Heap.RefType) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Ident(this.sink.Heap.NullRef));

+      }

+      else if (conditionType == Bpl.Type.Int) {

+        conditionExpr = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, conditionExpr, Bpl.Expr.Literal(0));

+      }

+      else {

+        System.Diagnostics.Debug.Assert(conditionType == Bpl.Type.Bool);

+      }

+

       Bpl.IfCmd ifcmd = new Bpl.IfCmd(conditionalStatement.Token(),

-          condTraverser.TranslatedExpressions.Pop(),

+          conditionExpr,

           thenTraverser.StmtBuilder.Collect(conditionalStatement.TrueBranch.Token()),

           null,

           elseTraverser.StmtBuilder.Collect(conditionalStatement.FalseBranch.Token())

diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index dd57d72f..726a1ea6 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -150,6 +150,9 @@ namespace BytecodeTranslator {
       s = s.Replace('%', '$');

       s = s.Replace('&', '$');

       s = s.Replace('"', '$');

+      s = s.Replace('[', '$');

+      s = s.Replace(']', '$');

+      s = s.Replace('|', '$');

       return s;

     }