Skip to content

GitLab

K
keyjoana
Commit ed2a3ac2 authored by Joachim Müssig's avatar Joachim Müssig
Browse files
Options

clear up code, javadoc

parent fb230341
Hide whitespace changes
Inline Side-by-side
Showing with 49 additions and 94 deletions
src/gui/asynctaskhandler/AsyncAutoRunner.java
View file @ ed2a3ac2
......@@ -36,7 +36,7 @@ import joanakey.violations.ViolationsWrapper;
/**
*
* @author holger
* @author holger,joachim
*/
public class AsyncAutoRunner implements Runnable {
......@@ -180,7 +180,7 @@ public class AsyncAutoRunner implements Runnable {
NumberFormat formatter = new DecimalFormat("#0.000");
Platform.runLater(() -> {
if (!violationsWrapper.allDisproved()) {
violationsWrapper.resetCheckedEdges();
violationsWrapper.resetCheckedEdges(); //TODO: correct to reset checked edges ?
actionLogger.endProgressWithMessage("Run Auto finished attempt in "
+ formatter.format((endTime - startTime) / 1000d) + " seconds");
} else {
......
src/joanakey/AutomationHelper.java
View file @ ed2a3ac2
......@@ -377,13 +377,13 @@ public class AutomationHelper {
+ LINE_SEP
+ "[SMTSettings]SelectedTaclets="
+ LINE_SEP
+ "[StrategyProperty]METHOD_OPTIONS_KEY="+METHOD_SETTING//METHOD_EXPAND" //TODO: The user should be able to choose from the GUI if he wants expand or contract
+ "[StrategyProperty]METHOD_OPTIONS_KEY="+METHOD_SETTING
+ LINE_SEP
+ "[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF"
+ LINE_SEP
+ "[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER"
+ LINE_SEP
+ "[StrategyProperty]LOOP_OPTIONS_KEY="+LOOP_SETTING//LOOP_EXPAND" //TODO: The user should be able to choose from the GUI if he want to use the option LOOP_INVARANT instead
+ "[StrategyProperty]LOOP_OPTIONS_KEY="+LOOP_SETTING
+ LINE_SEP
+ "[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF"
+ LINE_SEP
......
src/joanakey/CombinedApproach.java
View file @ ed2a3ac2
......@@ -46,6 +46,13 @@ import joanakey.annotations.SDGAnnotationAdder;
import joanakey.annotations.SingleAnnotationAdder;
import joanakey.violations.ViolationsDisproverSemantic;
/**
* Entry of the combined approach.
* This class can parse a given .joak file, which is generated by the spec gui and perform a {@link IFCAnalysis} with Joana.
* The result of the {@link IFCAnalysis} and the information of the .joak file are used to generate a {@link JoanaAndKeYCheckData}.
* @author joachim,..
*
*/
public class CombinedApproach {
public static final String PATH_KeY = "pathKeY";
......@@ -140,6 +147,15 @@ public class CombinedApproach {
return completeString.toString();
}
/**
* parse a .joak file and generate {@link JoanaAndKeYCheckData}.
* @param filetoload the .joak file you want to parse.
* @return {@link JoanaAndKeYCheckData}
* @throws IOException
* @throws ClassHierarchyException
* @throws UnsoundGraphException
* @throws CancelException
*/
public static JoanaAndKeYCheckData parseInputFile(File filetoload)
throws IOException, ClassHierarchyException,
UnsoundGraphException, CancelException {
......@@ -164,7 +180,7 @@ public class CombinedApproach {
StateSaverCGConsumerBuilder stateSaverBuilder = new StateSaverCGConsumerBuilder();
SDGAnalysis analysis = (SDGAnalysis) runJoanaCreateSDGAndIFCAnalyis(pathToJar, pathToSDG, entryMethod, stateSaverBuilder); //TODO restore !
SDGAnalysis analysis = (SDGAnalysis) runJoanaCreateSDGAndIFCAnalyis(pathToJar, pathToSDG, entryMethod, stateSaverBuilder);
StateSaver stateSaver;
if (pathToSDG.isEmpty() && pathToStateSaver.isEmpty()) {
stateSaver = stateSaverBuilder.buildStateSaver(analysis.getProgram().getSDG(), pathToJar, entryMethod.toString());
......@@ -234,17 +250,13 @@ public class CombinedApproach {
} else if (securityLevelString.equals(LOW_SECURITY)) {
securityLevelLattice = BuiltinLattices.STD_SECLEVEL_LOW;
}
Collection<SDGProgramPart> allProgramParts =
analysis.getProgram().getAllProgramParts();
//Collection<SDGProgramPart> allProgramParts =
// analysis.getProgram().getAllProgramParts();
JSONObject description = jsonObj.getJSONObject(DESCR_CAT);
String from = description.getString(FROM);
//String from = description.getString(FROM);
Supplier<Collection<SDGNode>> nodeSupplier = null;
Supplier<Collection<SDGNode>> partSupplier = null;
String sdgNodeString = description.getString(SDG_NODE);
//Supplier<Collection<SDGNode>> partSupplier = null;
//String sdgNodeString = description.getString(SDG_NODE);
int sdgNodeId = description.getInt(SDG_NODE_ID);
nodeSupplier = () -> {
SDGNode node = analysis.getProgram().getSDG().getNode(sdgNodeId);
......@@ -320,6 +332,23 @@ public class CombinedApproach {
return new SingleAnnotationAdder(partSupplier, annoAddMethod,
securityLevelLattice);
}
/**
* perform an IFCAnalysis with the sdg graph given in pathToSDG.
* If this sdg file does not exists, a new {@link SDGProgram}, with a new {@link SDG} is generated.
* If a new {@link SDGProgram} is generated, because of the missing file, the node id's of the new graph can be different from
* the node id's of the sdg graph generated in the spec gui !
* This can be a problem if you have used the annotation with sdg nodes, in the spec gui.
* @param pathToJar String path to the jar file, created by the spec gui.
* @param pathToSDG String path to the SDG file, created by the spec gui.
* @param entryMethod
* @param stateSaverBuilder
* @return
* @throws ClassHierarchyException
* @throws IOException
* @throws UnsoundGraphException
* @throws CancelException
*/
public static IFCAnalysis
runJoanaCreateSDGAndIFCAnalyis(String pathToJar, String pathToSDG,
JavaMethodSignature entryMethod,
......@@ -334,30 +363,26 @@ public class CombinedApproach {
//TODO: write new methods for the two branches and catch empty sdg/saver files
if (sdg == null || !sdg.exists() || pathToSDG.isEmpty()) {
SDGConfig config =
new SDGConfig(pathToJar, entryMethod.toBCString(), Stubs.JRE_15);//TODO: does jre_15 works ?
new SDGConfig(pathToJar, entryMethod.toBCString(), Stubs.JRE_15);
config.setComputeInterferences(true);
config.setMhpType(MHPType.PRECISE);
config.setPointsToPrecision(PointsToPrecision.INSTANCE_BASED);
config.setExceptionAnalysis(ExceptionAnalysis.INTERPROC);
config.setFieldPropagation(FieldPropagation.OBJ_GRAPH_NO_MERGE_AT_ALL);
// save intermediate results of SDG generation points to call graph
config.setCGConsumer(stateSaverBuilder);
// Schneidet beim SDG application edges raus, so besser sichtbar mit dem graphviewer
config.setPruningPolicy(ApplicationLoaderPolicy.INSTANCE);
System.out.println("File not found: "+ pathToSDG);
//System.out.println("File not found: "+ pathToSDG);
program = SDGProgram.createSDGProgram(config, System.out,
new NullProgressMonitor());
} else {
program = SDGProgram.loadSDG(pathToSDG, MHPType.PRECISE);
System.out.println("SDG loaded from file "+ pathToSDG);
//System.out.println("SDG loaded from file "+ pathToSDG);
}
//TODO check if overloading or overriding methods ?!
//TODO check if some methods should be overwritten ?!
SDGAnalysis ana = new SDGAnalysis(program);
return ana;
}
private static String concatenatePaths(String firstPart, String secondPart) {
......
src/joanakey/SDGAnalysis.java
View file @ ed2a3ac2
/**
* This file is part of the Joana IFC project. It is developed at the
* Programming Paradigms Group of the Karlsruhe Institute of Technology.
*
* For further details on licensing please read the information at
* http://joana.ipd.kit.edu or contact the authors.
*/
package joanakey;
import java.util.Collection;
......@@ -26,14 +19,10 @@ import joanakey.annotations.SDGNodeAnnotation;
import joanakey.annotations.SDGNodeAnnotationManager;
/**
* Subclass of {@link IFCAnalysis} which also allows to annotate {@link SDGNode}s instead of only {@link SDGProgramPart}s.
* @author muessig.
*/
public class SDGAnalysis extends IFCAnalysis {
// private SDGNodeAnnotationManager sdgAnnManager;
// private SDGProgram program;
// private IFC<String> ifc;
// private IStaticLattice<String> secLattice;
/**
* @param program
......
src/joanakey/StateSaver.java
View file @ ed2a3ac2
......@@ -43,66 +43,7 @@ public class StateSaver {
private HashMap<SDGNode, PersistentCGNode> formalInsToPersistentCGNodes = new HashMap<>();
private TIntIntMap node2CG = null;
private TIntIntMap node2SSA = null;
// @Override
// public void consume(CallGraph callGraph,
// PointerAnalysis<? extends InstanceKey> pointerAnalyis) {
// this.callGraph = callGraph;
// this.pointerAnalyis = pointerAnalyis;
// }
// public static StateSaver generateFromJson(JSONObject jsonObj, SDG sdg)
// throws IOException {
// StateSaver stateSaver = new StateSaver();
//
// JSONArray formalNodeToCGNodeArr = jsonObj.getJSONArray(FORMAL_INS_TO_PERS_CG);
// for (int i = 0; i < formalNodeToCGNodeArr.length(); ++i) {
// JSONObject currentPair = formalNodeToCGNodeArr.getJSONObject(i);
// int sdgIndex = currentPair.getInt(SDG_NODE);
// JSONObject persistentCGNode = currentPair.getJSONObject(CG_NODE);
// SDGNode node = sdg.getNode(sdgIndex);
// stateSaver.formalInsToPersistentCGNodes.put(node,
// PersistentCGNode
// .generateFromJsonObj(persistentCGNode));
// }
//
// JSONArray cgNodeArr = jsonObj.getJSONArray(CG_NODE + "s");
// for (int i = 0; i < cgNodeArr.length(); ++i) {
// JSONObject currentCGNodeSaveObj = cgNodeArr.getJSONObject(i);
// PersistentCGNode currentPersistentCGNode =
// PersistentCGNode.generateFromJsonObj(currentCGNodeSaveObj);
// stateSaver.persistentCGNodes.add(currentPersistentCGNode);
// stateSaver.cgNodeIdToPersistentCGNodes.put(currentPersistentCGNode.getCgNodeId(),
// currentPersistentCGNode);
// }
//
// JSONArray pointerKeyArr = jsonObj.getJSONArray(LOCAL_POINTER_KEYS);
// for (int i = 0; i < pointerKeyArr.length(); ++i) {
// JSONObject currentPointerKeyJsonObj = pointerKeyArr.getJSONObject(i);
// PersistentLocalPointerKey currentLocalPointerKey =
// PersistentLocalPointerKey.generateFromJsonObj(currentPointerKeyJsonObj,
// stateSaver.persistentCGNodes);
// stateSaver.persistentLocalPointerKeys.add(currentLocalPointerKey);
// }
//
// JSONArray disjunctPointstoArr = jsonObj.getJSONArray(DISJUNCT_POINTS_TO);
// for (int i = 0; i < disjunctPointstoArr.length(); ++i) {
// JSONObject currentDisjObj = disjunctPointstoArr.getJSONObject(i);
// int key = currentDisjObj.getInt(KEY);
// JSONArray values = currentDisjObj.getJSONArray(VALUES);
// List<PersistentLocalPointerKey> disPointers = new ArrayList<>();
// for (int j = 0; j < values.length(); ++j) {
// int currDisIndex = values.getInt(j);
// disPointers.add(stateSaver.persistentLocalPointerKeys.get(currDisIndex));
// }
// PersistentLocalPointerKey keyPointerKey =
// stateSaver.persistentLocalPointerKeys.get(key);
// stateSaver.disjunctPointsToSets.put(keyPointerKey, disPointers);
// }
//
// return stateSaver;
// }
public CallGraph getCallGraph() {
return callGraph;
}
......
Markdown is supported
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