Commit 593fe1a9 authored by Joachim Müssig's avatar Joachim Müssig
Browse files

clear up code, javadoc

parent 16bd0497
...@@ -32,7 +32,7 @@ import edu.kit.joana.ifc.sdg.graph.SDGNode; ...@@ -32,7 +32,7 @@ import edu.kit.joana.ifc.sdg.graph.SDGNode;
* based on the Wala CFG whether the (potential) illegal information * based on the Wala CFG whether the (potential) illegal information
* flow described by the chop can only occur along the true branch or * flow described by the chop can only occur along the true branch or
* only along the false branch or both. * only along the false branch or both.
* @author mihai * @author mihai, joachim
*/ */
public class BranchAnalyzer { public class BranchAnalyzer {
...@@ -112,9 +112,6 @@ public class BranchAnalyzer { ...@@ -112,9 +112,6 @@ public class BranchAnalyzer {
} }
return result; return result;
} }
...@@ -267,7 +264,6 @@ public class BranchAnalyzer { ...@@ -267,7 +264,6 @@ public class BranchAnalyzer {
ISSABasicBlock falseBlock = Util.getNotTakenSuccessor(cfg, basicblock); ISSABasicBlock falseBlock = Util.getNotTakenSuccessor(cfg, basicblock);
//construct the set of successor basic blocks along the true branch //construct the set of successor basic blocks along the true branch
Collection<ISSABasicBlock> trueSuccessors = cfg.getNormalSuccessors(trueBlock); Collection<ISSABasicBlock> trueSuccessors = cfg.getNormalSuccessors(trueBlock);
System.out.println(cfg.getSuccNodeCount(falseBlock));
trueSuccessors.add(trueBlock); trueSuccessors.add(trueBlock);
//construct the set of successor basic blocks along the false branch //construct the set of successor basic blocks along the false branch
Collection<ISSABasicBlock> falseSuccessors = cfg.getNormalSuccessors(falseBlock); Collection<ISSABasicBlock> falseSuccessors = cfg.getNormalSuccessors(falseBlock);
...@@ -289,11 +285,10 @@ public class BranchAnalyzer { ...@@ -289,11 +285,10 @@ public class BranchAnalyzer {
//get basic block for successor //get basic block for successor
SSACFG succCFG = getCFG(succ); SSACFG succCFG = getCFG(succ);
BasicBlock succBlock = succCFG.getBlockForInstruction(succInstrIndex); BasicBlock succBlock = succCFG.getBlockForInstruction(succInstrIndex);
List<ISSABasicBlock> dominators = calculateDominators(succBlock, cfg); List<ISSABasicBlock> dominators = calculateDominators(succBlock, cfg);
if(inFalseBranch(dominators, falseBlock)) { if(inFalseBranch(dominators, falseBlock)) {
//TODO: remove if not needed
} }
//set flag if the successor is among the true successors //set flag if the successor is among the true successors
...@@ -353,7 +348,6 @@ public class BranchAnalyzer { ...@@ -353,7 +348,6 @@ public class BranchAnalyzer {
} }
} }
//TODO:
private boolean inTrueBranch(List<ISSABasicBlock> dominators, ISSABasicBlock firstTrueBlock) { private boolean inTrueBranch(List<ISSABasicBlock> dominators, ISSABasicBlock firstTrueBlock) {
//return true if first true block of predicate block is contained in dominators //return true if first true block of predicate block is contained in dominators
if (dominators.contains(firstTrueBlock)) { if (dominators.contains(firstTrueBlock)) {
...@@ -439,6 +433,11 @@ public class BranchAnalyzer { ...@@ -439,6 +433,11 @@ public class BranchAnalyzer {
} }
return result; return result;
} }
/**
* generate the contact and the assume method. This string should be appended to the sliced java file.
* @return String with assume contract and assume method
*/
public String getAssumeMethod() { public String getAssumeMethod() {
String contract = "/*@\n" String contract = "/*@\n"
+ "@ requires true;\n" + "@ requires true;\n"
......
...@@ -39,12 +39,10 @@ public class Main { ...@@ -39,12 +39,10 @@ public class Main {
// File joakFile = new File("/home/mihai/workspace/keyjoana/testdata/loop2.joak"); // File joakFile = new File("/home/mihai/workspace/keyjoana/testdata/loop2.joak");
File joakFile = new File("/home/joachim/JoanaKeYBeispiele/SecureExamples/IFLoop2/program/Joak/test.joak"); File joakFile = new File("/home/joachim/JoanaKeYBeispiele/SecureExamples/IFLoop2/program/Joak/test.joak");
// File joakFile = new File("/home/joachim/JoanaKeYBeispiele/SecureExamples/IFLoop2/program/Joak/IFLoop2JoakWithSDGNodesWithStateSaverString3.joak");
System.out.println("Starting Joana..."); System.out.println("Starting Joana...");
JoanaAndKeYCheckData data = CombinedApproach.parseInputFile(joakFile); JoanaAndKeYCheckData data = CombinedApproach.parseInputFile(joakFile);
data.addAnnotations(); data.addAnnotations();
//IFCAnalysis ana = data.getAnalysis(); //IFCAnalysis ana = data.getAnalysis();
SDGAnalysis ana = (SDGAnalysis) data.getAnalysis(); SDGAnalysis ana = (SDGAnalysis) data.getAnalysis();
...@@ -86,7 +84,6 @@ public class Main { ...@@ -86,7 +84,6 @@ public class Main {
cg = data.getStateSaver().getCallGraph(); cg = data.getStateSaver().getCallGraph();
//TODO: PreProcessor
ProgramSimplifier simplifer = new ProgramSimplifier(high, low, sdg); ProgramSimplifier simplifer = new ProgramSimplifier(high, low, sdg);
//Set<SDGNode> relevantNodes = simplifer.getBackwardsSlice(); //Set<SDGNode> relevantNodes = simplifer.getBackwardsSlice();
// Set<SDGNode> relevantNodes = simplifer.getChopNodes(); // Set<SDGNode> relevantNodes = simplifer.getChopNodes();
......
...@@ -235,6 +235,12 @@ public class SourceCodeSlicer { ...@@ -235,6 +235,12 @@ public class SourceCodeSlicer {
} }
/**
* Write the slice to a File
* @param slice result you want to write to a file
* @param target path to the File
* @throws IOException
*/
public void writeSlice(Map<String, Set<Integer>> slice, String target) throws IOException { public void writeSlice(Map<String, Set<Integer>> slice, String target) throws IOException {
File sourceFolder = new File(pathToJavaSource); File sourceFolder = new File(pathToJavaSource);
...@@ -277,6 +283,10 @@ public class SourceCodeSlicer { ...@@ -277,6 +283,10 @@ public class SourceCodeSlicer {
} }
} }
/**
* print the slice result
* @param slice
*/
public void printSlice(Map<String, Set<Integer>> slice){ public void printSlice(Map<String, Set<Integer>> slice){
for(String file : slice.keySet()){ for(String file : slice.keySet()){
......
...@@ -50,7 +50,6 @@ public class ViolationSlicer { ...@@ -50,7 +50,6 @@ public class ViolationSlicer {
File target = new File(pathToJavaFile); File target = new File(pathToJavaFile);
String targetPath = target.getParentFile().getAbsolutePath() + File.separator + "slices" + File.separator String targetPath = target.getParentFile().getAbsolutePath() + File.separator + "slices" + File.separator
+ "slice" + "Source" + high + "Sink" + low + File.separator + "src"; + "slice" + "Source" + high + "Sink" + low + File.separator + "src";
System.out.println("Writing slice to: " + targetPath); System.out.println("Writing slice to: " + targetPath);
try { try {
slicer.writeSlice(slice, targetPath); slicer.writeSlice(slice, targetPath);
...@@ -103,6 +102,7 @@ public class ViolationSlicer { ...@@ -103,6 +102,7 @@ public class ViolationSlicer {
//TODO: finish //TODO: finish
//warning not finished yet //warning not finished yet
@Deprecated
public static void simpifyProgramForAllViolations(Collection<? extends IViolation<SecurityNode>> violations, SDG sdg, JoanaAndKeYCheckData checkData) { public static void simpifyProgramForAllViolations(Collection<? extends IViolation<SecurityNode>> violations, SDG sdg, JoanaAndKeYCheckData checkData) {
int i = 1; int i = 1;
for (IViolation<SecurityNode> violation : violations) { for (IViolation<SecurityNode> violation : violations) {
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment