From a51d0b34a76bb28e3141225b653cceb646116d78 Mon Sep 17 00:00:00 2001 From: qadeer Date: Mon, 2 Dec 2013 14:27:05 -0800 Subject: forgot to add this file --- Source/Concurrency/YieldTypeChecker.cs | 395 +++++++++++++++++++++++++++++++++ 1 file changed, 395 insertions(+) create mode 100644 Source/Concurrency/YieldTypeChecker.cs diff --git a/Source/Concurrency/YieldTypeChecker.cs b/Source/Concurrency/YieldTypeChecker.cs new file mode 100644 index 00000000..407cb0d3 --- /dev/null +++ b/Source/Concurrency/YieldTypeChecker.cs @@ -0,0 +1,395 @@ +#if QED +using System; +using System.Collections; +using System.Collections.Generic; + +using System.Linq; +using System.Text; +using Microsoft.Boogie; +using Microsoft.Automata; + +namespace Microsoft.Boogie +{ + /* + Summary: + * + */ + class YieldTypeChecker + { + Program typeCheckedProg; + private YieldTypeCheckerCore yTypeChecker; + CharSetSolver yieldTypeCheckerAutomatonSolver; + string yieldTypeCheckerRegex = @"^((1|2)+(3|4))*((D)+(((5|6))+((7|8))+((1|2))+((3|4)))*[A]((9)+(7)+(3))*)*$"; + Char[][] yieldTypeCheckerVocabulary; + BvSet yielTypeCheckerBvSet; + Automaton yieldTypeCheckerAutomaton; + + + public YieldTypeChecker(Program program) + { + typeCheckedProg = program; + 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','F'} + }; + yielTypeCheckerBvSet = yieldTypeCheckerAutomatonSolver.MkRangesConstraint(false, yieldTypeCheckerVocabulary); + yieldTypeCheckerAutomaton = yieldTypeCheckerAutomatonSolver.Convert(yieldTypeCheckerRegex); //accepts strings that match the regex r + this.Run(typeCheckedProg); + } + + // Complete after discussing with Shaz! + // Important function, may be one more function needed ? + //This Function will process the implementation body's > + //1. Map each character in the path string into a character in our Autamaton vocab. + private Dictionary, string[]> ProcRawPath(Dictionary, string[]> rawPaths) + { + + Dictionary, string[]> processedPaths = new Dictionary, string[]>(); + + return processedPaths; + } + + + public bool Run(Program program) + { + + foreach (Implementation impl in program.TopLevelDeclarations) + { + // Create YieldTypeChecker + // Compute Utility Maps for an Implementation + if (impl.Blocks.Count > 0) + { + int phaseNumSpecImpl = QKeyValue.FindIntAttribute(impl.Proc.Attributes, "phase", 0); + yTypeChecker = new YieldTypeCheckerCore(impl, phaseNumSpecImpl); + Dictionary, string[]> inputToAutomata = ProcRawPath(yTypeChecker.PostProcessPaths()); + foreach (KeyValuePair, string[]> pair in inputToAutomata) + { + foreach (string inputPath in pair.Value) + { + if (!(yieldTypeCheckerAutomatonSolver.Accepts(yieldTypeCheckerAutomaton, inputPath))) + { + return false; + } + } + } + + + } + } + return true; + } + } + + /* Dictionary> phaseNumToCall; */ + // I think I dont need this + // phaseNumToCall[Impl] ==> Dictionary dict={ + //foreach(CallCmd in callCmdsInImpl[Impl] + // ->foreach KeyValPair p in dict + // -> get p.Second gives phase num in + + class YieldTypeCheckerCore + { + + CheckingContext checkingContext; + int errorCount; + + + Implementation ytypeChecked; // YieldTypeChecked body + int numCallInEncImpl; + int specPhaseNumImpl; + int yTypeCheckCurrentPhaseNum; + + Dictionary> callCmdsInImpl; // callCmdsInImpl[Implementation] ==> Set = { call1, call2, call3 ... } + Dictionary numCallCmdInEnclosingProc; // Number of CallCmds in + Dictionary, string>> yieldTypeCheckPattern; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] where phk+1 == atcSpecPhsNumTypeCheckedProc + Dictionary>> phaseIntervals; // (-inf ph0 ] (ph0 ph1] (ph1 ph2] ..... (phk phk+1] intervals + + public YieldTypeCheckerCore(Implementation toTypeCheck, int specPhaseNum) + { + ytypeChecked = toTypeCheck; + this.errorCount = 0; + this.checkingContext = new CheckingContext(null); + numCallInEncImpl = 0; + specPhaseNumImpl = specPhaseNum; + yTypeCheckCurrentPhaseNum = 0; + + /*Utility Maps*/ + phaseIntervals = new Dictionary>>(); + yieldTypeCheckPattern = new Dictionary, string>>(); + callCmdsInImpl = new Dictionary>(); + numCallCmdInEnclosingProc = new Dictionary(); + + } + + public Dictionary, string[]> CreateRawInputToTypeCheck() + { + List> iterOverPhaseList = phaseIntervals[ytypeChecked]; + this.CalculateCallCmds(ytypeChecked); + this.VisitImplementation(ytypeChecked); + + for (int i = 0; + + yTypeCheckCurrentPhaseNum <= specPhaseNumImpl + && i < iterOverPhaseList.Count; + + i++) + { + VisitImplementation(ytypeChecked); + yTypeCheckCurrentPhaseNum = yTypeCheckCurrentPhaseNum + iterOverPhaseList[i].Item2 + 1; + } + + return PostProcessPaths(); + + + + + } + + private void CalculateCallCmds(Implementation impl) + { + HashSet callCmdInBodyEncImpl = new HashSet(); + List callCmdInBodyEncImplList = new List(); + + foreach (Block b in impl.Blocks) + { + List cmds = new List(); + for (int i = 0; i < b.Cmds.Count; i++) + { + Cmd cmd = b.Cmds[i]; + if (cmd is CallCmd) + { + CallCmd callCmd = b.Cmds[i] as CallCmd; + numCallInEncImpl = numCallInEncImpl + 1; + numCallCmdInEnclosingProc.Add(impl, numCallInEncImpl); + + + if (!(callCmdInBodyEncImpl.Contains(callCmd))) + { + callCmdInBodyEncImpl.Add(callCmd); + callCmdInBodyEncImplList.Add(callCmd);// + + } + + } + } + + } + + //Sort all PhaseNum of callCmds inside Implementation + List callCmdPhaseNumIndexList = new List(); + for (int i = 0; i < callCmdInBodyEncImplList.Count; i++) + { + int tmpPhaseNum = QKeyValue.FindIntAttribute(callCmdInBodyEncImplList[i].Proc.Attributes, "phase", 0); + callCmdPhaseNumIndexList.Add(tmpPhaseNum); + } + + callCmdPhaseNumIndexList.Sort(); + + List> phsIntrvs = new List>(); + //Create Phase Intervals + for (int i = 0; i < callCmdPhaseNumIndexList.Count; i++) + { + //set the initial + if (i == 0) + { + Tuple initTuple = new Tuple(int.MinValue, callCmdPhaseNumIndexList[i]); + phsIntrvs.Add(initTuple); + } + else + { + Tuple intervalToInsert = new Tuple(callCmdPhaseNumIndexList[i - 1] + 1, callCmdPhaseNumIndexList[i]); + phsIntrvs.Add(intervalToInsert); + } + } + + //Set Implementation -> List map + phaseIntervals.Add(ytypeChecked, phsIntrvs); + //Set Implelentation -> CallCmds + callCmdsInImpl.Add(ytypeChecked, callCmdInBodyEncImpl); + //Set Implementation -> numberofCalls + numCallCmdInEnclosingProc.Add(ytypeChecked, numCallInEncImpl); + + } + public void ComputePaths(Block b) + { + + foreach (Cmd cmd in b.Cmds) + { + if (cmd is AssignCmd) + { + AssignCmd assnCmd = cmd as AssignCmd; + AddCheckAssignCmd(assnCmd); + } + else if (cmd is CallCmd) + { + CallCmd callCmd = cmd as CallCmd; + AddCheckCallCmd(callCmd, yTypeCheckCurrentPhaseNum); + } + else if (cmd is AssumeCmd) + { + AssumeCmd assmCmd = cmd as AssumeCmd; + AddCheckAssumeCmd(assmCmd); + } + else if (cmd is HavocCmd) + { + HavocCmd havocCmd = cmd as HavocCmd; + AddCheckHavocCmd(havocCmd); + } + else if (cmd is YieldCmd) + { + YieldCmd yldCmd = cmd as YieldCmd; + AddCheckYieldCmd(yldCmd); + } + else if (cmd is AssertCmd) + { + AssertCmd assertCmd = cmd as AssertCmd; + AddCheckAssertCmd(assertCmd); + } + } + } + + /* + (-inf 4] -> "PQBAL" "..." + [3 7] -> "PQB" , "PQYA " ... + .. + .. + (k specReachPoint] -> .... + */ + public Dictionary, string[]> PostProcessPaths() + { + Dictionary, string[]> pathsPerPhase = new Dictionary, string[]>(); + Dictionary, string> pathPerPhase = yieldTypeCheckPattern[ytypeChecked]; + List> iterOverPhaseList = phaseIntervals[ytypeChecked]; + + for (int i = 0; i < iterOverPhaseList.Count; i++) + { + string[] pathsPerPhs = pathPerPhase[iterOverPhaseList[i]].Split('S'); + pathsPerPhase.Add(iterOverPhaseList[i], pathsPerPhs); + } + //Discuss with Shaz in detail ! + return pathsPerPhase; + } + + public void AddCheckCallCmd(CallCmd cmd, int currentCheckPhsNum) + { + List> iterOverPhaseList = phaseIntervals[ytypeChecked]; + for (int i = 0; i < iterOverPhaseList.Count; i++) + { + + if (currentCheckPhsNum <= iterOverPhaseList[i].Item2) + { + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "S"; + } + else + { + foreach (Ensures e in ytypeChecked.Proc.Ensures) + { + if (QKeyValue.FindBoolAttribute(e.Attributes, "atomic")) + { + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "A"; + + } + else if (QKeyValue.FindBoolAttribute(e.Attributes, "right")) + { + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "R"; + } + else if (QKeyValue.FindBoolAttribute(e.Attributes, "left")) + { + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "L"; + } + else if (QKeyValue.FindBoolAttribute(e.Attributes, "both")) + { + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "B"; + } + + } + + } + } + } + + public void AddCheckYieldCmd(YieldCmd cmd) + { + List> iterOverPhaseList = phaseIntervals[ytypeChecked]; + for (int i = 0; i < iterOverPhaseList.Count; i++) + { + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "Y"; + } + } + //Assuming that "AssumeCmd can not include Global variable" check done in previous typechecks + public void AddCheckAssumeCmd(AssumeCmd cmd) + { + + List> iterOverPhaseList = phaseIntervals[ytypeChecked]; + for (int i = 0; i < iterOverPhaseList.Count; i++) + { + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] = + yieldTypeCheckPattern[ytypeChecked][iterOverPhaseList[i]] + "Y"; + } + } + + // Go through with Shaz + //public void AddCheckNaryExpr() { } + + // Go through with Shaz + public void AddCheckAssignCmd(AssignCmd cmd) { } + + //Go through with Shaz + public void AddCheckHavocCmd(HavocCmd cmd) { } + + // Go through with Shaz + public void AddCheckAssertCmd(AssertCmd cmd) { } + + + public void VisitImplementation(Implementation node) + { + if (node != ytypeChecked) + { + + Error(node, "The visited implementation must be" + ytypeChecked.Name); + } + + specPhaseNumImpl = QKeyValue.FindIntAttribute(node.Proc.Attributes, "phase", 0); + + // + Stack dfsStack = new Stack(); + HashSet dfsStackAsSet = new HashSet(); + dfsStack.Push(node.Blocks[0]); + dfsStackAsSet.Add(node.Blocks[0]); + while (dfsStack.Count > 0) + { + Block b = dfsStack.Pop(); + dfsStackAsSet.Remove(b); + ComputePaths(b); + + if (b.TransferCmd is ReturnCmd) + { + continue; + } + GotoCmd gotoCmd = b.TransferCmd as GotoCmd; + foreach (Block target in gotoCmd.labelTargets) + { + dfsStack.Push(target); + dfsStackAsSet.Add(target); + } + } + } + + + private void Error(Absy node, string message) + { + checkingContext.Error(node, message); + errorCount++; + } + + + } +} +#endif \ No newline at end of file -- cgit v1.2.3