More support for reals, especially real constants.

3 files changed, 54 insertions, 18 deletions

diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index 0670efbe..87afde39 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -374,10 +374,8 @@ namespace BytecodeTranslator
 

     #region Translate Constant Access

 

-    public override void Visit(ICompileTimeConstant constant)

-    {

-      if (constant.Value == null)

-      {

+    public override void Visit(ICompileTimeConstant constant) {

+      if (constant.Value == null) {

         var bplType = sink.CciTypeToBoogie(constant.Type);

         if (bplType == Bpl.Type.Int) {

           var lit = Bpl.Expr.Literal(0);

@@ -390,23 +388,35 @@ namespace BytecodeTranslator
         } else {

           throw new NotImplementedException(String.Format("Don't know how to translate type: '{0}'", TypeHelper.GetTypeName(constant.Type)));

         }

-     }

-      else if (constant.Value is bool)

-      {

-        TranslatedExpressions.Push(((bool)constant.Value) ? Bpl.Expr.True : Bpl.Expr.False);

+        return;

       }

-      else if (constant.Value is string)

-      {

+      if (constant.Value is string) {

         var c = this.sink.FindOrCreateConstant((string)(constant.Value));

         TranslatedExpressions.Push(Bpl.Expr.Ident(c));

-

-        //throw new NotImplementedException("Strings are not translated");

-      } else {

-        // TODO: (mschaef) hack

-        var lit = Bpl.Expr.Literal((int)constant.Value);

-        lit.Type = Bpl.Type.Int;

-        TranslatedExpressions.Push(lit);

+        return;

       }

+      switch (constant.Type.TypeCode) {

+        case PrimitiveTypeCode.Boolean:

+          TranslatedExpressions.Push(((bool)constant.Value) ? Bpl.Expr.True : Bpl.Expr.False);

+          break;

+        case PrimitiveTypeCode.Char: // chars are represented as ints

+        case PrimitiveTypeCode.Int16:

+        case PrimitiveTypeCode.Int32:

+        case PrimitiveTypeCode.Int64:

+        case PrimitiveTypeCode.Int8:

+          var lit = Bpl.Expr.Literal((int)constant.Value);

+          lit.Type = Bpl.Type.Int;

+          TranslatedExpressions.Push(lit);

+          break;

+        case PrimitiveTypeCode.Float32:

+        case PrimitiveTypeCode.Float64:

+          var c = this.sink.FindOrCreateConstant((double)(constant.Value));

+          TranslatedExpressions.Push(Bpl.Expr.Ident(c));

+          return;

+        default:

+          throw new NotImplementedException();

+      }

+      return;

     }

 

     public override void Visit(IDefaultValue defaultValue) {

@@ -460,7 +470,7 @@ namespace BytecodeTranslator
         this.indexExpr = savedIndexExpr;

 

         var e = this.TranslatedExpressions.Pop();

-        if (methodCall.MethodToCall.ContainingType.IsValueType)

+        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

diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 9e1fa296..812fddb1 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -130,6 +130,9 @@ namespace BytecodeTranslator {
     [RepresentationFor("Box2Ref", "function Box2Ref(Box): Ref;")]

     public Bpl.Function Box2Ref = null;

 

+    [RepresentationFor("Box2Real", "function Box2Real(Box): Real;")]

+    public Bpl.Function Box2Real = null;

+

     [RepresentationFor("Int2Box", "function Int2Box(int): Box;")]

     public Bpl.Function Int2Box = null;

 

@@ -142,6 +145,9 @@ namespace BytecodeTranslator {
     [RepresentationFor("Ref2Box", "function Ref2Box(Ref): Box;")]

     public Bpl.Function Ref2Box = null;

 

+    [RepresentationFor("Real2Box", "function Real2Box(Real): Box;")]

+    public Bpl.Function Real2Box = null;

+

     public Bpl.Expr Box(Bpl.IToken tok, Bpl.Type boogieType, Bpl.Expr expr) {

       Bpl.Function conversion;

       if (boogieType == Bpl.Type.Bool)

@@ -152,6 +158,8 @@ namespace BytecodeTranslator {
         conversion = this.Struct2Box;

       else if (boogieType == RefType)

         conversion = this.Ref2Box;

+      else if (boogieType == RealType)

+        conversion = this.Real2Box;

       else

         throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

@@ -173,6 +181,8 @@ namespace BytecodeTranslator {
         conversion = this.Box2Struct;

       else if (boogieType == RefType)

         conversion = this.Box2Ref;

+      else if (boogieType == RealType)

+        conversion = this.Box2Real;

       else

         throw new InvalidOperationException(String.Format("Unknown Boogie type: '{0}'", boogieType.ToString()));

 

diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index 8e163c4f..2bf3b7d3 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -232,6 +232,22 @@ namespace BytecodeTranslator {
     }

     private Dictionary<string, Bpl.Constant> declaredStringConstants = new Dictionary<string, Bpl.Constant>();

 

+    public Bpl.Constant FindOrCreateConstant(double d) {

+      Bpl.Constant c;

+      var str = d.ToString();

+      if (!this.declaredRealConstants.TryGetValue(str, out c)) {

+        var tok = Bpl.Token.NoToken;

+        var t = Heap.RealType;

+        var name = "$real_literal_" + TranslationHelper.TurnStringIntoValidIdentifier(str) + "_" + declaredStringConstants.Count;

+        var tident = new Bpl.TypedIdent(tok, name, t);

+        c = new Bpl.Constant(tok, tident, true);

+        this.declaredRealConstants.Add(str, c);

+        this.TranslatedProgram.TopLevelDeclarations.Add(c);

+      }

+      return c;

+    }

+    private Dictionary<string, Bpl.Constant> declaredRealConstants = new Dictionary<string, Bpl.Constant>();

+

     private Dictionary<IPropertyDefinition, Bpl.Variable> declaredProperties = new Dictionary<IPropertyDefinition, Bpl.Variable>();

 

     private List<Bpl.Function> projectionFunctions = new List<Bpl.Function>();