summaryrefslogtreecommitdiff
path: root/BCT/BytecodeTranslator
diff options
context:
space:
mode:
Diffstat (limited to 'BCT/BytecodeTranslator')
-rw-r--r--BCT/BytecodeTranslator/ExpressionTraverser.cs101
-rw-r--r--BCT/BytecodeTranslator/HeapFactory.cs11
-rw-r--r--BCT/BytecodeTranslator/MetadataTraverser.cs15
-rw-r--r--BCT/BytecodeTranslator/Sink.cs19
-rw-r--r--BCT/BytecodeTranslator/TranslationHelper.cs2
5 files changed, 137 insertions, 11 deletions
diff --git a/BCT/BytecodeTranslator/ExpressionTraverser.cs b/BCT/BytecodeTranslator/ExpressionTraverser.cs
index ccd3f748..123280ed 100644
--- a/BCT/BytecodeTranslator/ExpressionTraverser.cs
+++ b/BCT/BytecodeTranslator/ExpressionTraverser.cs
@@ -349,11 +349,16 @@ namespace BytecodeTranslator
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;
+ case PrimitiveTypeCode.Float32: {
+ var c = this.sink.FindOrCreateConstant((float)(constant.Value));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(c));
+ return;
+ }
+ case PrimitiveTypeCode.Float64: {
+ var c = this.sink.FindOrCreateConstant((double)(constant.Value));
+ TranslatedExpressions.Push(Bpl.Expr.Ident(c));
+ return;
+ }
case PrimitiveTypeCode.NotPrimitive:
if (constant.Type.IsEnum) {
lit = Bpl.Expr.Literal((int)constant.Value);
@@ -902,7 +907,37 @@ namespace BytecodeTranslator
base.Visit(addition);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Add, lexp, rexp));
+ Bpl.Expr e;
+ switch (addition.Type.TypeCode) {
+ case PrimitiveTypeCode.Float32:
+ case PrimitiveTypeCode.Float64:
+ e = new Bpl.NAryExpr(
+ addition.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.RealPlus),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ break;
+ default:
+ e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Add, lexp, rexp);
+ break;
+ }
+ TranslatedExpressions.Push(e);
+ }
+
+ // TODO: Encode this correctly!
+ public override void Visit(IBitwiseAnd bitwiseAnd) {
+ base.Visit(bitwiseAnd);
+ Bpl.Expr rexp = TranslatedExpressions.Pop();
+ Bpl.Expr lexp = TranslatedExpressions.Pop();
+ TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.And, lexp, rexp));
+ }
+
+ // TODO: Encode this correctly!
+ public override void Visit(IBitwiseOr bitwiseOr) {
+ base.Visit(bitwiseOr);
+ Bpl.Expr rexp = TranslatedExpressions.Pop();
+ Bpl.Expr lexp = TranslatedExpressions.Pop();
+ TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Or, lexp, rexp));
}
public override void Visit(IDivision division)
@@ -910,7 +945,21 @@ namespace BytecodeTranslator
base.Visit(division);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, rexp));
+ Bpl.Expr e;
+ switch (division.Type.TypeCode) {
+ case PrimitiveTypeCode.Float32:
+ case PrimitiveTypeCode.Float64:
+ e = new Bpl.NAryExpr(
+ division.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.RealDivide),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ break;
+ default:
+ e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Div, lexp, rexp);
+ break;
+ }
+ TranslatedExpressions.Push(e);
}
// TODO: Encode this correctly!
@@ -926,7 +975,21 @@ namespace BytecodeTranslator
base.Visit(subtraction);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, lexp, rexp));
+ Bpl.Expr e;
+ switch (subtraction.Type.TypeCode) {
+ case PrimitiveTypeCode.Float32:
+ case PrimitiveTypeCode.Float64:
+ e = new Bpl.NAryExpr(
+ subtraction.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.RealMinus),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ break;
+ default:
+ e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Sub, lexp, rexp);
+ break;
+ }
+ TranslatedExpressions.Push(e);
}
public override void Visit(IMultiplication multiplication)
@@ -934,7 +997,21 @@ namespace BytecodeTranslator
base.Visit(multiplication);
Bpl.Expr rexp = TranslatedExpressions.Pop();
Bpl.Expr lexp = TranslatedExpressions.Pop();
- TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Mul, lexp, rexp));
+ Bpl.Expr e;
+ switch (multiplication.Type.TypeCode) {
+ case PrimitiveTypeCode.Float32:
+ case PrimitiveTypeCode.Float64:
+ e = new Bpl.NAryExpr(
+ multiplication.Token(),
+ new Bpl.FunctionCall(this.sink.Heap.RealTimes),
+ new Bpl.ExprSeq(lexp, rexp)
+ );
+ break;
+ default:
+ e = Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Mul, lexp, rexp);
+ break;
+ }
+ TranslatedExpressions.Push(e);
}
public override void Visit(IModulus modulus)
@@ -1152,6 +1229,12 @@ namespace BytecodeTranslator
default:
throw new NotImplementedException(msg);
}
+ case PrimitiveTypeCode.UIntPtr:
+ case PrimitiveTypeCode.IntPtr:
+ // just ignore the conversion. REVIEW: is that the right thing to do?
+ this.TranslatedExpressions.Push(exp);
+ return;
+
case PrimitiveTypeCode.Boolean:
if (TypeHelper.IsPrimitiveInteger(conversion.ValueToConvert.Type)) {
TranslatedExpressions.Push(Bpl.Expr.Binary(Bpl.BinaryOperator.Opcode.Neq, exp, Bpl.Expr.Literal(0)));
diff --git a/BCT/BytecodeTranslator/HeapFactory.cs b/BCT/BytecodeTranslator/HeapFactory.cs
index 3dc1b5f9..0b2dd6cf 100644
--- a/BCT/BytecodeTranslator/HeapFactory.cs
+++ b/BCT/BytecodeTranslator/HeapFactory.cs
@@ -229,6 +229,17 @@ namespace BytecodeTranslator {
public Bpl.Function Real2Ref = null;
#endregion
+ #region Real number operations
+ [RepresentationFor("RealPlus", "function RealPlus(Real, Real): Real;")]
+ public Bpl.Function RealPlus = null;
+ [RepresentationFor("RealMinus", "function RealMinus(Real, Real): Real;")]
+ public Bpl.Function RealMinus = null;
+ [RepresentationFor("RealTimes", "function RealTimes(Real, Real): Real;")]
+ public Bpl.Function RealTimes = null;
+ [RepresentationFor("RealDivide", "function RealDivide(Real, Real): Real;")]
+ public Bpl.Function RealDivide = null;
+ #endregion
+
#region Ref conversions
[RepresentationFor("Ref2Int", "function Ref2Int(Ref, Type, Type): int;")]
public Bpl.Function Ref2Int = null;
diff --git a/BCT/BytecodeTranslator/MetadataTraverser.cs b/BCT/BytecodeTranslator/MetadataTraverser.cs
index 18b8e0e6..1cad1a36 100644
--- a/BCT/BytecodeTranslator/MetadataTraverser.cs
+++ b/BCT/BytecodeTranslator/MetadataTraverser.cs
@@ -396,7 +396,20 @@ namespace BytecodeTranslator {
} else { // method is translated as a function
//var func = decl as Bpl.Function;
//Contract.Assume(func != null);
- //func.Body = new Bpl.CodeExpr(new Bpl.VariableSeq(), translatedBody.BigBlocks);
+ //var blocks = new List<Bpl.Block>();
+ //var counter = 0;
+ //var returnValue = decl.OutParams[0];
+ //foreach (var bb in translatedBody.BigBlocks) {
+ // var label = bb.LabelName ?? "L" + counter++.ToString();
+ // var newTransferCmd = (bb.tc is Bpl.ReturnCmd)
+ // ? new Bpl.ReturnExprCmd(bb.tc.tok, Bpl.Expr.Ident(returnValue))
+ // : bb.tc;
+ // var b = new Bpl.Block(bb.tok, label, bb.simpleCmds, newTransferCmd);
+ // blocks.Add(b);
+ //}
+ //var localVars = new Bpl.VariableSeq();
+ //localVars.Add(returnValue);
+ //func.Body = new Bpl.CodeExpr(localVars, blocks);
}
#endregion
diff --git a/BCT/BytecodeTranslator/Sink.cs b/BCT/BytecodeTranslator/Sink.cs
index bc28d9be..127317e9 100644
--- a/BCT/BytecodeTranslator/Sink.cs
+++ b/BCT/BytecodeTranslator/Sink.cs
@@ -251,6 +251,20 @@ namespace BytecodeTranslator {
}
return c;
}
+ public Bpl.Constant FindOrCreateConstant(float f) {
+ Bpl.Constant c;
+ var str = f.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>();
@@ -431,7 +445,7 @@ namespace BytecodeTranslator {
// Can't visit the method's contracts until the formalMap and procedure are added to the
// table because information in them might be needed (e.g., if a parameter is mentioned
// in a contract.
- #region Check The Method Contracts
+ #region Translate the method's contracts
var possiblyUnspecializedMethod = Unspecialize(method);
@@ -586,6 +600,9 @@ namespace BytecodeTranslator {
// also, should it return true for properties and all of the other things the tools
// consider pure?
private bool IsPure(IMethodDefinition method) {
+ bool isPropertyGetter = method.IsSpecialName && method.Name.Value.StartsWith("get_");
+ if (isPropertyGetter) return true;
+
foreach (var a in method.Attributes) {
if (TypeHelper.GetTypeName(a.Type).EndsWith("PureAttribute")) {
return true;
diff --git a/BCT/BytecodeTranslator/TranslationHelper.cs b/BCT/BytecodeTranslator/TranslationHelper.cs
index d554d83e..cf856024 100644
--- a/BCT/BytecodeTranslator/TranslationHelper.cs
+++ b/BCT/BytecodeTranslator/TranslationHelper.cs
@@ -111,6 +111,7 @@ namespace BytecodeTranslator {
s = s.Replace('-', '$');
s = s.Replace(' ', '$');
s = s.Replace('\t', '$');
+ s = s.Replace('\r', '$');
s = s.Replace('\n', '$');
s = s.Replace('/', '$');
s = s.Replace('\\', '$');
@@ -119,6 +120,7 @@ namespace BytecodeTranslator {
s = s.Replace(';', '$');
s = s.Replace('%', '$');
s = s.Replace('&', '$');
+ s = s.Replace('"', '$');
return s;
}
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 03:34:33 +0000