diff options
| -rw-r--r-- | Source/Core/BitvectorAnalysis.cs | 288 | ||||
| -rw-r--r-- | Source/Core/StandardVisitor.cs | 2 |
2 files changed, 274 insertions, 16 deletions
diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs index 4b6a32e8..8dc80345 100644 --- a/Source/Core/BitvectorAnalysis.cs +++ b/Source/Core/BitvectorAnalysis.cs @@ -95,13 +95,30 @@ namespace Microsoft.Boogie { private Dictionary<Expr, DisjointSet> exprToDisjointSet = new Dictionary<Expr, DisjointSet>();
private Dictionary<Variable, DisjointSet> varToDisjointSet = new Dictionary<Variable, DisjointSet>();
- private DisjointSet uniqueBvSet = new DisjointSet();
+ private DisjointSet uniqueBv8Set = new DisjointSet();
+ private DisjointSet uniqueBv16Set = new DisjointSet();
+ private DisjointSet uniqueBv32Set = new DisjointSet();
+ private DisjointSet uniqueBv64Set = new DisjointSet();
+
+ public int Bits(Expr expr) {
+ DisjointSet disjointSet = MakeDisjointSet(expr);
+ if (disjointSet.Find() == uniqueBv8Set.Find())
+ return 8;
+ if (disjointSet.Find() == uniqueBv16Set.Find())
+ return 16;
+ if (disjointSet.Find() == uniqueBv32Set.Find())
+ return 32;
+ if (disjointSet.Find() == uniqueBv64Set.Find())
+ return 64;
+ return 0;
+ }
public Type NewType(Variable var) {
DisjointSet disjointSet = MakeDisjointSet(var);
return NewType(var.TypedIdent.Type, disjointSet);
}
+ /*
private bool Test(DisjointSet disjointSet) {
DisjointSet bvRoot = uniqueBvSet.Find();
if (disjointSet == null)
@@ -110,16 +127,25 @@ namespace Microsoft.Boogie { return false;
return true;
}
+ */
+
+ private Type Test(Type type, DisjointSet disjointSet) {
+ if (disjointSet.Find() == uniqueBv8Set.Find())
+ return new BvType(8);
+ if (disjointSet.Find() == uniqueBv16Set.Find())
+ return new BvType(16);
+ if (disjointSet.Find() == uniqueBv32Set.Find())
+ return new BvType(32);
+ if (disjointSet.Find() == uniqueBv64Set.Find())
+ return new BvType(64);
+
+ return type;
+ }
private Type NewType(Type type, DisjointSet disjointSet) {
MapType mapType = type as MapType;
if (mapType == null) {
- if (type is BvType && Test(disjointSet)) {
- return Type.Int;
- }
- else {
- return type;
- }
+ return Test(type, disjointSet);
}
else {
MapDisjointSet mapDisjointSet = disjointSet as MapDisjointSet;
@@ -128,13 +154,8 @@ namespace Microsoft.Boogie { Type result = NewType(mapType.Result, mapDisjointSet.Result);
bool newTypeNeeded = (result != mapType.Result);
for (int i = 0; i < mapType.Arguments.Length; i++) {
- if (mapType.Arguments[i] is BvType && Test(mapDisjointSet.Args(i))) {
- newArguments.Add(Type.Int);
- newTypeNeeded = true;
- }
- else {
- newArguments.Add(mapType.Arguments[i]);
- }
+ newArguments.Add(Test(mapType.Arguments[i], mapDisjointSet.Args(i)));
+ newTypeNeeded = newTypeNeeded || (newArguments[i] != mapType.Arguments[i]);
}
if (newTypeNeeded) {
return new MapType(mapType.tok, mapType.TypeParameters, newArguments, result);
@@ -174,10 +195,21 @@ namespace Microsoft.Boogie { }
public static void DoBitVectorAnalysis(Program program) {
+ DuplicateLiteralExpr duplicateLiteralExpr = new DuplicateLiteralExpr();
+ duplicateLiteralExpr.Visit(program);
+
BitVectorAnalysis bvAnalyzer = new BitVectorAnalysis();
bvAnalyzer.Visit(program);
+ /*
BvToIntRewriter bvtoIntRewriter = new BvToIntRewriter(bvAnalyzer);
bvtoIntRewriter.Visit(program);
+ */
+ IntToBvRewriter intToBvRewriter = new IntToBvRewriter(program, bvAnalyzer);
+ intToBvRewriter.Visit(program);
+ program.TopLevelDeclarations.Add(intToBvRewriter.bv8Id);
+ program.TopLevelDeclarations.Add(intToBvRewriter.bv16Id);
+ program.TopLevelDeclarations.Add(intToBvRewriter.bv32Id);
+ program.TopLevelDeclarations.Add(intToBvRewriter.bv64Id);
}
public override Implementation VisitImplementation(Implementation node) {
@@ -227,6 +259,108 @@ namespace Microsoft.Boogie { BinaryOperator op = node.Fun as BinaryOperator;
if (op != null) {
Debug.Assert(node.Args.Length == 2);
+ MakeDisjointSet(node.Args[0]).Union(MakeDisjointSet(node.Args[1]));
+ }
+
+ FunctionCall fcall = node.Fun as FunctionCall;
+ if (fcall != null) {
+ Function func = fcall.Func;
+
+ // unify each actual argument with corresponding formal argument
+ for (int i = 0; i < node.Args.Length; i++) {
+ DisjointSet actual = MakeDisjointSet(node.Args[i]);
+ DisjointSet formal = MakeDisjointSet(func.InParams[i]);
+ actual.Union(formal);
+ }
+ Debug.Assert(func.OutParams.Length == 1);
+ MakeDisjointSet(node).Union(MakeDisjointSet(func.OutParams[0]));
+
+ if (func.Name == "intToBv8") {
+ Debug.Assert(node.Args.Length == 1);
+ Expr e = node.Args[0];
+ DisjointSet actual = MakeDisjointSet(e);
+ actual.Union(uniqueBv8Set);
+ }
+
+ if (func.Name == "intToBv16") {
+ Debug.Assert(node.Args.Length == 1);
+ Expr e = node.Args[0];
+ DisjointSet actual = MakeDisjointSet(e);
+ actual.Union(uniqueBv16Set);
+ }
+
+ if (func.Name == "intToBv32") {
+ Debug.Assert(node.Args.Length == 1);
+ Expr e = node.Args[0];
+ DisjointSet actual = MakeDisjointSet(e);
+ actual.Union(uniqueBv32Set);
+ }
+
+ if (func.Name == "intToBv64") {
+ Debug.Assert(node.Args.Length == 1);
+ Expr e = node.Args[0];
+ DisjointSet actual = MakeDisjointSet(e);
+ actual.Union(uniqueBv64Set);
+ }
+
+ if (func.Name == "bv8ToInt") {
+ Debug.Assert(node.Args.Length == 1);
+ DisjointSet actual = MakeDisjointSet(node);
+ actual.Union(uniqueBv8Set);
+ }
+
+ if (func.Name == "bv16ToInt") {
+ Debug.Assert(node.Args.Length == 1);
+ DisjointSet actual = MakeDisjointSet(node);
+ actual.Union(uniqueBv16Set);
+ }
+
+ if (func.Name == "bv32ToInt") {
+ Debug.Assert(node.Args.Length == 1);
+ DisjointSet actual = MakeDisjointSet(node);
+ actual.Union(uniqueBv32Set);
+ }
+
+ if (func.Name == "bv64ToInt") {
+ Debug.Assert(node.Args.Length == 1);
+ DisjointSet actual = MakeDisjointSet(node);
+ actual.Union(uniqueBv64Set);
+ }
+ }
+
+ MapSelect select = node.Fun as MapSelect;
+ if (select != null) {
+ int i = 0;
+ MapDisjointSet mapDisjointSet = (MapDisjointSet)MakeDisjointSet(node.Args[i]);
+ i++;
+ DisjointSet[] args = new DisjointSet[node.Args.Length - 1];
+ for (; i < node.Args.Length; i++) {
+ args[i - 1] = MakeDisjointSet(node.Args[i]);
+ }
+ mapDisjointSet.Union(new MapDisjointSet(args, MakeDisjointSet(node)));
+ }
+
+ MapStore store = node.Fun as MapStore;
+ if (store != null) {
+ int i = 0;
+ MapDisjointSet mapDisjointSet = (MapDisjointSet)MakeDisjointSet(node.Args[i]);
+ i++;
+ DisjointSet[] args = new DisjointSet[node.Args.Length - 2];
+ for (; i < node.Args.Length - 1; i++) {
+ args[i - 1] = MakeDisjointSet(node.Args[i]);
+ }
+ mapDisjointSet.Union(new MapDisjointSet(args, MakeDisjointSet(node.Args[i])));
+ mapDisjointSet.Union(MakeDisjointSet(node));
+ }
+
+ return base.VisitNAryExpr(node);
+ }
+
+ /*
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ BinaryOperator op = node.Fun as BinaryOperator;
+ if (op != null) {
+ Debug.Assert(node.Args.Length == 2);
if (op.Op == BinaryOperator.Opcode.Eq || op.Op == BinaryOperator.Opcode.Neq) {
MakeDisjointSet(node.Args[0]).Union(MakeDisjointSet(node.Args[1]));
}
@@ -281,7 +415,7 @@ namespace Microsoft.Boogie { return base.VisitNAryExpr(node);
}
-
+
public override BvConcatExpr VisitBvConcatExpr(BvConcatExpr node) {
foreach (Expr e in node.Arguments) {
DisjointSet actual = MakeDisjointSet(e);
@@ -303,6 +437,7 @@ namespace Microsoft.Boogie { }
return base.VisitLiteralExpr(node);
}
+ */
public override Expr VisitIdentifierExpr(IdentifierExpr node) {
DisjointSet a = MakeDisjointSet(node);
@@ -312,6 +447,7 @@ namespace Microsoft.Boogie { }
}
+ /*
class BvToIntRewriter : StandardVisitor {
private BitVectorAnalysis bvAnalyzer;
public BvToIntRewriter(BitVectorAnalysis bvAnalyzer) {
@@ -341,4 +477,126 @@ namespace Microsoft.Boogie { return node;
}
}
+ */
+
+ class MyLiteralExpr : LiteralExpr {
+ public MyLiteralExpr(IToken tok, bool b) : base(tok, b) { }
+ public MyLiteralExpr(IToken tok, Basetypes.BigNum v) : base(tok, v) { }
+ public MyLiteralExpr(IToken tok, Basetypes.BigNum v, int b) : base(tok, v, b) { }
+ public override bool Equals(object obj) {
+ return this == obj;
+ }
+ public override int GetHashCode() {
+ return base.GetHashCode();
+ }
+ }
+
+ class DuplicateLiteralExpr : StandardVisitor {
+ public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ LiteralExpr litExpr;
+ if (node.Val is bool) {
+ litExpr = new MyLiteralExpr(Token.NoToken, (bool)node.Val);
+ } else if (node.Val is Basetypes.BigNum) {
+ litExpr = new MyLiteralExpr(Token.NoToken, (Basetypes.BigNum)node.Val);
+ } else {
+ BvConst bvconst = (BvConst) node.Val;
+ litExpr = new MyLiteralExpr(Token.NoToken, bvconst.Value, bvconst.Bits);
+ }
+ litExpr.Typecheck(new TypecheckingContext(null));
+ return litExpr;
+ }
+ }
+
+ class IntToBvRewriter : StandardVisitor {
+ private BitVectorAnalysis bvAnalyzer;
+ public Function bv8Id;
+ public Function bv16Id;
+ public Function bv32Id;
+ public Function bv64Id;
+
+ public IntToBvRewriter(Program program, BitVectorAnalysis bvAnalyzer) {
+ this.bvAnalyzer = bvAnalyzer;
+
+ BvType bv8Type = new BvType(8);
+ VariableSeq bv8In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv8Type), true));
+ Formal bv8Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv8Type), false);
+ bv8Id = new Function(Token.NoToken, "bv8Id", bv8In, bv8Out);
+ bv8Id.Body = new IdentifierExpr(Token.NoToken, bv8In[0]);
+ bv8Id.AddAttribute("inline");
+
+ BvType bv16Type = new BvType(16);
+ VariableSeq bv16In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv16Type), true));
+ Formal bv16Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv16Type), false);
+ bv16Id = new Function(Token.NoToken, "bv16Id", bv16In, bv16Out);
+ bv16Id.Body = new IdentifierExpr(Token.NoToken, bv16In[0]);
+ bv16Id.AddAttribute("inline");
+
+ BvType bv32Type = new BvType(32);
+ VariableSeq bv32In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv32Type), true));
+ Formal bv32Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv32Type), false);
+ bv32Id = new Function(Token.NoToken, "bv32Id", bv32In, bv32Out);
+ bv32Id.Body = new IdentifierExpr(Token.NoToken, bv32In[0]);
+ bv32Id.AddAttribute("inline");
+
+ BvType bv64Type = new BvType(64);
+ VariableSeq bv64In = new VariableSeq(new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "in", bv64Type), true));
+ Formal bv64Out = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, "out", bv64Type), false);
+ bv64Id = new Function(Token.NoToken, "bv64Id", bv64In, bv64Out);
+ bv64Id.Body = new IdentifierExpr(Token.NoToken, bv64In[0]);
+ bv64Id.AddAttribute("inline");
+ }
+
+ public override Constant VisitConstant(Constant node) {
+ node.TypedIdent.Type = bvAnalyzer.NewType(node);
+ return node;
+ }
+
+ public override Variable VisitVariable(Variable node) {
+ node.TypedIdent.Type = bvAnalyzer.NewType(node);
+ return node;
+ }
+
+ public override Implementation VisitImplementation(Implementation node) {
+ this.VisitVariableSeq(node.LocVars);
+ this.VisitVariableSeq(node.InParams);
+ this.VisitVariableSeq(node.OutParams);
+ return base.VisitImplementation(node);
+ }
+
+ public override Procedure VisitProcedure(Procedure node) {
+ this.VisitVariableSeq(node.InParams);
+ this.VisitVariableSeq(node.OutParams);
+ return node;
+ }
+
+ public override Expr VisitNAryExpr(NAryExpr node) {
+ FunctionCall fcall = node.Fun as FunctionCall;
+ if (fcall != null) {
+ Function func = fcall.Func;
+ if (func.Name == "intToBv8" || func.Name == "bv8ToInt") {
+ node.Fun = new FunctionCall(bv8Id);
+ }
+ if (func.Name == "intToBv16" || func.Name == "bv16ToInt") {
+ node.Fun = new FunctionCall(bv16Id);
+ }
+ if (func.Name == "intToBv32" || func.Name == "bv32ToInt") {
+ node.Fun = new FunctionCall(bv32Id);
+ }
+ if (func.Name == "intToBv64" || func.Name == "bv64ToInt") {
+ node.Fun = new FunctionCall(bv64Id);
+ }
+ }
+ return base.VisitNAryExpr(node);
+ }
+
+ public override LiteralExpr VisitLiteralExpr(LiteralExpr node) {
+ int numBits = bvAnalyzer.Bits(node);
+ if (numBits > 0 && node.Val is Basetypes.BigNum) {
+ return new LiteralExpr(Token.NoToken, (Basetypes.BigNum)node.Val, numBits);
+ }
+ else {
+ return node;
+ }
+ }
+ }
}
diff --git a/Source/Core/StandardVisitor.cs b/Source/Core/StandardVisitor.cs index 528e442f..9bbeada1 100644 --- a/Source/Core/StandardVisitor.cs +++ b/Source/Core/StandardVisitor.cs @@ -48,7 +48,7 @@ namespace Microsoft.Boogie { }
/// <summary>
- /// Walks an IR, mutuating it into a new form
+ /// Walks an IR, mutating it into a new form
/// </summary>
public abstract class StandardVisitor : Visitor {
public Visitor callingVisitor;
|