diff options
| author |  Ally Donaldson <unknown> | 2013-12-09 09:49:06 +0000 |
|---|---|---|
| committer | Ally Donaldson <unknown> | 2013-12-09 09:49:06 +0000 |
| commit | d7bf93bf834d9856de385de7c2d980aaf09802ca (patch) | |
| tree | 8410342d9d7da2c6e3d3b4b6b8abc1b4ea983980 | |
| parent | c44eeb0c3120f6bd9d377019e96ea11508252806 (diff) | |
| parent | 8c029eac9244b10bf0bdf3451d91af74f0acc419 (diff) | |
Merge
| -rw-r--r-- | Binaries/UnivBackPred2.smt | 131 | ||||
| -rw-r--r-- | Binaries/UnivBackPred2.smt2 | 8 | ||||
| -rw-r--r-- | Source/BoogieDriver/BoogieDriver.csproj | 6 | ||||
| -rw-r--r-- | Source/Concurrency/YieldTypeChecker.cs | 560 | ||||
| -rw-r--r-- | Source/Core/BitvectorAnalysis.cs | 585 | ||||
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 9 | ||||
| -rw-r--r-- | Source/Core/Core.csproj | 5 | ||||
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 53 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 18 |
9 files changed, 355 insertions, 1020 deletions
diff --git a/Binaries/UnivBackPred2.smt b/Binaries/UnivBackPred2.smt deleted file mode 100644 index 76c77d60..00000000 --- a/Binaries/UnivBackPred2.smt +++ /dev/null @@ -1,131 +0,0 @@ -; -------------------------------------------------------------------------
-; Boogie universal background predicate
-; Copyright (c) 2004-2006, Microsoft Corp.
- :logic AUFLIA
- :category { industrial }
-
-:extrasorts ( boogieU )
-:extrasorts ( boogieT )
-:extrasorts ( TermBool )
-
-:extrafuns (( boolTrue TermBool ))
-:extrafuns (( boolFalse TermBool ))
-:extrafuns (( boolIff TermBool TermBool TermBool ))
-:extrafuns (( boolImplies TermBool TermBool TermBool ))
-:extrafuns (( boolAnd TermBool TermBool TermBool ))
-:extrafuns (( boolOr TermBool TermBool TermBool ))
-:extrafuns (( boolNot TermBool TermBool ))
-:extrafuns (( UEqual boogieU boogieU TermBool ))
-:extrafuns (( TEqual boogieT boogieT TermBool ))
-:extrafuns (( IntEqual Int Int TermBool ))
-:extrafuns (( intLess Int Int TermBool ))
-:extrafuns (( intAtMost Int Int TermBool ))
-:extrafuns (( intGreater Int Int TermBool ))
-:extrafuns (( intAtLeast Int Int TermBool ))
-:extrafuns (( boogieIntMod Int Int Int ))
-:extrafuns (( boogieIntDiv Int Int Int ))
-
-; used for translation with type premisses
-:extrapreds (( UOrdering2 boogieU boogieU ))
-; used for translation with type arguments
-:extrapreds (( UOrdering3 boogieT boogieU boogieU ))
-
-; used for translation with type premisses
-:extrafuns (( TermUOrdering2 boogieU boogieU TermBool ))
-; used for translation with type arguments
-:extrafuns (( TermUOrdering3 boogieT boogieU boogieU TermBool ))
-
- ; formula/term axioms
- :assumption
- (forall (?x TermBool) (?y TermBool)
- (iff
- (= (boolIff ?x ?y) boolTrue)
- (iff (= ?x boolTrue) (= ?y boolTrue))))
-
- :assumption
- (forall (?x TermBool) (?y TermBool)
- (iff
- (= (boolImplies ?x ?y) boolTrue)
- (implies (= ?x boolTrue) (= ?y boolTrue))))
-
- :assumption
- (forall (?x TermBool) (?y TermBool)
- (iff
- (= (boolAnd ?x ?y) boolTrue)
- (and (= ?x boolTrue) (= ?y boolTrue))))
-
- :assumption
- (forall (?x TermBool) (?y TermBool)
- (iff
- (= (boolOr ?x ?y) boolTrue)
- (or (= ?x boolTrue) (= ?y boolTrue))))
-
- :assumption
- (forall (?x TermBool)
- (iff
- (= (boolNot ?x) boolTrue)
- (not (= ?x boolTrue)))
- :pat { (boolNot ?x) }
- )
-
- :assumption
- (forall (?x boogieU) (?y boogieU)
- (iff
- (= (UEqual ?x ?y) boolTrue)
- (= ?x ?y)))
-
- :assumption
- (forall (?x boogieT) (?y boogieT)
- (iff
- (= (TEqual ?x ?y) boolTrue)
- (= ?x ?y)))
-
- :assumption
- (forall (?x Int) (?y Int)
- (iff
- (= (IntEqual ?x ?y) boolTrue)
- (= ?x ?y)))
-
- :assumption
- (forall (?x Int) (?y Int)
- (iff
- (= (intLess ?x ?y) boolTrue)
- (< ?x ?y)))
-
- :assumption
- (forall (?x Int) (?y Int)
- (iff
- (= (intAtMost ?x ?y) boolTrue)
- (<= ?x ?y)))
-
- :assumption
- (forall (?x Int) (?y Int)
- (iff
- (= (intAtLeast ?x ?y) boolTrue)
- (>= ?x ?y)))
-
- :assumption
- (forall (?x Int) (?y Int)
- (iff
- (= (intGreater ?x ?y) boolTrue)
- (> ?x ?y)))
-
- ; false is not true
- :assumption
- (distinct boolFalse boolTrue)
-
- :assumption
- (forall (?x boogieU) (?y boogieU)
- (iff
- (= (TermUOrdering2 ?x ?y) boolTrue)
- (UOrdering2 ?x ?y)))
-
- :assumption
- (forall (?x boogieT) (?y boogieU) (?z boogieU)
- (iff
- (= (TermUOrdering3 ?x ?y ?z) boolTrue)
- (UOrdering3 ?x ?y ?z)))
-
-; End Boogie universal background predicate
-; -------------------------------------------------------------------------
-
diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2 deleted file mode 100644 index 9bb05bfb..00000000 --- a/Binaries/UnivBackPred2.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -; Boogie universal background predicate
-; Copyright (c) 2004-2010, Microsoft Corp.
-(set-info :category "industrial")
-(declare-sort |T@U| 0)
-(declare-sort |T@T| 0)
-(declare-fun real_pow (Real Real) Real)
-(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
-(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)
diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj index cb37cf6c..f5c366a0 100644 --- a/Source/BoogieDriver/BoogieDriver.csproj +++ b/Source/BoogieDriver/BoogieDriver.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -222,7 +222,7 @@ </PropertyGroup>
<PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|x86'">
<DebugSymbols>true</DebugSymbols>
- <OutputPath>bin\x86\QED\</OutputPath>
+ <OutputPath>..\..\Binaries\</OutputPath>
<DefineConstants>TRACE;DEBUG</DefineConstants>
<DebugType>full</DebugType>
<PlatformTarget>x86</PlatformTarget>
@@ -321,4 +321,4 @@ <Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project>
\ No newline at end of file diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 25bf7b9e..366d9a8b 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -1,14 +1,15 @@ #if QED
+#define DEBUG
+#define DEBUG_DETAIL
+
using System;
using System.Collections;
using System.Collections.Generic;
-
using System.Linq;
using System.Text;
using Microsoft.Boogie;
using Microsoft.Automata;
-
using System.Diagnostics.Contracts;
using Microsoft.Boogie.AbstractInterpretation;
using Microsoft.Boogie.GraphUtil;
@@ -21,17 +22,16 @@ namespace Microsoft.Boogie */
class YieldTypeChecker
{
+ /*static subfields of yieldtypesafe(YTS) property language*/
+ static CharSetSolver yieldTypeCheckerAutomatonSolver;
+ static string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";// regex of property to build automaton of YTS language
+ static Char[][] yieldTypeCheckerVocabulary;
+ static BvSet yielTypeCheckerBvSet;
+ static Automaton<BvSet> yieldTypeCheckerAutomaton;
- static CharSetSolver yieldTypeCheckerAutomatonSolver;
- static string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";
- static Char[][] yieldTypeCheckerVocabulary;
- static BvSet yielTypeCheckerBvSet;
- static Automaton<BvSet> yieldTypeCheckerAutomaton;
-
-
private YieldTypeChecker()
{
-
+
yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
yieldTypeCheckerVocabulary = new char[][] {
new char[]{'1','2'},
@@ -43,54 +43,61 @@ namespace Microsoft.Boogie new char[]{'D','E'}
};
yielTypeCheckerBvSet = yieldTypeCheckerAutomatonSolver.MkRangesConstraint(false, yieldTypeCheckerVocabulary);
- yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); //accepts strings that match the regex r
-
-
+ yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); // YTS property , L(YTSP)
+
+
}
- public static bool IsYieldTypeSafe(Automaton<BvSet> implTypeCheckAutomaton){
-
- List<BvSet> witnessSet;
- var isNonEmpty = Automaton<BvSet>.CheckDifference(
- implTypeCheckAutomaton,
- yieldTypeCheckerAutomaton,
- 0,
- yieldTypeCheckerAutomatonSolver,
- out witnessSet);
+ /*
+ Parameter: Automaton<BvSet> implTypeCheckAutomaton : Automaton of implementation body build with respect to YTSI.
+ Return : if L(YTSI) is subset of L(YTSP) {TRUE} else {FALSE}
+ */
+ public static bool IsYieldTypeSafe(Automaton<BvSet> implTypeCheckAutomaton)
+ {
+
+ List<BvSet> witnessSet;
+ var isNonEmpty = Automaton<BvSet>.CheckDifference(
+ implTypeCheckAutomaton,
+ yieldTypeCheckerAutomaton,
+ 0,
+ yieldTypeCheckerAutomatonSolver,
+ out witnessSet);
+ // Ask Margus, Shaz to be sure !
if (isNonEmpty)
{
- // var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldTypeCheckerAutomatonSolver.Choose(bvset)));
+ // var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldTypeCheckerAutomatonSolver.Choose(bvset)));
//Console.Write("\n Program is not Yield Type Safe \n");
//Console.Write("Debugging ... \n Difference of impl and yiled type check automaton : \n" + witness);
return false;
}
-
- //Console.Write("\n Program is Yield Type Safe \n");
return true;
}
-
+ /*
+ Parameter : LinearTypeChecker linearTypeChecker : YTS Checker is a component of linearTypeChecker.Adds instance of YTS checker into linearType checker
+ */
public static void AddChecker(LinearTypeChecker linearTypeChecker)
{
Program yielTypeCheckedProgram = linearTypeChecker.program;
YieldTypeChecker regExprToAuto = new YieldTypeChecker();
foreach (var decl in yielTypeCheckedProgram.TopLevelDeclarations)
{
- Implementation impl = decl as Implementation;
+ Implementation impl = decl as Implementation;
if (impl != null)
{
- if (impl.Blocks.Count > 0)
+ if (impl.Blocks.Count > 0)// Do yield type checking for every implementation who has body.
{
int phaseNumSpecImpl = 0;
foreach (Ensures e in impl.Proc.Ensures)
{
- phaseNumSpecImpl = QKeyValue.FindIntAttribute(e.Attributes, "phase", int.MaxValue);
+ phaseNumSpecImpl = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0); // Get phase number of implementation's procedure
}
Automaton<BvSet> yieldTypeCheckImpl = YieldTypeCheckerCore.TypeCheck(impl, phaseNumSpecImpl);
- if (!IsYieldTypeSafe(yieldTypeCheckImpl)) {
+ if (!IsYieldTypeSafe(yieldTypeCheckImpl))
+ {
Console.Write("\n Body of " + impl.Proc.Name + " is not yield type safe " + "\n");
return;
-
+
}
}
@@ -99,31 +106,26 @@ namespace Microsoft.Boogie }
}
-
+ /*
+ * Executor class for creating L(YTSI).
+ */
class YieldTypeCheckerCore
{
-
CheckingContext checkingContext;
int errorCount;
-
-
- Implementation ytypeChecked;
- // int numCallInEncImpl; // number of callcmds in impl
+ Implementation ytypeChecked; // Implementation whose body is being YTS checked
int specPhaseNumImpl; // impl.proc's spec num
int yTypeCheckCurrentPhaseNum;// current phase of yield type checking
int programCounter; // initial state of the impl
int concreteInitialState; // First seen initial state in an implementation
-
HashSet<CallCmd> callCmdsInImpl; // callCmdsInImpl[Implementation] ==> Set = { call1, call2, call3 ... }
int numCallCmdInEnclosingProc; // Number of CallCmds in
-
Dictionary<Tuple<int, int>, string> verticesToEdges; // Tuple<int,int> --> "Y" : State(k) --Y--> State(k+1)
HashSet<Tuple<int, int>> yieldTypeCheckGraph; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] where phk+1 == atcSpecPhsNumTypeCheckedProc
- // Dictionary<Implementation, Automaton<YieldTypeSet>> yieldTypeCheckAutomaton; // To be generated with input yieldTypeCheckGraph
-
List<Tuple<int, int>> phaseIntervals; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] intervals
+ List<int> finalStates; //final
+ List<int> initialStates; // initial states collection. There are epsilon transitions (ASCII 'E') from concreteInitial state to these initial states
-
private YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum)
{
ytypeChecked = toTypeCheck;
@@ -133,6 +135,10 @@ namespace Microsoft.Boogie specPhaseNumImpl = specPhaseNum;
yTypeCheckCurrentPhaseNum = 0;
programCounter = Math.Abs(Guid.NewGuid().GetHashCode());
+ initialStates = new List<int>();
+ finalStates = new List<int>();
+
+ initialStates.Add(programCounter);//
concreteInitialState = programCounter;
/*Utility Maps*/
@@ -142,15 +148,16 @@ namespace Microsoft.Boogie // Graph and Automaton
yieldTypeCheckGraph = new HashSet<Tuple<int, int>>();
- verticesToEdges = new Dictionary<Tuple<int, int>, string>();
+ verticesToEdges = new Dictionary<Tuple<int, int>, string>();
}
-
- // return phase intervals
- private void CalculateCallCmds(Implementation impl)
+ /*Parameter : Implementation impl : Implementation whose phase intervals, statistical data(number of call stmts) are computed
+ */
+ private void ComputePhaseIntervals(Implementation impl)
{
List<CallCmd> callCmdInBodyEncImplList = new List<CallCmd>();
-
+
+ // Compute CallCmds inside impl
foreach (Block b in impl.Blocks)
{
List<Cmd> cmds = new List<Cmd>();
@@ -161,61 +168,103 @@ namespace Microsoft.Boogie {
CallCmd callCmd = b.Cmds[i] as CallCmd;
numCallCmdInEnclosingProc = numCallCmdInEnclosingProc + 1;
-
-
-
+
if (!(callCmdsInImpl.Contains(callCmd)))
{
callCmdsInImpl.Add(callCmd);
callCmdInBodyEncImplList.Add(callCmd);//
}
-
}
}
-
}
- //Sort all PhaseNum of callCmds inside Implementation
+
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n CallCmds inside program \n");
+ for (int i = 0; i < callCmdInBodyEncImplList.Count; i++) {
+ Console.Write("\nCallCmd " + callCmdInBodyEncImplList[i].Proc.Name+" ");
+
+ }
+#endif
+ //Collect phase numbers of CallCmds inside impl
List<int> callCmdPhaseNumIndexList = new List<int>();
for (int i = 0; i < callCmdInBodyEncImplList.Count; i++)
{
- int tmpPhaseNum = QKeyValue.FindIntAttribute(callCmdInBodyEncImplList[i].Proc.Attributes, "phase", 0);
- callCmdPhaseNumIndexList.Add(tmpPhaseNum);
+ foreach (Ensures e in callCmdInBodyEncImplList[i].Proc.Ensures)
+ {
+ //callePhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", int.MaxValue);
+ int tmpPhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0);
+ callCmdPhaseNumIndexList.Add(tmpPhaseNum);
+ }
}
+ // Get phase number of procedure of implementation : No Need !
+ // foreach (Ensures e in ytypeChecked.Proc.Ensures)
+ // {
+ // int tmpPhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0);
+ callCmdPhaseNumIndexList.Add(specPhaseNumImpl);
+ //}
+ //Sort all PhaseNum of callCmds inside Implementation
callCmdPhaseNumIndexList.Sort();
-
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n CallCmds's phase numbers \n");
+ for (int i = 0; i < callCmdInBodyEncImplList.Count; i++)
+ {
+ Console.Write("\nCallCmd Phase Num " + callCmdPhaseNumIndexList[i].ToString() + " ");
+ }
+#endif
//Create Phase Intervals
for (int i = 0; i < callCmdPhaseNumIndexList.Count; i++)
{
- //set the initial
+ //create the initial phase (-inf leastPhaseNum]
if (i == 0)
{
Tuple<int, int> initTuple = new Tuple<int, int>(int.MinValue, callCmdPhaseNumIndexList[i]);
phaseIntervals.Add(initTuple);
}
- else
+ else // create other phase intervals
{
Tuple<int, int> intervalToInsert = new Tuple<int, int>(callCmdPhaseNumIndexList[i - 1] + 1, callCmdPhaseNumIndexList[i]);
phaseIntervals.Add(intervalToInsert);
}
}
-
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n Number of phases is " + phaseIntervals.Count.ToString());
+ for (int i = 0;i<phaseIntervals.Count ; i++) {
+ Console.Write("\n Phase " + i.ToString() + "[" + phaseIntervals[i].Item1.ToString() + "," + phaseIntervals[i].Item2.ToString() + "]" + "\n");
+ }
+#endif
}
-
+ /*Parameter:YieldTypeCheckerCore yieldTypeCheckerPerImpl: takes an executor object to do all computation to build L(YTSI)
+ */
public Automaton<BvSet> YieldTypeCheckAutomata(YieldTypeCheckerCore yieldTypeCheckerPerImpl)
- {
-
- for (int i = 0; i<this.phaseIntervals.Count ; i++) {
- yTypeCheckCurrentPhaseNum = this.phaseIntervals[i].Item2 - 1;
+ {
+ ComputePhaseIntervals(yieldTypeCheckerPerImpl.ytypeChecked); // Compute intervals
+ for (int i = 0; i < this.phaseIntervals.Count; i++) // take current phase check num from each interval
+ {
+ yTypeCheckCurrentPhaseNum = this.phaseIntervals[i].Item2 - 1; // set current phase num
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write(" \n TypeChecking for phase " + yTypeCheckCurrentPhaseNum.ToString() + "\n");
+#endif
+ yieldTypeCheckerPerImpl.BuildAutomatonGraph(); // build component of graph for a phase interval
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n Raw Graph is : \n");
+ Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));
+#endif
+ // Bug found and solved: regenerate program counter , dont get the last state of the graph component from last phase interval
+ programCounter = Math.Abs(Guid.NewGuid().GetHashCode());
}
- yieldTypeCheckerPerImpl.BuildAutomatonGraph();
- //Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));
+ // Update edges w.r.t yield reaching. VocabX{True,False}
yieldTypeCheckerPerImpl.PostProcessGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph());
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n Refined Graph is : \n");
+ Console.Write(yieldTypeCheckerPerImpl.PrintGraph(yieldTypeCheckerPerImpl.GetTuplesForGraph()));
+#endif
+ //Build Automaton from graph created
return yieldTypeCheckerPerImpl.BuildAutomaton(yieldTypeCheckerPerImpl.GetTuplesForGraph());
-
+
}
public static Automaton<BvSet> TypeCheck(Implementation impl, int specPhsNum)
@@ -223,20 +272,21 @@ namespace Microsoft.Boogie YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(impl, specPhsNum);
return yieldTypeCheckerPerImpl.YieldTypeCheckAutomata(yieldTypeCheckerPerImpl);
}
-
-
-
-
+ /*
+ * Implementation visitor call this main-visit-entrance function
+ */
private void BuildAutomatonGraph()
{
- foreach (Block block in ytypeChecked.Blocks)
+
+ foreach (Block block in ytypeChecked.Blocks)
{
-
+ // Handles visiting basic commands
for (int i = 0; i < block.Cmds.Count; i++)
{
AddNodeToGraph(block.Cmds[i]);
}
+ //Handles visiting transfer commands
if (block.TransferCmd is GotoCmd)
{
GotoCmd gt = block.TransferCmd as GotoCmd;
@@ -251,14 +301,17 @@ namespace Microsoft.Boogie }
-
+ /*
+ * Creates Graph<int> from HashSet<Tuple<int,int>>
+ */
private Graph<int> GetTuplesForGraph()
{
Graph<int> graphFromTuples = new Graph<int>(yieldTypeCheckGraph);
return graphFromTuples;
-
}
-
+ /*
+ * Visitor functions of basic commands
+ */
private void AddNodeToGraph(Cmd cmd)
{
if (cmd is AssignCmd)
@@ -289,10 +342,8 @@ namespace Microsoft.Boogie }
else if (cmd is CallCmd)
{
-
CallCmd callCmd = cmd as CallCmd;
AddNodeToGraphForCallCmd(callCmd, yTypeCheckCurrentPhaseNum);
-
}
}
@@ -305,19 +356,17 @@ namespace Microsoft.Boogie // Create a Epsilon transition between them
Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
yieldTypeCheckGraph.Add(srcdst);
- verticesToEdges[srcdst] = "N";
+ verticesToEdges[srcdst] = "E";
}
private void AddNodeToGraphForReturnCmd(ReturnCmd cmd)
{
-
// Do nothing !
-
+ finalStates.Add(programCounter);
}
-
+
private void AddNodeToGraphForYieldCmd(YieldCmd cmd)
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -330,7 +379,6 @@ namespace Microsoft.Boogie private void AddNodeToGraphForAssignCmd(AssignCmd cmd)
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -342,7 +390,6 @@ namespace Microsoft.Boogie private void AddNodeToGraphForHavocCmd(HavocCmd cmd)
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -350,12 +397,10 @@ namespace Microsoft.Boogie Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
yieldTypeCheckGraph.Add(srcdst);
verticesToEdges[srcdst] = "Q";
-
}
private void AddNodeToGraphForAssumeCmd(AssumeCmd cmd)
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -363,7 +408,6 @@ namespace Microsoft.Boogie Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
yieldTypeCheckGraph.Add(srcdst);
verticesToEdges[srcdst] = "P";
-
}
private void AddNodeToGraphForAssertCmd(AssertCmd cmd)
@@ -376,28 +420,32 @@ namespace Microsoft.Boogie Tuple<int, int> srcdst = new Tuple<int, int>(source, dest);
yieldTypeCheckGraph.Add(srcdst);
verticesToEdges[srcdst] = "E";
-
}
-
+ /*
+ * Parameter : int currentCheckPhsNum: currentCheckPhsNum is phase num that we do YTS check for.
+ * If (currentCheckPhsNum <= callePhaseNum) {get atomic specification of CallCmd} else{ exit point in the graph is created}
+ *
+ */
private void AddNodeToGraphForCallCmd(CallCmd cmd, int currentCheckPhsNum)
{
int callePhaseNum = 0;
-
foreach (Ensures e in cmd.Proc.Ensures)
{
- callePhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", int.MaxValue);
+ callePhaseNum = QKeyValue.FindIntAttribute(e.Attributes, "phase", 0);
}
+ //Exit point created
if (callePhaseNum > currentCheckPhsNum)
{
+ finalStates.Add(programCounter);
int source = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = source;
+ initialStates.Add(programCounter);
}
else
{
-
-
+ // Get atomic specification of CallCmd's procedure and put as a node in graph
foreach (Ensures e in cmd.Proc.Ensures)
{
if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic"))
@@ -430,7 +478,6 @@ namespace Microsoft.Boogie }
else if (QKeyValue.FindBoolAttribute(e.Attributes, "both"))
{
-
int source = programCounter;
int dest = Math.Abs(Guid.NewGuid().GetHashCode());
programCounter = dest;
@@ -438,24 +485,10 @@ namespace Microsoft.Boogie yieldTypeCheckGraph.Add(srcdst);
verticesToEdges[srcdst] = "B";
}
-
}
-
}
-
}
-
- private Graph<int> CreateGrapFromHashSet(HashSet<Tuple<int, int>> grph)
- {
-
- Graph<int> graphForAutomaton = new Graph<int>(grph);
-
- // Do Some transformation on graph here //
-
- return graphForAutomaton;
-
- }
public string PrintGraph(Graph<int> graph)
{
var s = new StringBuilder();
@@ -463,38 +496,49 @@ namespace Microsoft.Boogie foreach (var e in graph.Edges)
s.AppendLine(" \"" + e.Item1.ToString() + "\" -- " + verticesToEdges[e] + " --> " + " \"" + e.Item2.ToString() + "\";");
s.AppendLine("}");
-
return s.ToString();
-
}
-
- private HashSet<Tuple<int,int>> CollectBackEdges(Graph<int> g, Tuple<int,int> backEdge)
- {
+
+ // Dragon Book Pagepg 662
+ /*
+ * Parameter : backEdge : is an Yield transition in the graph. Compute all backward edges based on predecessors of this node.
+ * This is called for every edge X, CollectBackEdges(graph,X) that has cond "Y".
+ * Return: HashSet<Tuple<int, int>> yieldingEdges : set of edges that can be reached by backEdge which has Y(yield) condition
+ */
+ private HashSet<Tuple<int, int>> CollectBackEdges(Graph<int> g, Tuple<int, int> backEdge)
+ {
int n = backEdge.Item1;
int d = backEdge.Item2;
HashSet<int> loop = new HashSet<int>();
Stack<int> stack = new Stack<int>();
- HashSet<Tuple<int,int>> yieldReachingEdges = new HashSet<Tuple<int,int>>();
+ HashSet<Tuple<int, int>> yieldReachingEdges = new HashSet<Tuple<int, int>>();
loop.Add(d);
if (!n.Equals(d)) // then n is not in loop
{
loop.Add(n);
stack.Push(n); // push n onto stack
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n First pushed item on stack is " + n.ToString());
+#endif
}
while (stack.Count > 0) // not empty
{
int m = stack.Peek();
- // Console.Write("\n Back is : " + m.ToString()+ "\n");
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n Back is : " + m.ToString() + "\n");
+#endif
stack.Pop(); // pop stack
foreach (int p in g.Predecessors(m))
{
- // Contract.Assert(p!= null);
+ // Contract.Assert(p!= null);
if (!(loop.Contains(p)))
{
- Tuple<int , int > yieldReaching = new Tuple<int,int>(p,m);
+ Tuple<int, int> yieldReaching = new Tuple<int, int>(p, m);
yieldReachingEdges.Add(yieldReaching);
- //Console.Write("\n "+ p.ToString()+ " --> " + m.ToString() + "\n");
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n " + p.ToString() + " --> " + m.ToString() + "\n");
+#endif
loop.Add(p);
stack.Push(p); // push p onto stack
}
@@ -502,18 +546,22 @@ namespace Microsoft.Boogie }
return yieldReachingEdges;
}
-
- private HashSet<Tuple<int,int>> BackwardEdgesOfYields(Graph<int> graph)
+ /*
+ * Calls CollectBackEdges for each Y edge existing in graph
+ */
+ private HashSet<Tuple<int, int>> BackwardEdgesOfYields(Graph<int> graph)
{
HashSet<Tuple<int, int>> yieldTrueEdges = new HashSet<Tuple<int, int>>();
-
- foreach(var e in graph.Edges){
-
-
- if(verticesToEdges[e] == "Y"){
- HashSet<Tuple<int,int>> yieldReachingEdges= CollectBackEdges(graph, e);
- foreach(Tuple<int,int> yldrch in yieldReachingEdges){
- // Console.Write("\n" + " From :"+yldrch.Item1.ToString() + " To :"+yldrch.Item2.ToString()+"\n");
+ foreach (var e in graph.Edges)
+ {
+ if (verticesToEdges[e] == "Y")
+ {
+ HashSet<Tuple<int, int>> yieldReachingEdges = CollectBackEdges(graph, e);
+ foreach (Tuple<int, int> yldrch in yieldReachingEdges)
+ {
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n" + " From :" + yldrch.Item1.ToString() + " To :" + yldrch.Item2.ToString() + "\n");
+#endif
yieldTrueEdges.Add(yldrch);
}
}
@@ -521,6 +569,9 @@ namespace Microsoft.Boogie return yieldTrueEdges;
}
+ /*
+ * Updates vertices map according to according to yieldReaching edges. If an edge in graph is not yield reaching that its vertices map updated.
+ */
private void PostProcessGraph(Graph<int> graph)
{
HashSet<Tuple<int, int>> yieldTrueEdges = BackwardEdgesOfYields(graph);
@@ -557,16 +608,11 @@ namespace Microsoft.Boogie {
verticesToEdges[yldrch] = "D";
}
-
-
-
}
foreach (Tuple<int, int> nyldrch in yieldTypeCheckGraph)
{
-
if (!yieldTrueEdges.Contains(nyldrch))
{
-
if (verticesToEdges[nyldrch] == "Q")
{
verticesToEdges[nyldrch] = "4";
@@ -590,69 +636,60 @@ namespace Microsoft.Boogie else if (verticesToEdges[nyldrch] == "A")
{
verticesToEdges[nyldrch] = "B";
- }
-
+ }
+ else if (verticesToEdges[nyldrch] == "Y")
+ {
+ // Bug found : Yielding(Y) == NonYielding(Y)
+ verticesToEdges[nyldrch] = "D";
+ }
}
-
}
}
- private int[] ComputeFinalStates(Graph<int> graph)
+ private int[] ComputeFinalStates()
{
-
- List<int> finalStatesList = new List<int>();
-
- foreach (int fe in graph.Nodes)
+ int[] finalS = new int[finalStates.Count];
+ for (int i = 0; i < finalStates.Count; i++)
{
- foreach (Tuple<int, int> e in graph.Edges)
- {
- if (!fe.Equals(e.Item1))
- {
- finalStatesList.Add(fe);
- }
- }
+ finalS[i] = finalStates[i];
}
- int[] finalStates = new int[finalStatesList.Count];
-
- for (int i = 0; i < finalStatesList.Count; i++) {
- finalStates[i] = finalStatesList[i];
+#if (DEBUG && !DEBUG_DETAIL)
+ for (int i = 0; i < finalStates.Count; i++)
+ {
+ Console.Write("\nAn final state : \n");
+ Console.Write(finalStates[i].ToString() + " ");
}
-
- return finalStates;
+#endif
+ return finalS;
}
- private List<int> ComputeInitalStates(Graph<int> graph) {
+ private List<int> ComputeInitalStates()
+ {
- List<int> initialStates = new List<int>();
- foreach (int fe in graph.Nodes)
+#if (DEBUG && !DEBUG_DETAIL)
+ for (int i = 0; i<initialStates.Count;i++ )
{
- foreach (Tuple<int, int> e in graph.Edges)
- {
- if (!fe.Equals(e.Item2))
- {
- initialStates.Add(fe);
- }
- }
- }
+ Console.Write("\nAn initial state : \n");
+ Console.Write(initialStates[i].ToString() + " ");
+ }
+#endif
return initialStates;
-
}
-
- private Automaton<BvSet> BuildAutomaton(Graph<int> graph) {
-
+
+ private Automaton<BvSet> BuildAutomaton(Graph<int> graph)
+ {
//List<Move<YieldTypeSet>> transitions = new List<Move<YieldTypeSet>>();
List<int[]> transitions = new List<int[]>();
-
- foreach (Tuple<int, int> e in graph.Edges) {
+ foreach (Tuple<int, int> e in graph.Edges)
+ {
if (verticesToEdges[e] == "3")
{
-
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 51; // ASCII 3
- transition[2]=51;
- transition[3] = e.Item2;
- transitions.Add(transition);
+ transition[2] = 51;
+ transition[3] = e.Item2;
+ transitions.Add(transition);
/*
List<int> transition = new List<int>();
@@ -661,14 +698,14 @@ namespace Microsoft.Boogie transition.Add(e.Item2);
transitions.Add(transition);*/
//transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.Q)));
-
+
}
else if (verticesToEdges[e] == "1")
{
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 49; // ASCII 1
- transition[2]=49;
+ transition[2] = 49;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -679,14 +716,14 @@ namespace Microsoft.Boogie transitions.Add(transition);
*/
//transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.P)));
-
+
}
else if (verticesToEdges[e] == "7")
{
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 55; // ASCII 7
- transition[2]=55;
+ transition[2] = 55;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -702,10 +739,10 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 53; // ASCII 5
- transition[2]=53;
+ transition[2] = 53;
transition[3] = e.Item2;
transitions.Add(transition);
-
+
/*
List<int> transition = new List<int>();
transition.Add(e.Item1);
@@ -719,10 +756,10 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 57; // ASCII 9
- transition[2]=57;
+ transition[2] = 57;
transition[3] = e.Item2;
transitions.Add(transition);
-
+
/*
List<int> transition = new List<int>();
transition.Add(e.Item1);
@@ -736,7 +773,7 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 65; // ASCII A
- transition[2]=65;
+ transition[2] = 65;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -752,10 +789,10 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 68; // ASCII D
- transition[2]=68;
+ transition[2] = 68;
transition[3] = e.Item2;
transitions.Add(transition);
-
+
/*
List<int> transition = new List<int>();
transition.Add(e.Item1);
@@ -769,7 +806,7 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 52; // ASCII 4
- transition[2]=52;
+ transition[2] = 52;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -786,7 +823,7 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 50; // ASCII 2
- transition[2]=50;
+ transition[2] = 50;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -802,7 +839,7 @@ namespace Microsoft.Boogie int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 56; // ASCII 8
- transition[2]=56;
+ transition[2] = 56;
transition[3] = e.Item2;
transitions.Add(transition);
/*
@@ -836,7 +873,7 @@ namespace Microsoft.Boogie transition[1] = 67; // ASCII C
transition[2] = 67;
transition[3] = e.Item2;
-
+
transitions.Add(transition);
/*
List<int> transition = new List<int>();
@@ -860,18 +897,20 @@ namespace Microsoft.Boogie transition.Add(66);
transition.Add(e.Item2);
transitions.Add(transition);
- *///transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.AF)));
-
+ */
+ //transitions.Add(Move<YieldTypeSet>.M(e.Item1, e.Item2, new YieldTypeSet(Transitions.AF)));
+
}
- else if (verticesToEdges[e] == "E") {
-
+ else if (verticesToEdges[e] == "E")
+ {
+
int[] transition = new int[4];
transition[0] = e.Item1;
transition[1] = 69; // ASCII E
transition[2] = 69;
- transition[3] =e.Item2;
+ transition[3] = e.Item2;
transitions.Add(transition);
-
+
/*List<int> transition = new List<int>();
transition.Add(e.Item1);
transition.Add(69);
@@ -879,32 +918,41 @@ namespace Microsoft.Boogie transitions.Add(transition);
*/
//transitions.Add(Move<YieldTypeSet>.Epsilon(e.Item1,e.Item2));
-
+
}
-
- }
+ }
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write(" \n Transitions before EPSILONS are added\n ");
+ for (int i = 0; i < transitions.Count; i++)
+ {
+ int[] trans = transitions[i];
+ Console.Write("\n From : " + trans[0].ToString() + "--- " + trans[1] + " --- " + " to : " + trans[3].ToString());
+ }
+#endif
var solver = new CharSetSolver();
-
+
// get initial states
- List<int> initialStates = ComputeInitalStates(graph);
+ List<int> initialStates = ComputeInitalStates();
+
// get final states
- int[] finalStates = ComputeFinalStates(graph);
- // put Epslion from first initial state seen to other initial states created
+ int[] finalStates = ComputeFinalStates();
- foreach (int s in initialStates) {
+ // put Epslion from first initial state seen to other initial states created
+ foreach (int s in initialStates)
+ {
// Put every one epsilon to itself no problem
/*if (!s.Equals(concreteInitialState)) { }*/
-
+
if (!s.Equals(concreteInitialState))
- {
+ {
int[] transition = new int[4];
transition[0] = concreteInitialState;
transition[1] = 69;
transition[2] = 69;
- transition[3] = s;
-
+ transition[3] = s;
+ transitions.Add(transition);
/*
List<int> transition = new List<int>();
transition.Add(concreteInitialState);
@@ -913,41 +961,54 @@ namespace Microsoft.Boogie transition.Add(s);
transitions.Add(transition);
- */
+ */
}
//transitions.Add(Move<YieldTypeSet>.Epsilon(concreteInitialState,s));
}
-
-
-
-
- // int[][] transitionArray = new int[5][];
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write(" \n Transitions are\n ");
+ for (int i = 0; i < transitions.Count; i++)
+ {
+ int[] trans = transitions[i];
+ Console.Write("\n From : " + trans[0].ToString() + "--- " + trans[1] + " --- " + " to : " + trans[3].ToString());
+ }
+#endif
+
+
// create Automaton
- Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(concreteInitialState,finalStates,transitions);
+ Automaton<BvSet> yieldTypeCheckAutomaton = solver.ReadFromRanges(concreteInitialState, finalStates, transitions);
+#if (DEBUG && !DEBUG_DETAIL)
+ Console.Write("\n" + ytypeChecked.Proc.Name + " Automaton \n");
+ Console.Write("\n" + "Number of moves " + yieldTypeCheckAutomaton.MoveCount.ToString() + "\n");
+ Console.Write("\n" + "Number of states " + yieldTypeCheckAutomaton.StateCount.ToString() + "\n");
+ foreach (var move in yieldTypeCheckAutomaton.GetMoves())
+ {
+ // Ask Margus,Shaz : BvSet concerns !
+ Console.WriteLine(move.SourceState.ToString() + " " + move.Condition.ToString() + " " + move.TargetState.ToString());
+ //solver.ShowDAG(yieldTypeCheckAutomaton,ytypeChecked.Proc.Name+" Automaton");
+ // solver.ShowGraph(yieldTypeCheckAutomaton,ytypeChecked.Proc.Name+" Automaton");
+ }
+#endif
//create Automaton
//Automaton<YieldTypeSet> yieldTypeCheckAutomaton = Automaton<YieldTypeSet>.Create(concreteInitialState, finalStates, transitions); ;
-
- return yieldTypeCheckAutomaton;
+ return yieldTypeCheckAutomaton;
}
-
+
private void Error(Absy node, string message)
{
checkingContext.Error(node, message);
errorCount++;
}
-
-
}
static class Transitions
{
-
public static uint P = 0x1;
public static uint Q = 0x4;
public static uint Y = 0x1000;
@@ -961,38 +1022,36 @@ namespace Microsoft.Boogie public static uint RF = 0x20;
public static uint LF = 0x800;
public static uint AF = 0x400;
-
-
}
- // Ask Margus :
+ // Ask Margus,Shaz:
// 1. We dont have BvSet constructor to pass uint as parameter
- // 1.1 Assume that I want to add a transition to my list of moves List<Move<BvSet>> transitions ;
- // transitions.Add( Move<BvSet>.M( source, final, !! Here I can not pass an uint as condition and there is no casting possible to BvSet))
- // but I would like to pass a specific bit set in an uint. How can I provide this?
+ // 1.1 Assume that I want to add a transition to my list of moves List<Move<BvSet>> transitions ;
+ // transitions.Add( Move<BvSet>.M( source, final, !! Here I can not pass an uint as condition and there is no casting possible to BvSet))
+ // but I would like to pass a specific bit set in an uint. How can I provide this?
// 2. Assme that I have a regex like
- //string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";
- //2.1 I would like to create an automaton from this regex.
- // Do I need to perform range constraint in BitWidth.BV7 to have only the strings that can be generated by those letters ? Like the following :
-
- // yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
- // yieldTypeCheckerVocabulary = new char[][] {
- // new char[]{'1','2'},
- // new char[]{'3','4'},
- // new char[]{'5','6'},
- // new char[]{'7','8'},
- // new char[]{'9','A'},
- // new char[]{'B','C'},
- // new char[]{'D','E'}
- // };
- // yielTypeCheckerBvSet = yieldTypeCheckerAutomatonSolver.MkRangesConstraint(false, yieldTypeCheckerVocabulary);
- // yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); //accepts strings that match the regex r
-
- //2.2 If we have such automaton created in 2.1 and we would like to check whether another automaton is subset of this. The automaton that we do check for is built as the following
- // state1 -- transitionCond --> state2 : In order to proper subset type checking what transitionCond should be ? BvSet, uint, int, ASCII[CHAR]-> int ? ex : a -> 65
-
-
- public class YieldTypeSet
+ //string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$";
+ //2.1 I would like to create an automaton from this regex.
+ // Do I need to perform range constraint in BitWidth.BV7 to have only the strings that can be generated by those letters ? Like the following :
+
+ // yieldTypeCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7);
+ // yieldTypeCheckerVocabulary = new char[][] {
+ // new char[]{'1','2'},
+ // new char[]{'3','4'},
+ // new char[]{'5','6'},
+ // new char[]{'7','8'},
+ // new char[]{'9','A'},
+ // new char[]{'B','C'},
+ // new char[]{'D','E'}
+ // };
+ // yielTypeCheckerBvSet = yieldTypeCheckerAutomatonSolver.MkRangesConstraint(false, yieldTypeCheckerVocabulary);
+ // yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); //accepts strings that match the regex r
+
+ //2.2 If we have such automaton created in 2.1 and we would like to check whether another automaton is subset of this. The automaton that we do check for is built as the following
+ // state1 -- transitionCond --> state2 : In order to proper subset type checking what transitionCond should be ? BvSet, uint, int, ASCII[CHAR]-> int ? ex : a -> 65
+
+
+ public class YieldTypeSet
{
uint elems;
@@ -1112,4 +1171,5 @@ namespace Microsoft.Boogie }
}
+
#endif
\ No newline at end of file diff --git a/Source/Core/BitvectorAnalysis.cs b/Source/Core/BitvectorAnalysis.cs deleted file mode 100644 index a555352b..00000000 --- a/Source/Core/BitvectorAnalysis.cs +++ /dev/null @@ -1,585 +0,0 @@ -using System;
-using System.Collections.Generic;
-using Microsoft.Boogie;
-using System.Diagnostics;
-
-namespace Microsoft.Boogie {
- // Build an equivalence relation over the set of program expressions
- // Assignment, equality, function calls and procedure calls are the polymorphic operations
- // that can be applied to both bitvectors and all other types.
- // Otherwise all bitvector operations are separate
- public class BitVectorAnalysis : StandardVisitor {
- class DisjointSet {
- DisjointSet parent;
- int rank;
- public DisjointSet() {
- this.parent = this;
- this.rank = 0;
- }
-
- public virtual void Union(DisjointSet that) {
- DisjointSet xRoot = this.Find();
- DisjointSet yRoot = that.Find();
- if (xRoot == yRoot)
- return;
-
- // x and y are not already in same set. Merge them.
- if (xRoot.rank < yRoot.rank) {
- xRoot.parent = yRoot;
- }
- else if (xRoot.rank > yRoot.rank) {
- yRoot.parent = xRoot;
- }
- else {
- yRoot.parent = xRoot;
- xRoot.rank = xRoot.rank + 1;
- }
- }
-
- public DisjointSet Find() {
- if (parent == this) {
- return this;
- }
- else {
- parent = parent.Find();
- return parent;
- }
- }
- }
-
- class MapDisjointSet : DisjointSet {
- private DisjointSet[] args;
- public DisjointSet Args(int i) {
- return args[i];
- }
-
- private DisjointSet result;
- public DisjointSet Result { get { return result; } }
-
- public MapDisjointSet(DisjointSet[] args, DisjointSet result) {
- this.args = args;
- this.result = result;
- }
-
- public override void Union(DisjointSet that) {
- base.Union(that);
- MapDisjointSet thatMap = that as MapDisjointSet;
- Debug.Assert(thatMap != null);
- Debug.Assert(this.args.Length == thatMap.args.Length);
-
- // unify args
- for (int i = 0; i < this.args.Length; i++) {
- if (this.args[i] == null) {
- this.args[i] = thatMap.args[i];
- }
- else if (thatMap.args[i] == null) {
- thatMap.args[i] = this.args[i];
- }
- else {
- this.args[i].Union(thatMap.args[i]);
- }
- }
-
- // unify result
- if (this.result == null) {
- this.result = thatMap.Result;
- }
- else if (thatMap.result == null) {
- thatMap.result = this.result;
- }
- else {
- this.result.Union(thatMap.result);
- }
- }
- }
-
- private Dictionary<Expr, DisjointSet> exprToDisjointSet = new Dictionary<Expr, DisjointSet>();
- private Dictionary<Variable, DisjointSet> varToDisjointSet = new Dictionary<Variable, DisjointSet>();
- private readonly DisjointSet uniqueBv32Set = new DisjointSet();
-
- public int Bits(Expr expr) {
- DisjointSet disjointSet = MakeDisjointSet(expr);
- if (disjointSet.Find() == uniqueBv32Set.Find())
- return 32;
- return 0;
- }
-
- public Type NewType(Variable var) {
- DisjointSet disjointSet = MakeDisjointSet(var);
- return NewType(var.TypedIdent.Type, disjointSet);
- }
-
- public bool IsBv32(Expr expr) {
- DisjointSet disjointSet = MakeDisjointSet(expr);
- return (disjointSet.Find() == uniqueBv32Set.Find());
- }
-
- private Type NewType(Type type, DisjointSet disjointSet) {
- MapType mapType = type as MapType;
- if (mapType == null) {
- if (disjointSet.Find() == uniqueBv32Set.Find())
- return new BvType(32);
- else
- return type;
- }
- else {
- MapDisjointSet mapDisjointSet = disjointSet as MapDisjointSet;
- Debug.Assert(mapDisjointSet != null);
- List<Type> newArguments = new List<Type>();
- Type result = NewType(mapType.Result, mapDisjointSet.Result);
- bool newTypeNeeded = (result != mapType.Result);
- for (int i = 0; i < mapType.Arguments.Count; i++) {
- if (mapDisjointSet.Args(i).Find() == uniqueBv32Set.Find()) {
- newArguments.Add(new BvType(32));
- newTypeNeeded = true;
- }
- else {
- newArguments.Add(mapType.Arguments[i]);
- }
- }
- if (newTypeNeeded) {
- return new MapType(mapType.tok, mapType.TypeParameters, newArguments, result);
- }
- else {
- return mapType;
- }
- }
- }
-
- private DisjointSet MakeDisjointSet(Type type) {
- MapType mapType = type as MapType;
- if (mapType == null) {
- return new DisjointSet();
- }
- DisjointSet[] args = new DisjointSet[mapType.Arguments.Count];
- for (int i = 0; i < args.Length; i++) {
- args[i] = MakeDisjointSet(mapType.Arguments[i]);
- }
- DisjointSet result = MakeDisjointSet(mapType.Result);
- return new MapDisjointSet(args, result);
- }
-
- private DisjointSet MakeDisjointSet(Expr expr) {
- if (!exprToDisjointSet.ContainsKey(expr)) {
- Debug.Assert(expr.Type != null);
- exprToDisjointSet[expr] = MakeDisjointSet(expr.Type);
- }
- return exprToDisjointSet[expr];
- }
-
- private DisjointSet MakeDisjointSet(Variable var) {
- if (!varToDisjointSet.ContainsKey(var)) {
- varToDisjointSet[var] = MakeDisjointSet(var.TypedIdent.Type);
- }
- return varToDisjointSet[var];
- }
-
- public static void DoBitVectorAnalysis(Program program) {
- DuplicateLiteralExpr duplicateLiteralExpr = new DuplicateLiteralExpr();
- duplicateLiteralExpr.Visit(program);
-
- BitVectorAnalysis bvAnalyzer = new BitVectorAnalysis();
- bvAnalyzer.Visit(program);
- IntToBvRewriter intToBvRewriter = new IntToBvRewriter(program, bvAnalyzer);
- intToBvRewriter.Visit(program);
- program.TopLevelDeclarations.Add(intToBvRewriter.bv32Id);
- }
-
- public override Axiom VisitAxiom(Axiom node) {
- return node;
- }
-
- public override Implementation VisitImplementation(Implementation node) {
- for (int i = 0; i < node.InParams.Count; i++) {
- DisjointSet a = MakeDisjointSet(node.InParams[i]);
- DisjointSet b = MakeDisjointSet(node.Proc.InParams[i]);
- a.Union(b);
- }
- for (int i = 0; i < node.OutParams.Count; i++) {
- DisjointSet a = MakeDisjointSet(node.OutParams[i]);
- DisjointSet b = MakeDisjointSet(node.Proc.OutParams[i]);
- a.Union(b);
- }
- return base.VisitImplementation(node);
- }
-
- public override Cmd VisitAssignCmd(AssignCmd node) {
- AssignCmd simpleAssignCmd = node.AsSimpleAssignCmd;
- List<AssignLhs> lhss = simpleAssignCmd.Lhss;
- List<Expr> rhss = simpleAssignCmd.Rhss;
- foreach (Expr rhs in rhss) {
- VisitExpr(rhs);
- }
- for (int i = 0; i < lhss.Count; i++) {
- SimpleAssignLhs lhs = (SimpleAssignLhs) lhss[i];
- DisjointSet lhsSet = MakeDisjointSet(lhs.AsExpr);
- lhsSet.Union(MakeDisjointSet(rhss[i]));
- }
- return base.VisitAssignCmd(node);
- }
-
- public override Cmd VisitCallCmd(CallCmd node) {
- for (int i = 0; i < node.Ins.Count; i++) {
- DisjointSet actual = MakeDisjointSet(node.Ins[i]);
- DisjointSet formal = MakeDisjointSet(node.Proc.InParams[i]);
- actual.Union(formal);
- }
- for (int i = 0; i < node.Outs.Count; i++) {
- DisjointSet actual = MakeDisjointSet(node.Outs[i]);
- DisjointSet formal = MakeDisjointSet(node.Proc.OutParams[i]);
- actual.Union(formal);
- }
- return base.VisitCallCmd(node);
- }
-
- public static bool IsComparisonIntegerFunction(Function func) {
- if (func.Name == "INT_LT")
- return true;
- if (func.Name == "INT_ULT")
- return true;
- if (func.Name == "INT_LEQ")
- return true;
- if (func.Name == "INT_ULEQ")
- return true;
- if (func.Name == "INT_GT")
- return true;
- if (func.Name == "INT_UGT")
- return true;
- if (func.Name == "INT_GEQ")
- return true;
- if (func.Name == "INT_UGEQ")
- return true;
- return false;
- }
-
- public static bool IsIntegerFunction(Function func) {
- if (func.Name == "INT_EQ")
- return true;
- if (func.Name == "INT_NEQ")
- return true;
- if (func.Name == "INT_ADD")
- return true;
- if (func.Name == "INT_SUB")
- return true;
- if (func.Name == "INT_MULT")
- return true;
- if (func.Name == "INT_DIV")
- return true;
- if (func.Name == "INT_LT")
- return true;
- if (func.Name == "INT_ULT")
- return true;
- if (func.Name == "INT_LEQ")
- return true;
- if (func.Name == "INT_ULEQ")
- return true;
- if (func.Name == "INT_GT")
- return true;
- if (func.Name == "INT_UGT")
- return true;
- if (func.Name == "INT_GEQ")
- return true;
- if (func.Name == "INT_UGEQ")
- return true;
- if (func.Name == "INT_AND")
- return true;
- if (func.Name == "INT_OR")
- return true;
- if (func.Name == "INT_XOR")
- return true;
- if (func.Name == "INT_NOT")
- return true;
- if (func.Name == "INT_MINUS_BOTH_PTR_OR_BOTH_INT")
- return true;
- if (func.Name == "INT_MINUS_LEFT_PTR")
- return true;
- if (func.Name == "INT_PLUS")
- return true;
- if (func.Name == "INT_BINARY_BOTH_INT")
- return true;
- return false;
- }
-
- public static bool IsBv32Function(Function func) {
- if (func.Name == "BV32_EQ")
- return true;
- if (func.Name == "BV32_NEQ")
- return true;
- if (func.Name == "BV32_ADD")
- return true;
- if (func.Name == "BV32_SUB")
- return true;
- if (func.Name == "BV32_MULT")
- return true;
- if (func.Name == "BV32_DIV")
- return true;
- if (func.Name == "BV32_LT")
- return true;
- if (func.Name == "BV32_ULT")
- return true;
- if (func.Name == "BV32_LEQ")
- return true;
- if (func.Name == "BV32_ULEQ")
- return true;
- if (func.Name == "BV32_GT")
- return true;
- if (func.Name == "BV32_UGT")
- return true;
- if (func.Name == "BV32_GEQ")
- return true;
- if (func.Name == "BV32_UGEQ")
- return true;
- if (func.Name == "BV32_AND")
- return true;
- if (func.Name == "BV32_OR")
- return true;
- if (func.Name == "BV32_XOR")
- return true;
- if (func.Name == "BV32_NOT")
- return true;
- if (func.Name == "BV32_MINUS_BOTH_PTR_OR_BOTH_INT")
- return true;
- if (func.Name == "BV32_MINUS_LEFT_PTR")
- return true;
- if (func.Name == "BV32_PLUS")
- return true;
- if (func.Name == "BV32_BINARY_BOTH_INT")
- return true;
- return false;
- }
-
- public override Expr VisitNAryExpr(NAryExpr node) {
- BinaryOperator op = node.Fun as BinaryOperator;
- if (op != null) {
- Debug.Assert(node.Args.Count == 2);
- MakeDisjointSet(node.Args[0]).Union(MakeDisjointSet(node.Args[1]));
- }
-
- FunctionCall fcall = node.Fun as FunctionCall;
- if (fcall != null) {
- Function func = fcall.Func;
-
- if (IsIntegerFunction(func)) {
- DisjointSet x;
- if (IsComparisonIntegerFunction(func))
- x = MakeDisjointSet(node.Args[0]);
- else
- x = MakeDisjointSet(node);
- for (int i = 0; i < node.Args.Count; i++) {
- DisjointSet actual = MakeDisjointSet(node.Args[i]);
- actual.Union(x);
- }
- }
-
- if (func.Name == "intToBv32") {
- DisjointSet arg0 = MakeDisjointSet(node.Args[0]);
- arg0.Union(uniqueBv32Set);
- }
-
- if (func.Name == "bv32ToInt") {
- DisjointSet result = MakeDisjointSet(node);
- result.Union(uniqueBv32Set);
- }
-
- if (func.Name == "INT_AND" || func.Name == "INT_OR" || func.Name == "INT_XOR" || func.Name == "INT_NOT") {
- DisjointSet result = MakeDisjointSet(node);
- result.Union(uniqueBv32Set);
- }
- }
-
- 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.Count - 1];
- for (; i < node.Args.Count; 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.Count - 2];
- for (; i < node.Args.Count - 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 VisitIdentifierExpr(IdentifierExpr node) {
- DisjointSet a = MakeDisjointSet(node);
- DisjointSet b = MakeDisjointSet(node.Decl);
- a.Union(b);
- return base.VisitIdentifierExpr(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 bv32Id;
- Dictionary<string, Function> intFunctions;
- Dictionary<string, Function> bv32Functions;
- void DiscoverIntAndBv32Functions(Program program) {
- intFunctions = new Dictionary<string, Function>();
- bv32Functions = new Dictionary<string, Function>();
- foreach (Declaration d in program.TopLevelDeclarations) {
- Function func = d as Function;
- if (func == null) continue;
- if (BitVectorAnalysis.IsIntegerFunction(func)) {
- intFunctions.Add(func.Name, func);
- }
- if (BitVectorAnalysis.IsBv32Function(func)) {
- bv32Functions.Add(func.Name, func);
- }
- }
- }
- string IntToBv32(string name) {
- if (name == "INT_EQ")
- return "BV32_EQ";
- if (name == "INT_NEQ")
- return "BV32_NEQ";
- if (name == "INT_ADD")
- return "BV32_ADD";
- if (name == "INT_SUB")
- return "BV32_SUB";
- if (name == "INT_MULT")
- return "BV32_MULT";
- if (name == "INT_DIV")
- return "BV32_DIV";
- if (name == "INT_LT")
- return "BV32_LT";
- if (name == "INT_ULT")
- return "BV32_ULT";
- if (name == "INT_LEQ")
- return "BV32_LEQ";
- if (name == "INT_ULEQ")
- return "BV32_ULEQ";
- if (name == "INT_GT")
- return "BV32_GT";
- if (name == "INT_UGT")
- return "BV32_UGT";
- if (name == "INT_GEQ")
- return "BV32_GEQ";
- if (name == "INT_UGEQ")
- return "BV32_UGEQ";
- if (name == "INT_AND")
- return "BV32_AND";
- if (name == "INT_OR")
- return "BV32_OR";
- if (name == "INT_XOR")
- return "BV32_XOR";
- if (name == "INT_NOT")
- return "BV32_NOT";
- if (name == "INT_MINUS_BOTH_PTR_OR_BOTH_INT")
- return "BV32_MINUS_BOTH_PTR_OR_BOTH_INT";
- if (name == "INT_MINUS_LEFT_PTR")
- return "BV32_MINUS_LEFT_PTR";
- if (name == "INT_PLUS")
- return "BV32_PLUS";
- if (name == "INT_BINARY_BOTH_INT")
- return "BV32_BINARY_BOTH_INT";
- System.Diagnostics.Debug.Assert(false);
- return "";
- }
-
- Function IntToBv32(Function func) {
- return bv32Functions[IntToBv32(func.Name)];
- }
-
- public IntToBvRewriter(Program program, BitVectorAnalysis bvAnalyzer) {
- this.bvAnalyzer = bvAnalyzer;
- DiscoverIntAndBv32Functions(program);
-
- BvType bv32Type = new BvType(32);
- List<Variable> bv32In = new List<Variable> { 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");
- }
-
- 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 == "intToBv32" || func.Name == "bv32ToInt") {
- node.Fun = new FunctionCall(bv32Id);
- }
- else if (BitVectorAnalysis.IsIntegerFunction(func) && bvAnalyzer.IsBv32(node.Args[0])) {
- node.Fun = new FunctionCall(IntToBv32(func));
- }
- }
- 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/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 95b57a74..b9d6800c 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -482,8 +482,6 @@ namespace Microsoft.Boogie { }
public bool ExpandLambdas = true; // not useful from command line, only to be set to false programatically
public bool DoModSetAnalysis = false;
- public bool DoBitVectorAnalysis = false;
- public string BitVectorAnalysisOutputBplFile = null;
public bool UseAbstractInterpretation = true; // true iff the user want to use abstract interpretation
public int /*0..9*/StepsBeforeWidening = 0; // The number of steps that must be done before applying a widen operator
@@ -1318,13 +1316,6 @@ namespace Microsoft.Boogie { }
return true;
- case "doBitVectorAnalysis":
- DoBitVectorAnalysis = true;
- if (ps.ConfirmArgumentCount(1)) {
- BitVectorAnalysisOutputBplFile = args[ps.i];
- }
- return true;
-
default:
bool optionValue = false;
if (ps.CheckBooleanFlag("printUnstructured", ref optionValue)) {
diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj index 8be4cda9..a5231853 100644 --- a/Source/Core/Core.csproj +++ b/Source/Core/Core.csproj @@ -1,4 +1,4 @@ -<?xml version="1.0" encoding="utf-8"?>
+<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
@@ -164,7 +164,6 @@ <Compile Include="AbsyExpr.cs" />
<Compile Include="AbsyQuant.cs" />
<Compile Include="AbsyType.cs" />
- <Compile Include="BitvectorAnalysis.cs" />
<Compile Include="InterProceduralReachabilityGraph.cs" />
<Compile Include="CommandLineOptions.cs" />
<Compile Include="DeadVarElim.cs" />
@@ -233,4 +232,4 @@ <Target Name="AfterBuild">
</Target>
-->
-</Project>
+</Project>
\ No newline at end of file diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index d9046b17..a53fa06f 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -465,14 +465,6 @@ namespace Microsoft.Boogie if (oc != PipelineOutcome.ResolvedAndTypeChecked)
return;
- // Do bitvector analysis
- if (CommandLineOptions.Clo.DoBitVectorAnalysis)
- {
- Microsoft.Boogie.BitVectorAnalysis.DoBitVectorAnalysis(program);
- PrintBplFile(CommandLineOptions.Clo.BitVectorAnalysisOutputBplFile, program, false);
- return;
- }
-
if (CommandLineOptions.Clo.PrintCFGPrefix != null)
{
foreach (var impl in program.TopLevelDeclarations.OfType<Implementation>())
@@ -484,22 +476,11 @@ namespace Microsoft.Boogie }
}
- // Eliminate dead variables
- Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+ EliminateDeadVariables(program);
- // Collect mod sets
- if (CommandLineOptions.Clo.DoModSetAnalysis)
- {
- Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
- }
+ CollectModSets(program);
- // Coalesce blocks
- if (CommandLineOptions.Clo.CoalesceBlocks)
- {
- if (CommandLineOptions.Clo.Trace)
- Console.WriteLine("Coalescing blocks...");
- Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
- }
+ CoalesceBlocks(program);
if (CommandLineOptions.Clo.StratifiedInlining == 0)
{
@@ -533,6 +514,32 @@ namespace Microsoft.Boogie }
+ public static void CoalesceBlocks(Program program)
+ {
+ if (CommandLineOptions.Clo.CoalesceBlocks)
+ {
+ if (CommandLineOptions.Clo.Trace)
+ Console.WriteLine("Coalescing blocks...");
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+ }
+
+
+ public static void CollectModSets(Program program)
+ {
+ if (CommandLineOptions.Clo.DoModSetAnalysis)
+ {
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
+ }
+ }
+
+
+ public static void EliminateDeadVariables(Program program)
+ {
+ Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+ }
+
+
public static void PrintBplFile(string filename, Program program, bool allowPrintDesugaring, bool setTokens = true)
{
Contract.Requires(program != null);
@@ -695,6 +702,7 @@ namespace Microsoft.Boogie return PipelineOutcome.ResolvedAndTypeChecked;
}
+
public static void Inline(Program program)
{
Contract.Requires(program != null);
@@ -734,6 +742,7 @@ namespace Microsoft.Boogie }
}
+
/// <summary>
/// Given a resolved and type checked Boogie program, infers invariants for the program
/// and then attempts to verify it. Returns:
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 668dede9..05bcdb01 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -53,7 +53,7 @@ namespace Microsoft.Boogie.SMTLib Contract.Requires(gen != null);
Contract.Requires(ctx != null);
- InitializeGlobalInformation("UnivBackPred2.smt2");
+ InitializeGlobalInformation();
this.options = (SMTLibProverOptions)options;
this.ctx = ctx;
@@ -1182,9 +1182,8 @@ namespace Microsoft.Boogie.SMTLib private static string _backgroundPredicates;
- static void InitializeGlobalInformation(string backgroundPred)
+ static void InitializeGlobalInformation()
{
- Contract.Requires(backgroundPred != null);
Contract.Ensures(_backgroundPredicates != null);
//throws ProverException, System.IO.FileNotFoundException;
if (_backgroundPredicates == null) {
@@ -1194,12 +1193,13 @@ namespace Microsoft.Boogie.SMTLib }
else
{
- string codebaseString = cce.NonNull(Path.GetDirectoryName(cce.NonNull(System.Reflection.Assembly.GetExecutingAssembly().Location)));
- string univBackPredPath = Path.Combine(codebaseString, backgroundPred);
- using (StreamReader reader = new System.IO.StreamReader(univBackPredPath))
- {
- _backgroundPredicates = reader.ReadToEnd();
- }
+ _backgroundPredicates = @"
+(set-info :category ""industrial"")
+(declare-sort |T@U| 0)
+(declare-sort |T@T| 0)
+(declare-fun real_pow (Real Real) Real)
+(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
+(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)";
}
}
}
|