From 0ef68160d1c969c866f8ada83f35bb43f7faa188 Mon Sep 17 00:00:00 2001 From: kuruis Date: Sat, 4 Jan 2014 20:18:16 -0800 Subject: points on "home strecth of yield type checker" added --- Source/Concurrency/YieldTypeChecker.cs | 771 ++++++++++++++------------------- 1 file changed, 322 insertions(+), 449 deletions(-) diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs index 919f5dd7..24e5f437 100644 --- a/Source/Concurrency/YieldTypeChecker.cs +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -1,7 +1,8 @@ #if QED #define DEBUG -#define DEBUG_DETAIL +#define OPTIMIZED +#define NONOPTIMIZED using System; using System.Collections; @@ -18,29 +19,42 @@ namespace Microsoft.Boogie { using Set = GSet; - /* - Summary: - * - */ class YieldTypeChecker { /*static subfields of yieldtypesafe(YTS) property language*/ static CharSetSolver yieldCheckerAutomatonSolver; - static string yieldReachabilityCheckerRegex = @"^([1234])*([D]+([56781234])*A*([973])*)*$";// regex of property to build automaton of YTS language +#if OPTIMIZED + static string yieldReachabilityOptCheckerRegex = @"^1*([D]+([571])*A?([97])*)*$"; + static Automaton yieldReachabilityOptCheckerAutomaton; + static Automaton minimizedReachabilityOptCheckerAutomaton; +#endif +#if !NONOPTIMIZED + static string yieldReachabilityCheckerRegex = @"^([1234])*([D]+([56781234])*A?([973])*)*$";// regex of property to build automaton of YTS language static Automaton yieldReachabilityCheckerAutomaton; static Automaton minimizedReachabilityCheckerAutomaton; +#endif static Automaton yieldTypeSafeCheckerAutomaton; static Automaton minimizedYieldTypeSafeCheckerAutomaton; static YieldTypeChecker() { yieldCheckerAutomatonSolver = new CharSetSolver(BitWidth.BV7); +#if !NONOPTIMIZED yieldReachabilityCheckerAutomaton = Automaton.MkProduct(yieldCheckerAutomatonSolver.Convert(yieldReachabilityCheckerRegex), yieldCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"), // result of product with this Automaton provides us an automaton that has (*) existence alphanum chars in our property automaton yieldCheckerAutomatonSolver); minimizedReachabilityCheckerAutomaton = yieldReachabilityCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver); +#endif + +#if OPTIMIZED + yieldReachabilityOptCheckerAutomaton = + Automaton.MkProduct(yieldCheckerAutomatonSolver.Convert(yieldReachabilityOptCheckerRegex), + yieldCheckerAutomatonSolver.Convert(@"^[1-9A-D]*$"), // result of product with this Automaton provides us an automaton that has (*) existence alphanum chars in our property automaton + yieldCheckerAutomatonSolver); + minimizedReachabilityOptCheckerAutomaton = yieldReachabilityOptCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver); +#endif yieldTypeSafeCheckerAutomaton = yieldCheckerAutomatonSolver.ReadFromRanges( 0, new int[] { 0, 2 }, @@ -74,8 +88,8 @@ namespace Microsoft.Boogie }); minimizedYieldTypeSafeCheckerAutomaton = yieldTypeSafeCheckerAutomaton.Determinize(yieldCheckerAutomatonSolver).Minimize(yieldCheckerAutomatonSolver); -#if DEBUG && !DEBUG_DETAIL - yieldCheckerAutomatonSolver.ShowGraph(minimizedReachabilityCheckerAutomaton, "minimizedReachabilityPropertyAutomaton.dgml"); +#if !DEBUG + yieldCheckerAutomatonSolver.ShowGraph(minimizedReachabilityOptCheckerAutomaton, "minimizedReachabilityPropertyAutomaton.dgml"); yieldCheckerAutomatonSolver.ShowGraph(minimizedYieldTypeSafeCheckerAutomaton, "minimizedTypeSafePropertyAutomaton.dgml"); #endif } @@ -83,7 +97,6 @@ namespace Microsoft.Boogie private static HashSet ComputePhaseIntervals(MoverTypeChecker moverTypeChecker) { HashSet phases = new HashSet(); - foreach (var decl in moverTypeChecker.program.TopLevelDeclarations) { Procedure proc = decl as Procedure; @@ -101,38 +114,32 @@ namespace Microsoft.Boogie private static Tuple, bool> IsYieldReachabilitySafe(Automaton implReachabilityCheckAutomaton, Implementation impl, MoverTypeChecker moverTypeChecker, int phaseNum) { - List witnessSet; +#if !NONOPTIMIZED var isNonEmpty = Automaton.CheckDifference( implReachabilityCheckAutomaton, yieldReachabilityCheckerAutomaton, 0, yieldCheckerAutomatonSolver, out witnessSet); - - - var diffAutomaton = implReachabilityCheckAutomaton.Minus(yieldReachabilityCheckerAutomaton, yieldCheckerAutomatonSolver); -#if DEBUG && !DEBUG_DETAIL - string diffAutomatonGraphName = "diffAutomatonReachabilitySafe" + impl.Proc.Name + phaseNum.ToString(); - yieldCheckerAutomatonSolver.ShowGraph(diffAutomaton, diffAutomatonGraphName+".dgml"); #endif -#if !DEBUG && !DEBUG_DETAIL - string s = yieldTypeCheckerAutomatonSolver.GenerateMember(implTypeCheckAutomaton); - Console.WriteLine("\n member " + s+ " \n"); - if(!yieldTypeCheckerAutomatonSolver.Accepts(yieldTypeCheckerAutomaton,s)){ - Console.WriteLine("Property Automaton accepts a random member of impl_automaton " + s); - }else{ - Console.WriteLine("Property Automaton does not accept a random member of impl_automaton " + s); - } +#if OPTIMIZED + var isNonEmpty = Automaton.CheckDifference( + implReachabilityCheckAutomaton, + yieldReachabilityOptCheckerAutomaton, + 0, + yieldCheckerAutomatonSolver, + out witnessSet); + + var diffAutomaton = implReachabilityCheckAutomaton.Minus(yieldReachabilityOptCheckerAutomaton, yieldCheckerAutomatonSolver); #endif + if (isNonEmpty) { var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldCheckerAutomatonSolver.Choose(bvset))); - Console.WriteLine("error trace " + witness); Tuple, bool> errTraceExists = new Tuple, bool>(diffAutomaton, false); - return errTraceExists; } Tuple, bool> errTraceNotExist = new Tuple, bool>(diffAutomaton, true); @@ -148,32 +155,14 @@ namespace Microsoft.Boogie 0, yieldCheckerAutomatonSolver, out witnessSet); - - - var diffAutomaton = implTypeSafeCheckAutomaton.Minus(yieldTypeSafeCheckerAutomaton, yieldCheckerAutomatonSolver); -#if DEBUG && !DEBUG_DETAIL - string diffAutomatonGraphName = "diffAutomatonTypeSafety" + impl.Proc.Name + phaseNum.ToString(); - yieldCheckerAutomatonSolver.ShowGraph(diffAutomaton, diffAutomatonGraphName + ".dgml"); -#endif -#if !DEBUG && !DEBUG_DETAIL - string s = yieldTypeCheckerAutomatonSolver.GenerateMember(implTypeCheckAutomaton); - Console.WriteLine("\n member " + s+ " \n"); - if(!yieldTypeCheckerAutomatonSolver.Accepts(yieldTypeCheckerAutomaton,s)){ - Console.WriteLine("Property Automaton accepts a random member of impl_automaton " + s); - }else{ - Console.WriteLine("Property Automaton does not accept a random member of impl_automaton " + s); - } -#endif if (isNonEmpty) { var witness = new String(Array.ConvertAll(witnessSet.ToArray(), bvset => (char)yieldCheckerAutomatonSolver.Choose(bvset))); - Console.WriteLine("error trace " + witness); Tuple, bool> errTraceExists = new Tuple, bool>(diffAutomaton, false); return errTraceExists; } - Tuple, bool> errTraceNotExist = new Tuple, bool>(diffAutomaton, true); return errTraceNotExist; } @@ -199,15 +188,10 @@ namespace Microsoft.Boogie YieldTypeChecker regExprToAuto = new YieldTypeChecker(); HashSet phases = ComputePhaseIntervals(moverTypeChecker); -#if DEBUG && !DEBUG_DETAIL - Console.Write("Number of phases is " + phases.Count.ToString()); - foreach (int i in phases) { Console.WriteLine(" phase is " + i.ToString()); } -#endif - YieldTypeCheckerCore yieldTypeCheckerPerImpl = new YieldTypeCheckerCore(moverTypeChecker); foreach (int yTypeCheckCurrentPhaseNum in phases) // take current phase check num from each interval - { + { foreach (var decl in yieldTypeCheckedProgram.TopLevelDeclarations) { Implementation impl = decl as Implementation; @@ -217,6 +201,7 @@ namespace Microsoft.Boogie Tuple, Automaton>, Tuple, Automaton>> yieldCheckAutomatons = yieldTypeCheckerPerImpl.YieldTypeCheckAutomaton(impl, phaseNumSpecImpl, yTypeCheckCurrentPhaseNum); + Tuple, bool> isYieldReachable = IsYieldReachabilitySafe(yieldCheckAutomatons.Item2.Item2, impl, moverTypeChecker, yTypeCheckCurrentPhaseNum); Tuple, bool> isYieldTypeSafe = IsYieldTypeSafe(yieldCheckAutomatons.Item1.Item2, impl, moverTypeChecker, yTypeCheckCurrentPhaseNum); Automaton isYieldTypeSafeErrorAut = isYieldTypeSafe.Item1; @@ -244,9 +229,7 @@ namespace Microsoft.Boogie } else if (isYieldReachable.Item2 && isYieldTypeSafe.Item2) { -#if DEBUG && !DEBUG_DETAIL - // Console.WriteLine("Implementation " + impl.Proc.Name + " is yield safe at phase " + "[ " + phaseIntervals[i].Item1.ToString()+ " " +phaseIntervals[i].Item2.ToString()+" ]"); -#endif + } } } @@ -258,45 +241,50 @@ namespace Microsoft.Boogie int stateCounter; MoverTypeChecker moverTypeChecker; CharSetSolver solver; + Dictionary, string> edgeLabels; + HashSet finalStates; + HashSet initialStates; + Dictionary abysToNode; + Graph graph; + int specPhaseNumImpl, yTypeCheckCurrentPhaseNum; + Implementation yTypeChecked; + public YieldTypeCheckerCore(MoverTypeChecker moverTypeChecker) { solver = new CharSetSolver(BitWidth.BV7); this.moverTypeChecker = moverTypeChecker; + } - public Tuple, Automaton>, Tuple, Automaton>> YieldTypeCheckAutomaton(Implementation ytypeChecked, int specPhaseNumImpl, int yTypeCheckCurrentPhaseNum) + public Tuple, Automaton>, Tuple, Automaton>> YieldTypeCheckAutomaton(Implementation ytypeChecked, int specPhsNumImpl, int yTypeCheckCurPhaseNum) { + edgeLabels = new Dictionary, string>(); // Tuple --> "Y" : State(k) --Y--> State(k+1) - Dictionary, string> edgeLabels = new Dictionary, string>(); // Tuple --> "Y" : State(k) --Y--> State(k+1) - Dictionary abysToNode = CreateStateNumbers(ytypeChecked, yTypeCheckCurrentPhaseNum); - List finalStates = new List(); - List initialStates = new List(); + finalStates = new HashSet(); + initialStates = new HashSet(); stateCounter = 0; + yTypeChecked = ytypeChecked; + specPhaseNumImpl = specPhsNumImpl; + yTypeCheckCurrentPhaseNum = yTypeCheckCurPhaseNum; initialStates.Add(stateCounter); // First state is added to initial states - Graph bodyGraphForImplPhaseJ = BuildAutomatonGraph(ytypeChecked, yTypeCheckCurrentPhaseNum, abysToNode, edgeLabels, initialStates, finalStates); // build component of graph for a phase interval + abysToNode = CreateStateNumbers(); + graph = BuildAutomatonGraph(); // build component of graph for a phase interval -#if (DEBUG && !DEBUG_DETAIL) - Console.Write("\n Procedure's phase num is " + specPhaseNumImpl.ToString() + " \n"); - Console.Write("\n YieldTypeSafe Graph is created for phase: \n" + yTypeCheckCurrentPhaseNum.ToString()); - Console.Write(PrintGraph(bodyGraphForImplPhaseJ, ytypeChecked, edgeLabels)); -#endif - Automaton implYieldTypeSafeCheckAut = BuildAutomatonYieldTypeSafe(bodyGraphForImplPhaseJ, edgeLabels, initialStates, finalStates, ytypeChecked, yTypeCheckCurrentPhaseNum); + Automaton implYieldTypeSafeCheckAut = BuildAutomatonYieldTypeSafe(); Dictionary nodeToAbysYieldTypeSafe = new Dictionary(); foreach (KeyValuePair state in abysToNode) { nodeToAbysYieldTypeSafe[state.Value] = state.Key; } Tuple, Automaton> implYieldTypeSafeCheckAutomaton = new Tuple, Automaton>(nodeToAbysYieldTypeSafe, implYieldTypeSafeCheckAut); - - // Update edges w.r.t yield reaching. VocabX{True,False} +#if !NONOPTIMIZED + // Update edges w.r.t yield reaching. VocabX{True,False} PostProcessGraph(bodyGraphForImplPhaseJ, edgeLabels); -#if (DEBUG && !DEBUG_DETAIL) - Console.Write("\n Procedure's phase num is " + specPhaseNumImpl.ToString() +" \n"); - Console.Write("\n YieldReachabilityCheck Graph is created for phase : \n" + yTypeCheckCurrentPhaseNum.ToString()); - Console.Write(PrintGraph(bodyGraphForImplPhaseJ, ytypeChecked, edgeLabels)); -#endif - //Build Automaton from graph created Automaton implYieldReachCheckAut = BuildAutomatonYieldReachSafe(bodyGraphForImplPhaseJ, edgeLabels, initialStates, finalStates, ytypeChecked, yTypeCheckCurrentPhaseNum); // Last to arguments are just only for showGraph of automaton lib +#endif +#if OPTIMIZED + Automaton implYieldReachCheckAut = BuildOptAutomatonYieldReachSafe(); +#endif Dictionary nodeToAbysYieldReachSafe = new Dictionary(); foreach (KeyValuePair state in abysToNode) { @@ -305,378 +293,314 @@ namespace Microsoft.Boogie Tuple, Automaton> implYieldReachCheckAutomaton = new Tuple, Automaton>(nodeToAbysYieldReachSafe, implYieldReachCheckAut); Tuple, Automaton>, Tuple, Automaton>> yieldCheckImplAutomaton = new Tuple, Automaton>, Tuple, Automaton>>(implYieldTypeSafeCheckAutomaton, implYieldReachCheckAutomaton); - // Tuple, Automaton> yieldCheckImplAutomaton = new Tuple, Automaton>(implYieldTypeSafeCheckAutomaton, implYieldReachCheckAutomaton); return yieldCheckImplAutomaton; } - /* - CreateStateNumbers - 2.1 Input parameters : - 2.1.1 Implementation ytypeChecked - 2.1.2 int yTypeCheckCurrentPhaseNum - 2.2 Return value :Dictionary : returns KeyValuePair as - 2.3 Action :This function creates state numbers of a given body of an impl using incrementing stateCounter. It keeps KeyValuePair as CreateStateNumbers(Implementation ytypeChecked, int yTypeCheckCurrentPhaseNum) + public Dictionary CreateStateNumbers() { Dictionary abysToNodeNo = new Dictionary(); - /* - * Lets call this impl body traversing framework : ITF - foreach block in Impl.Blocks - foreach cmd in block.Cmds - absy2NodeNo[cmd] = stateCounter - stateCouner++ - absy2NodeNo[block.TransferCmd] = stateCounter - stateCounter++ - - */ - foreach (Block block in ytypeChecked.Blocks) + foreach (Block block in yTypeChecked.Blocks) { foreach (Cmd cmd in block.Cmds) { - if (IsAsyncCallCmd(cmd)) continue; -#if DEBUG && !DEBUG_DETAIL - if (IsProperActionCmd(cmd, yTypeCheckCurrentPhaseNum)) { Console.WriteLine( cmd.ToString() + " proper action"); } - if (IsExitStatement(cmd,yTypeCheckCurrentPhaseNum)) { Console.WriteLine(cmd.ToString() + " call exit action"); } - if (IsParallelCallCmdYield(cmd, yTypeCheckCurrentPhaseNum)) { Console.WriteLine( cmd.ToString() + " call parallel action"); } - if (IsSeqComposableParCallCmd(cmd, yTypeCheckCurrentPhaseNum)) { Console.WriteLine( cmd.ToString() + " call composable parallel action"); } -#endif if (cmd is ParCallCmd) { ParCallCmd calle = cmd as ParCallCmd; for (int i = 0; i < calle.CallCmds.Count; i++) { abysToNodeNo[calle.CallCmds[i]] = stateCounter; -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine("ParCmd " + calle.CallCmds[i].Proc.Name + " state " + stateCounter.ToString()); -#endif stateCounter++; } } else { abysToNodeNo[cmd] = stateCounter; - // Console.WriteLine("Cmd " + cmd.ToString() + " state " + stateCounter.ToString()); stateCounter++; } - } abysToNodeNo[block.TransferCmd] = stateCounter; - // Console.WriteLine("Cmd " + block.TransferCmd.ToString() + " state " + stateCounter.ToString()); stateCounter++; } return abysToNodeNo; } - private Graph BuildAutomatonGraph(Implementation ytypeChecked, int yTypeCheckCurrentPhaseNum, Dictionary bodyGraphForImplPhaseJ, - Dictionary, string> edgeLabels, List initialStates, List finalStates) + private Graph BuildAutomatonGraph() { HashSet> edges = new HashSet>(); - foreach (Block block in ytypeChecked.Blocks) + foreach (Block block in yTypeChecked.Blocks) { if (block.Cmds.Count >= 2) { for (int i = 0; i < block.Cmds.Count - 1; i++) { //IsProper - if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum))// this is handled in else but keep this branch now + if (IsProperActionCmd(block.Cmds[i]) && IsProperActionCmd(block.Cmds[i + 1]))// this is handled in else but keep this branch now { // proper state transition - int source = bodyGraphForImplPhaseJ[block.Cmds[i]]; - int dest = bodyGraphForImplPhaseJ[block.Cmds[i + 1]]; - //Console.Write("\n >=2 Adding proper transition " + source.ToString() + " --> " + dest.ToString()); + int source = abysToNode[block.Cmds[i]]; + int dest = abysToNode[block.Cmds[i + 1]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); } - else if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsProperActionCmd(block.Cmds[i]) && IsExitStatement(block.Cmds[i + 1])) { - int source = bodyGraphForImplPhaseJ[block.Cmds[i]]; + int source = abysToNode[block.Cmds[i]]; // create artificial final state int dest = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node ref: http://msdn.microsoft.com/en-us/library/system.guid(v=vs.110).aspx - //Console.Write("\n >=2 Adding next is EXT transition " + source.ToString() + " --> " + dest.ToString()); finalStates.Add(dest); Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); } - else if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsProperActionCmd(block.Cmds[i]) && IsParallelCallCmdYield(block.Cmds[i + 1])) { - int source = bodyGraphForImplPhaseJ[block.Cmds[i]]; + int source = abysToNode[block.Cmds[i]]; ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd; - int dest = bodyGraphForImplPhaseJ[nextCmd.CallCmds[0]]; + int dest = abysToNode[nextCmd.CallCmds[0]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); } - else if (IsProperActionCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsProperActionCmd(block.Cmds[i]) && IsSeqComposableParCallCmd(block.Cmds[i + 1])) { - int source = bodyGraphForImplPhaseJ[block.Cmds[i]]; + int source = abysToNode[block.Cmds[i]]; ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd; - int dest = bodyGraphForImplPhaseJ[nextCmd.CallCmds[0]]; + int dest = abysToNode[nextCmd.CallCmds[0]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); } // IsCallCmdsExit - else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsExitStatement(block.Cmds[i]) && IsProperActionCmd(block.Cmds[i + 1])) { // current cmd exit , next cmd will be put as initial state - //Console.Write("\n >=2 Adding current cmd is EXT next initial" + bodyGraphForImplPhaseJ[block.Cmds[i + 1]].ToString()); - initialStates.Add(bodyGraphForImplPhaseJ[block.Cmds[i + 1]]); - + initialStates.Add(abysToNode[block.Cmds[i + 1]]); } - else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsExitStatement(block.Cmds[i]) && IsExitStatement(block.Cmds[i + 1])) { continue; } - else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsExitStatement(block.Cmds[i]) && IsParallelCallCmdYield(block.Cmds[i + 1])) { // Add state number CallCmd of ParallelCmd ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd; - initialStates.Add(bodyGraphForImplPhaseJ[nextCmd.CallCmds[0]]); + initialStates.Add(abysToNode[nextCmd.CallCmds[0]]); } - else if (IsExitStatement(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsExitStatement(block.Cmds[i]) && IsSeqComposableParCallCmd(block.Cmds[i + 1])) { // Add state number CallCmd of ParallelCmd ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd; - initialStates.Add(bodyGraphForImplPhaseJ[nextCmd.CallCmds[0]]); + initialStates.Add(abysToNode[nextCmd.CallCmds[0]]); } // ParallelCallCmdYield - else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsParallelCallCmdYield(block.Cmds[i]) && IsParallelCallCmdYield(block.Cmds[i + 1])) { ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd; ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd; - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[0]]; - int dest = bodyGraphForImplPhaseJ[nextCmd.CallCmds[0]]; + int source = abysToNode[currentCmd.CallCmds[0]]; + int dest = abysToNode[nextCmd.CallCmds[0]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); } - else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsParallelCallCmdYield(block.Cmds[i]) && IsSeqComposableParCallCmd(block.Cmds[i + 1])) { ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd; ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd; - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[0]]; - int dest = bodyGraphForImplPhaseJ[nextCmd.CallCmds[0]]; + int source = abysToNode[currentCmd.CallCmds[0]]; + int dest = abysToNode[nextCmd.CallCmds[0]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); } - else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsParallelCallCmdYield(block.Cmds[i]) && IsExitStatement(block.Cmds[i + 1])) { //create dummy state as next state ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd; - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[0]]; + int source = abysToNode[currentCmd.CallCmds[0]]; int dest = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node - //Console.Write("\n >=2 Adding next is EXT transition " + source.ToString() + " --> " + dest.ToString()); finalStates.Add(dest); Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); } - else if (IsParallelCallCmdYield(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsParallelCallCmdYield(block.Cmds[i]) && IsProperActionCmd(block.Cmds[i + 1])) { ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd; - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[0]]; - int dest = bodyGraphForImplPhaseJ[block.Cmds[i + 1]]; + int source = abysToNode[currentCmd.CallCmds[0]]; + int dest = abysToNode[block.Cmds[i + 1]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); } //SeqComposable Parallel Cmd - else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsSeqComposableParCallCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsSeqComposableParCallCmd(block.Cmds[i]) && IsSeqComposableParCallCmd(block.Cmds[i + 1])) { ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd; ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd; for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++) { - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j]]; - int dest = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j + 1]]; + int source = abysToNode[currentCmd.CallCmds[j]]; + int dest = abysToNode[currentCmd.CallCmds[j + 1]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[j])); } // Peelout last iteration - int sourceBtwCalls = bodyGraphForImplPhaseJ[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; - int destBtwCalls = bodyGraphForImplPhaseJ[nextCmd.CallCmds[0]]; + int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; + int destBtwCalls = abysToNode[nextCmd.CallCmds[0]]; Tuple edgeBtw = new Tuple(sourceBtwCalls, destBtwCalls); edges.Add(edgeBtw); edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1])); } - else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsParallelCallCmdYield(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsSeqComposableParCallCmd(block.Cmds[i]) && IsParallelCallCmdYield(block.Cmds[i + 1])) { ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd; ParCallCmd nextCmd = block.Cmds[i + 1] as ParCallCmd; for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++) { - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j]]; - int dest = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j + 1]]; + int source = abysToNode[currentCmd.CallCmds[j]]; + int dest = abysToNode[currentCmd.CallCmds[j + 1]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j])); } // Peelout last iteration - int sourceBtwCalls = bodyGraphForImplPhaseJ[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; - int destBtwCalls = bodyGraphForImplPhaseJ[nextCmd.CallCmds[0]]; + int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; + int destBtwCalls = abysToNode[nextCmd.CallCmds[0]]; Tuple edgeBtw = new Tuple(sourceBtwCalls, destBtwCalls); edges.Add(edgeBtw); edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1])); } - else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsExitStatement(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsSeqComposableParCallCmd(block.Cmds[i]) && IsExitStatement(block.Cmds[i + 1])) { ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd; for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++) { - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j]]; - int dest = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j + 1]]; + int source = abysToNode[currentCmd.CallCmds[j]]; + int dest = abysToNode[currentCmd.CallCmds[j + 1]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j])); } // Peelout last iteration - int sourceBtwCalls = bodyGraphForImplPhaseJ[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; + int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; int destBtwCalls = Math.Abs(Guid.NewGuid().GetHashCode()); // Generate unique dummy node - //Console.Write("\n >=2 Adding next is EXT transition " + source.ToString() + " --> " + dest.ToString()); finalStates.Add(destBtwCalls); Tuple edgeBtw = new Tuple(sourceBtwCalls, destBtwCalls); edges.Add(edgeBtw); edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1])); } - else if (IsSeqComposableParCallCmd(block.Cmds[i], yTypeCheckCurrentPhaseNum) && IsProperActionCmd(block.Cmds[i + 1], yTypeCheckCurrentPhaseNum)) + else if (IsSeqComposableParCallCmd(block.Cmds[i]) && IsProperActionCmd(block.Cmds[i + 1])) { ParCallCmd currentCmd = block.Cmds[i] as ParCallCmd; for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++) { - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j]]; - int dest = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j + 1]]; + int source = abysToNode[currentCmd.CallCmds[j]]; + int dest = abysToNode[currentCmd.CallCmds[j + 1]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j])); } // Peelout last iteration - int sourceBtwCalls = bodyGraphForImplPhaseJ[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; - int destBtwCalls = bodyGraphForImplPhaseJ[block.Cmds[i + 1]]; // Generate unique dummy node + int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; + int destBtwCalls = abysToNode[block.Cmds[i + 1]]; // Generate unique dummy node Tuple edgeBtw = new Tuple(sourceBtwCalls, destBtwCalls); edges.Add(edgeBtw); edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1])); - }/* - else - {// Do proper transition - int source = bodyGraphForImplPhaseJ[block.Cmds[i]]; - int dest = bodyGraphForImplPhaseJ[block.Cmds[i + 1]]; - // Console.Write("\n >=2 Adding proper transitionels " + source.ToString() + " --> " + dest.ToString()); - Tuple edge = new Tuple(source, dest); - edges.Add(edge); - edgeLabels.Add(edge, GetEdgeType(block.Cmds[i])); - - }*/ + } } - - - if (IsExitStatement(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum)) + if (IsExitStatement(block.Cmds[block.Cmds.Count - 1])) { // put b.TransferCmd into initial states - //Console.Write("\n >=2 Last cmd is EXT put current as initial " + bodyGraphForImplPhaseJ[block.TransferCmd].ToString()); - - initialStates.Add(bodyGraphForImplPhaseJ[block.TransferCmd]); + initialStates.Add(abysToNode[block.TransferCmd]); } - /* else if (IsAsyncCallCmd(block.Cmds[block.Cmds.Count - 1])) { }*/ - else if (IsParallelCallCmdYield(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum)) + else if (IsParallelCallCmdYield(block.Cmds[block.Cmds.Count - 1])) { ParCallCmd currentCmd = block.Cmds[block.Cmds.Count - 1] as ParCallCmd; - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[0]]; - int dest = bodyGraphForImplPhaseJ[block.TransferCmd]; - //Console.Write("\n >=2 Adding proper transitionels " + source.ToString() + " --> " + dest.ToString()); + int source = abysToNode[currentCmd.CallCmds[0]]; + int dest = abysToNode[block.TransferCmd]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[block.Cmds.Count - 1])); - } - else if (IsSeqComposableParCallCmd(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum)) + else if (IsSeqComposableParCallCmd(block.Cmds[block.Cmds.Count - 1])) { ParCallCmd currentCmd = block.Cmds[block.Cmds.Count - 1] as ParCallCmd; - for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++) { - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j]]; - int dest = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j + 1]]; + int source = abysToNode[currentCmd.CallCmds[j]]; + int dest = abysToNode[currentCmd.CallCmds[j + 1]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j])); } - int sourceBtwCalls = bodyGraphForImplPhaseJ[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; - int destBtwCalls = bodyGraphForImplPhaseJ[block.TransferCmd]; // Generate unique dummy node + int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; + int destBtwCalls = abysToNode[block.TransferCmd]; // Generate unique dummy node Tuple edgeBtw = new Tuple(sourceBtwCalls, destBtwCalls); edges.Add(edgeBtw); edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1])); } - else if (IsProperActionCmd(block.Cmds[block.Cmds.Count - 1], yTypeCheckCurrentPhaseNum)) + else if (IsProperActionCmd(block.Cmds[block.Cmds.Count - 1])) { // proper transition to state before transfer command - int source = bodyGraphForImplPhaseJ[block.Cmds[block.Cmds.Count - 1]]; - int dest = bodyGraphForImplPhaseJ[block.TransferCmd]; - //Console.Write("\n >=2 Adding proper transitionels " + source.ToString() + " --> " + dest.ToString()); + int source = abysToNode[block.Cmds[block.Cmds.Count - 1]]; + int dest = abysToNode[block.TransferCmd]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[block.Cmds.Count - 1])); - } - } else if (block.Cmds.Count == 1) { - if (IsExitStatement(block.Cmds[0], yTypeCheckCurrentPhaseNum)) + if (IsExitStatement(block.Cmds[0])) { // put b.TransferCmd into initial states - // Console.Write("\n == 1 current cmd is EXT "+block.Cmds[0].ToString()+" put it as initial " ); - initialStates.Add(bodyGraphForImplPhaseJ[block.TransferCmd]); + initialStates.Add(abysToNode[block.TransferCmd]); } - else if (IsProperActionCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum)) + else if (IsProperActionCmd(block.Cmds[0])) { // proper transition to state before transfer command - int source = bodyGraphForImplPhaseJ[block.Cmds[0]]; - int dest = bodyGraphForImplPhaseJ[block.TransferCmd]; - // Console.Write("\n ==1 Adding proper transition " + source.ToString() + " --> " + dest.ToString()); - + int source = abysToNode[block.Cmds[0]]; + int dest = abysToNode[block.TransferCmd]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[0])); } - else if (IsParallelCallCmdYield(block.Cmds[0], yTypeCheckCurrentPhaseNum)) + else if (IsParallelCallCmdYield(block.Cmds[0])) { ParCallCmd currentCmd = block.Cmds[0] as ParCallCmd; - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[0]]; - int dest = bodyGraphForImplPhaseJ[block.TransferCmd]; - //Console.Write("\n >=2 Adding proper transitionels " + source.ToString() + " --> " + dest.ToString()); + int source = abysToNode[currentCmd.CallCmds[0]]; + int dest = abysToNode[block.TransferCmd]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(block.Cmds[0])); } - else if (IsSeqComposableParCallCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum)) + else if (IsSeqComposableParCallCmd(block.Cmds[0])) { ParCallCmd currentCmd = block.Cmds[0] as ParCallCmd; for (int j = 0; j < currentCmd.CallCmds.Count - 1; j++) { - int source = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j]]; - int dest = bodyGraphForImplPhaseJ[currentCmd.CallCmds[j + 1]]; + int source = abysToNode[currentCmd.CallCmds[j]]; + int dest = abysToNode[currentCmd.CallCmds[j + 1]]; Tuple edge = new Tuple(source, dest); edges.Add(edge); edgeLabels.Add(edge, GetEdgeType(currentCmd.CallCmds[j])); } - int sourceBtwCalls = bodyGraphForImplPhaseJ[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; - int destBtwCalls = bodyGraphForImplPhaseJ[block.TransferCmd]; // Generate unique dummy node + int sourceBtwCalls = abysToNode[currentCmd.CallCmds[currentCmd.CallCmds.Count - 1]]; + int destBtwCalls = abysToNode[block.TransferCmd]; // Generate unique dummy node Tuple edgeBtw = new Tuple(sourceBtwCalls, destBtwCalls); edges.Add(edgeBtw); edgeLabels.Add(edgeBtw, GetEdgeType(currentCmd.CallCmds[currentCmd.CallCmds.Count - 1])); @@ -684,38 +608,30 @@ namespace Microsoft.Boogie } } else if (block.Cmds.Count == 0) - { - // Target block Entry state will be fetched - //Console.Write("\n == 0 \n" ); - + {// Target block Entry state will be fetched } // Handle - HashSet targetBlockEntryStates = GetStateOfTargetBlock(block.TransferCmd, bodyGraphForImplPhaseJ, yTypeCheckCurrentPhaseNum, initialStates, finalStates); + HashSet targetBlockEntryStates = GetStateOfTargetBlock(block.TransferCmd); foreach (int entryState in targetBlockEntryStates) { - int source = bodyGraphForImplPhaseJ[block.TransferCmd]; + int source = abysToNode[block.TransferCmd]; Tuple transferEdge = new Tuple(source, entryState); - //Console.Write("\n Doing TC " + source.ToString() + " --> " + entryState.ToString()); - edges.Add(transferEdge); edgeLabels.Add(transferEdge, "E"); } } - Graph automatonGraphOfImplPerPhase = new Graph(edges); return automatonGraphOfImplPerPhase; } - private HashSet GetStateOfTargetBlock(TransferCmd tc, Dictionary bodyGraphForImplPhaseJ, int yTypeCheckCurrentPhaseNum, List initialStates, List finalStates) + private HashSet GetStateOfTargetBlock(TransferCmd tc) { HashSet targetBlockEntryStates = new HashSet(); if (tc is ReturnCmd) { ReturnCmd returnCmd = tc as ReturnCmd; - int source = bodyGraphForImplPhaseJ[tc]; + int source = abysToNode[tc]; finalStates.Add(source); - //Console.WriteLine(" There is a return baby ! " + source.ToString()); - // Do Nothing } else if (tc is GotoCmd) { @@ -724,36 +640,35 @@ namespace Microsoft.Boogie { if (block.Cmds.Count == 0) { - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[block.TransferCmd]); //Target block is empty. Add state of target block's transfer command (Goto or Return) + targetBlockEntryStates.Add(abysToNode[block.TransferCmd]); //Target block is empty. Add state of target block's transfer command (Goto or Return) } else if (block.Cmds.Count >= 1) { - if (IsExitStatement(block.Cmds[0], yTypeCheckCurrentPhaseNum)) + if (IsExitStatement(block.Cmds[0])) { - // Create artificial final state and put this into final states int targetState = Math.Abs(Guid.NewGuid().GetHashCode()); finalStates.Add(targetState); targetBlockEntryStates.Add(targetState); } - else if (IsProperActionCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum)) + else if (IsProperActionCmd(block.Cmds[0])) { - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[block.Cmds[0]]); + targetBlockEntryStates.Add(abysToNode[block.Cmds[0]]); } - else if (IsParallelCallCmdYield(block.Cmds[0], yTypeCheckCurrentPhaseNum)) + else if (IsParallelCallCmdYield(block.Cmds[0])) { ParCallCmd targetCmd = block.Cmds[0] as ParCallCmd; - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[targetCmd.CallCmds[0]]); + targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]); } - else if (IsSeqComposableParCallCmd(block.Cmds[0], yTypeCheckCurrentPhaseNum)) + else if (IsSeqComposableParCallCmd(block.Cmds[0])) { ParCallCmd targetCmd = block.Cmds[0] as ParCallCmd; - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[targetCmd.CallCmds[0]]); + targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]); } else if (IsAsyncCallCmd(block.Cmds[0])) { if (block.Cmds.Count == 1) { - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[block.TransferCmd]); + targetBlockEntryStates.Add(abysToNode[block.TransferCmd]); } else if (block.Cmds.Count > 1) { @@ -761,36 +676,36 @@ namespace Microsoft.Boogie for (existsNonAsync = 0; existsNonAsync < block.Cmds.Count; existsNonAsync++) { if (IsAsyncCallCmd(block.Cmds[existsNonAsync])) continue; - else if (IsParallelCallCmdYield(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum)) + else if (IsParallelCallCmdYield(block.Cmds[existsNonAsync])) { ParCallCmd targetCmd = block.Cmds[existsNonAsync] as ParCallCmd; - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[targetCmd.CallCmds[0]]); + targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]); break; } - else if (IsSeqComposableParCallCmd(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum)) + else if (IsSeqComposableParCallCmd(block.Cmds[existsNonAsync])) { ParCallCmd targetCmd = block.Cmds[existsNonAsync] as ParCallCmd; - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[targetCmd.CallCmds[0]]); + targetBlockEntryStates.Add(abysToNode[targetCmd.CallCmds[0]]); break; } - else if (IsExitStatement(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum)) + else if (IsExitStatement(block.Cmds[existsNonAsync])) { int targetState = Math.Abs(Guid.NewGuid().GetHashCode()); finalStates.Add(targetState); targetBlockEntryStates.Add(targetState); break; } - else if (IsExitStatement(block.Cmds[existsNonAsync], yTypeCheckCurrentPhaseNum)) + else if (IsExitStatement(block.Cmds[existsNonAsync])) { - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[block.Cmds[existsNonAsync]]); + targetBlockEntryStates.Add(abysToNode[block.Cmds[existsNonAsync]]); break; } } if (existsNonAsync == block.Cmds.Count) { // put target - targetBlockEntryStates.Add(bodyGraphForImplPhaseJ[block.TransferCmd]); //Target block is empty. Add state of target block's transfer command (Goto or Return) + targetBlockEntryStates.Add(abysToNode[block.TransferCmd]); //Target block is empty. Add state of target block's transfer command (Goto or Return) } } } @@ -836,7 +751,6 @@ namespace Microsoft.Boogie { Set s = ComputeGlobalReads(cmd); s.AddRange(ComputeGlobalWrites(cmd)); - return s; } @@ -855,7 +769,7 @@ namespace Microsoft.Boogie Set vars = new Set(); if (cmd is AssertCmd) - { + { // noop // AssertCmd assertCmd = cmd as AssertCmd; //assertCmd.Expr.ComputeFreeVariables(vars); // We can ignore assert cmds } @@ -864,8 +778,7 @@ namespace Microsoft.Boogie AssumeCmd assumeCmd = cmd as AssumeCmd; assumeCmd.Expr.ComputeFreeVariables(vars); } - // Being checked at Shaz's type checeker - /*else if (cmd is AssignCmd) + else if (cmd is AssignCmd) { AssignCmd assignCmd = cmd as AssignCmd; foreach (AssignLhs assignLhs in assignCmd.Lhss) @@ -880,10 +793,10 @@ namespace Microsoft.Boogie } } foreach (Expr rhs in assignCmd.Rhss) - { + { rhs.ComputeFreeVariables(vars); - } - }*/ + } + } else if (cmd is HavocCmd) { @@ -930,17 +843,16 @@ namespace Microsoft.Boogie { // noop } - /*else if (cmd is AssignCmd) // No need being checked in Shaz's typechecker - { // Actually no need - AssignCmd assignCmd = cmd as AssignCmd; - foreach (AssignLhs assignLhs in assignCmd.Lhss) + else if (cmd is AssignCmd) + { + AssignCmd assignCmd = cmd as AssignCmd; + foreach (AssignLhs assignLhs in assignCmd.Lhss) { - vars.Add(assignLhs.DeepAssignedVariable); + vars.Add(assignLhs.DeepAssignedVariable); } - } */ + } else if (cmd is HavocCmd) { - // Console.WriteLine(" Hovoc wrt"); HavocCmd havocCmd = cmd as HavocCmd; foreach (Expr var in havocCmd.Vars) { var.ComputeFreeVariables(vars); } } @@ -963,11 +875,11 @@ namespace Microsoft.Boogie } // - private bool IsProperActionCmd(Cmd cmd, int yTypeCheckCurrentPhaseNum) + private bool IsProperActionCmd(Cmd cmd) { - if (!IsExitStatement(cmd, yTypeCheckCurrentPhaseNum) && - !IsParallelCallCmdYield(cmd, yTypeCheckCurrentPhaseNum) && - !IsSeqComposableParCallCmd(cmd, yTypeCheckCurrentPhaseNum) && + if (!IsExitStatement(cmd) && + !IsParallelCallCmdYield(cmd) && + !IsSeqComposableParCallCmd(cmd) && !IsAsyncCallCmd(cmd)) { return true; @@ -975,13 +887,13 @@ namespace Microsoft.Boogie return false; } - private bool IsExitStatement(Cmd cmd, int yTypeCheckCurrentPhaseNum) + private bool IsExitStatement(Cmd cmd) { - if (IsCallCmdExitPoint(cmd, yTypeCheckCurrentPhaseNum) || IsAccessToNonQedVar(cmd)) { return true; } + if (IsCallCmdExitPoint(cmd) || IsAccessToNonQedVar(cmd)) { return true; } return false; } - private bool IsCallCmdExitPoint(Cmd cmd, int yTypeCheckCurrentPhaseNum) + private bool IsCallCmdExitPoint(Cmd cmd) { if (cmd is CallCmd && !IsAsyncCallCmd(cmd)) { @@ -989,25 +901,19 @@ namespace Microsoft.Boogie int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(callee.Proc); if (phaseSpecCallee >= yTypeCheckCurrentPhaseNum) { -#if DEBUG && !DEBUG_DETAIL - Console.Write("\nCall Cmd Check is " + callee.Proc.Name + "\n"); -#endif return true; - } - } return false; } - private bool IsParallelCallCmdYield(Cmd cmd, int yTypeCheckCurrentPhaseNum) + private bool IsParallelCallCmdYield(Cmd cmd) { if (cmd is ParCallCmd) { ParCallCmd callee = cmd as ParCallCmd; foreach (CallCmd parCallee in callee.CallCmds) { - int phaseSpecCallee = moverTypeChecker.FindPhaseNumber(parCallee.Proc); if (phaseSpecCallee >= yTypeCheckCurrentPhaseNum) { @@ -1017,29 +923,21 @@ namespace Microsoft.Boogie } return false; } - private bool IsSeqComposableParCallCmd(Cmd cmd, int yTypeCheckCurrentPhaseNum) + + private bool IsSeqComposableParCallCmd(Cmd cmd) { - if (cmd is ParCallCmd && !IsParallelCallCmdYield(cmd, yTypeCheckCurrentPhaseNum)) - { - return true; - } + if (cmd is ParCallCmd && !IsParallelCallCmdYield(cmd)) { return true; } return false; } - private bool IsAsyncCallCmd(Cmd cmd) { if (cmd is CallCmd) { CallCmd calle = cmd as CallCmd; - if (calle.IsAsync) - { - return true; - } + if (calle.IsAsync) { return true; } } return false; } - - private string GetEdgeType(Cmd cmd) { if (cmd is YieldCmd) @@ -1083,9 +981,7 @@ namespace Microsoft.Boogie //} } - - - private string PrintGraph(Graph graph, Implementation yTypeChecked, Dictionary, string> edgeLabels) + private string PrintGraph() { var s = new StringBuilder(); s.AppendLine("\nImplementation " + yTypeChecked.Proc.Name + " digraph G {"); @@ -1094,16 +990,14 @@ namespace Microsoft.Boogie s.AppendLine("}"); return s.ToString(); } - - - private HashSet> CollectBackwardEdgesOfYieldEdge(Graph g, int source) + private HashSet> CollectBackwardEdgesOfYieldEdge(int source) { HashSet> yieldReachingEdges = new HashSet>(); // Collect edges that are backward reachable from source vertex of yield a edge,source ---Y---> sink, in backward direction HashSet gray = new HashSet(); HashSet black = new HashSet(); HashSet white = new HashSet(); // Add all vertices except s into - foreach (int v in g.Nodes) + foreach (int v in graph.Nodes) { if (!v.Equals(source)) white.Add(v); @@ -1117,24 +1011,18 @@ namespace Microsoft.Boogie while (frontier.Count > 0) { int u = frontier.Dequeue(); - foreach (int v in g.Predecessors(u)) + foreach (int v in graph.Predecessors(u)) { -#if DEBUG && !DEBUG_DETAIL - Console.Write("\nVertex " + u.ToString() + " is currently being explored for " + v.ToString() + "\n"); -#endif + if (white.Contains(v) && !gray.Contains(v) && !black.Contains(v)) { -#if DEBUG && !DEBUG_DETAIL - Console.Write(v.ToString() + " is not explored beforehand \n"); -#endif + gray.Add(v); frontier.Enqueue(v); // Add to yielding edges yieldReachingEdges.Add(new Tuple(v, u)); } -#if DEBUG && !DEBUG_DETAIL - Console.Write(v.ToString() + " is already being explored"); -#endif + } black.Add(u); } @@ -1144,19 +1032,17 @@ namespace Microsoft.Boogie /* * Calls CollectBackEdges for each Y edge existing in graph */ - private HashSet> CollectYieldReachingEdgesOfGraph(Graph graph, Dictionary, string> edgeLabels) + private HashSet> CollectYieldReachingEdgesOfGraph() { HashSet> yieldTrueEdges = new HashSet>(); // Set {forall edges e : e is reaching a Y labeled edge} foreach (var e in graph.Edges) // Visits all edges to and do backward yield reachability analysis starting from source vertex of an "Y" labeled edge { if (edgeLabels[e] == "Y") { - HashSet> yieldReachingEdges = CollectBackwardEdgesOfYieldEdge(graph, e.Item1); + HashSet> yieldReachingEdges = CollectBackwardEdgesOfYieldEdge(e.Item1); foreach (Tuple yldrch in yieldReachingEdges) { -#if (DEBUG && !DEBUG_DETAIL) - Console.Write("\n" + " From :" + yldrch.Item1.ToString() + " To :" + yldrch.Item2.ToString() + "\n"); -#endif + yieldTrueEdges.Add(yldrch); } } @@ -1164,12 +1050,128 @@ namespace Microsoft.Boogie return yieldTrueEdges; } + private HashSet> CollectEdgesReachableFromAction(int source) + { + HashSet> edgesReachable = new HashSet>(); // Collect edges that are backward reachable from source vertex of yield a edge,source ---Y---> sink, in backward direction + HashSet gray = new HashSet(); + HashSet black = new HashSet(); + HashSet white = new HashSet(); + // Add all vertices except s into + foreach (int v in graph.Nodes) + { + if (!v.Equals(source)) + white.Add(v); + } + + Queue frontier = new Queue(); // + // n is given as start vertex + gray.Add(source); + frontier.Enqueue(source); + + while (frontier.Count > 0) + { + int u = frontier.Dequeue(); + foreach (int v in graph.Successors(u)) + { + + if (white.Contains(v) && !gray.Contains(v) && !black.Contains(v)) + { + + gray.Add(v); + frontier.Enqueue(v); + // Add to yielding edges + edgesReachable.Add(new Tuple(u, v)); + } + + } + black.Add(u); + } + + return edgesReachable; + + + } + private void IsExitOrRetReachableFromAtomicOrLeft() + { + foreach (var e in graph.Edges) + { + if (edgeLabels[e] == "A" || edgeLabels[e] == "L") + { + HashSet> edgesReachable = CollectEdgesReachableFromAction(e.Item1); + + if (!ReachesFinalState(edgesReachable) || !ReachesYieldState(edgesReachable)) + { + moverTypeChecker.Error(yTypeChecked, "Implementation Yield Reachable " + yTypeChecked.Proc.Name); + } + } + } + } + private void IsExitOrReachableFromBoth() + { + foreach (var e in graph.Edges) + { + if (edgeLabels[e] == "B") + { + HashSet> edgesReachable = CollectEdgesReachableFromAction(e.Item1); + if (!ReachesFinalState(edgesReachable) || !ReachesYieldState(edgesReachable)) + { + // Console.WriteLine("Both is converted to R"); + edgeLabels[e] = "R"; + } + } + } + + } + private void IsExitOrReachableFromLocal() + { + foreach (var e in graph.Edges) + { + if (edgeLabels[e] == "Q") + { + HashSet> edgesReachable = CollectEdgesReachableFromAction(e.Item1); + if (!ReachesFinalState(edgesReachable) || !ReachesYieldState(edgesReachable)) + { + // Console.WriteLine("Q is being converted to P"); + edgeLabels[e] = "P"; + } + edgeLabels[e] = "E"; + } + } + } + private bool ReachesFinalState(HashSet> edges) + { + + foreach (Tuple e in edges) + { + if (finalStates.Contains(e.Item1) || finalStates.Contains(e.Item2)) return true; + } + return false; + } + private bool ReachesYieldState(HashSet> edges) + { + foreach (var e in edges) + { + + if (edgeLabels[e] == "Y") return true; + } + return false; + } + + private Automaton BuildOptAutomatonYieldReachSafe() + { + + IsExitOrRetReachableFromAtomicOrLeft(); + IsExitOrReachableFromBoth(); + IsExitOrReachableFromLocal(); + return BuildAutomatonYieldTypeSafe(); + } + /* * 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 graph, Dictionary, string> edgeLabels) + private void PostProcessGraph() { - HashSet> yieldTrueEdges = CollectYieldReachingEdgesOfGraph(graph, edgeLabels); + HashSet> yieldTrueEdges = CollectYieldReachingEdgesOfGraph(); foreach (Tuple yldrch in yieldTrueEdges) { @@ -1238,37 +1240,16 @@ namespace Microsoft.Boogie } } - private int[] ComputeFinalStates(List finalStates) + private int[] ComputeFinalStates() { - int[] finalS = new int[finalStates.Count]; - for (int i = 0; i < finalStates.Count; i++) - { - finalS[i] = finalStates[i]; - } -#if (DEBUG && !DEBUG_DETAIL) - for (int i = 0; i < finalStates.Count; i++) - { - Console.Write("\nAn final state : \n"); - Console.Write(finalStates[i].ToString() + " "); - } -#endif - return finalS; + return finalStates.ToArray(); } - - - private List ComputeInitalStates(List initialStates) + private int[] ComputeInitialStates() { - -#if (DEBUG && !DEBUG_DETAIL) - for (int i = 0; i BuildAutomatonYieldTypeSafe(Graph graph, Dictionary, string> edgeLabels, List initialStates, List finalStates, Implementation ytypeChecked, int yTypeCheckCurrentPhaseNum) + + private Automaton BuildAutomatonYieldTypeSafe() { List transitions = new List(); foreach (Tuple e in graph.Edges) @@ -1348,32 +1329,8 @@ namespace Microsoft.Boogie } -#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 - - -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine(" ******* Printing initial states\n"); - foreach (int inits in initialStates) { - - Console.WriteLine("initial state is " + inits.ToString()); - } -#endif // get final states - int[] finalSts = ComputeFinalStates(finalStates); -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine("\n*****Printing Finals states\n"); - foreach (int finals in finalSts) - { - Console.WriteLine(" final state " + finals.ToString()); - } -#endif + int[] finalSts = ComputeFinalStates(); int dummyInitial = Math.Abs(Guid.NewGuid().GetHashCode()); foreach (int s in initialStates) { @@ -1384,41 +1341,12 @@ namespace Microsoft.Boogie transition[3] = s; transitions.Add(transition); } - -#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 yieldTypeCheckAutomaton = solver.ReadFromRanges(dummyInitial, finalSts, transitions); -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine("\n--Implementation Automaton for type safe--"); - foreach (var move in yieldTypeCheckAutomaton.GetMoves()) - { - Console.WriteLine("\n " + move.SourceState.ToString() + " -- " + this.PrintEpsilon(move.Condition, solver) + " --> " + move.TargetState.ToString() + " \n"); - } - string implAutomatonGraphName = ytypeChecked.Proc.Name + "YieldTypeSafephaseNum__" + yTypeCheckCurrentPhaseNum.ToString(); - solver.ShowGraph(yieldTypeCheckAutomaton, implAutomatonGraphName + ".dmgl"); -#endif - - -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine("\n--Epsilons Reduced Automaton--"); - foreach (var move in epsilonReducedAtutomaton.GetMoves()) { - Console.WriteLine("\n "+ move.SourceState.ToString() + " -- " + solver.PrettyPrint(move.Condition)+ " --> " + move.TargetState.ToString() +" \n"); - } -#endif - return yieldTypeCheckAutomaton; - } - private Automaton BuildAutomatonYieldReachSafe(Graph graph, Dictionary, string> edgeLabels, List initialStates, List finalStates, Implementation ytypeChecked, int yTypeCheckCurrentPhaseNum) + private Automaton BuildAutomatonYieldReachSafe() { List transitions = new List(); foreach (Tuple e in graph.Edges) @@ -1431,8 +1359,6 @@ namespace Microsoft.Boogie transition[2] = 51; transition[3] = e.Item2; transitions.Add(transition); - - } else if (edgeLabels[e] == "1") { @@ -1442,7 +1368,6 @@ namespace Microsoft.Boogie transition[2] = 49; transition[3] = e.Item2; transitions.Add(transition); - } else if (edgeLabels[e] == "7") { @@ -1452,7 +1377,6 @@ namespace Microsoft.Boogie transition[2] = 55; transition[3] = e.Item2; transitions.Add(transition); - } else if (edgeLabels[e] == "5") { @@ -1462,7 +1386,6 @@ namespace Microsoft.Boogie transition[2] = 53; transition[3] = e.Item2; transitions.Add(transition); - } else if (edgeLabels[e] == "9") { @@ -1472,7 +1395,6 @@ namespace Microsoft.Boogie transition[2] = 57; transition[3] = e.Item2; transitions.Add(transition); - } else if (edgeLabels[e] == "A") { @@ -1558,32 +1480,8 @@ namespace Microsoft.Boogie } -#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 - - -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine(" ******* Printing initial states\n"); - foreach (int inits in initialStates) { - - Console.WriteLine("initial state is " + inits.ToString()); - } -#endif // get final states - int[] finalSts = ComputeFinalStates(finalStates); -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine("\n*****Printing Finals states\n"); - foreach (int finals in finalSts) - { - Console.WriteLine(" final state " + finals.ToString()); - } -#endif + int[] finalSts = ComputeFinalStates(); int dummyInitial = Math.Abs(Guid.NewGuid().GetHashCode()); foreach (int s in initialStates) { @@ -1595,33 +1493,8 @@ namespace Microsoft.Boogie transitions.Add(transition); } -#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 yieldTypeCheckAutomaton = solver.ReadFromRanges(dummyInitial, finalSts, transitions); -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine("\n--Implementation Automaton--"); - foreach (var move in yieldTypeCheckAutomaton.GetMoves()) { - Console.WriteLine("\n "+ move.SourceState.ToString() + " -- " + this.PrintEpsilon(move.Condition,solver)+ " --> " + move.TargetState.ToString() +" \n"); - } - string implAutomatonGraphName = ytypeChecked.Proc.Name + "ReachabilityphaseNum__" + yTypeCheckCurrentPhaseNum.ToString(); - solver.ShowGraph(yieldTypeCheckAutomaton, implAutomatonGraphName+".dmgl"); -#endif - - -#if DEBUG && !DEBUG_DETAIL - Console.WriteLine("\n--Epsilons Reduced Automaton--"); - foreach (var move in epsilonReducedAtutomaton.GetMoves()) { - Console.WriteLine("\n "+ move.SourceState.ToString() + " -- " + solver.PrettyPrint(move.Condition)+ " --> " + move.TargetState.ToString() +" \n"); - } -#endif return yieldTypeCheckAutomaton; } -- cgit v1.2.3