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

add prototype for collecting formal nodes (assertion generation)

parent 4553cad4
package assertions;
import javafx.stage.FileChooser;
public class FileHandler {
FileChooser chooser;
public FileHandler() {
chooser = new FileChooser();
}
public void chooseFile() {
chooser.showOpenDialog(ownerWindow)
}
}
package assertions;
import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.Map;
import edu.kit.joana.api.sdg.SDGMethod;
import edu.kit.joana.api.sdg.SDGProgram;
import edu.kit.joana.ifc.sdg.graph.SDG;
import edu.kit.joana.ifc.sdg.graph.SDGEdge;
import edu.kit.joana.ifc.sdg.graph.SDGNode;
public class FormalNodeCollector {
private static String TAB = " ";
private SDG sdg;
private Map<SDGNode, String> formalInMethodMap;
private Map<SDGNode, String> formalOutMethodMap;
public FormalNodeCollector(SDG sdg) {
this.sdg = sdg;
}
public void collectAllFormalNodesForProcedure() {
Map<SDGNode, String> allFormalInToMethod = new HashMap<SDGNode, String>();
Map<SDGNode, String> allFormalOutToMethod = new HashMap<SDGNode, String>();
ArrayList<SDGNode> listOfEntryNodes = new ArrayList<SDGNode>();
for (SDGNode n : sdg.vertexSet()) {
if (n.getKind() == SDGNode.Kind.ENTRY) {
listOfEntryNodes.add(n);
System.out.println(n.getLabel());
}
}
for (SDGNode entry : listOfEntryNodes) {
String entryName = entry.getLabel();
// for (SDGNode formIn : sdg.getFormalIns(entry)) {
for (SDGEdge e : sdg.edgesOf(entry)) {
SDGNode y = e.getTarget();
if (y.getKind() == SDGNode.Kind.FORMAL_IN) {
//TODO: use better filter for fields if possible ?
//The current solution only checks if the node has a dependency to the heap
if (sdg.hasIncomingEdgesOfKind(y, SDGEdge.Kind.DATA_HEAP)
|| sdg.hasOutgoingEdgesOfKind(y, SDGEdge.Kind.DATA_HEAP)) {
allFormalInToMethod.put(y, entryName);
}
}
if (y.getKind() == SDGNode.Kind.FORMAL_OUT) {
//TODO: use better filter for fields if possible ?
//The current solution only checks if the node has a dependency to the heap
if (sdg.hasIncomingEdgesOfKind(y, SDGEdge.Kind.DATA_HEAP)
|| sdg.hasOutgoingEdgesOfKind(y, SDGEdge.Kind.DATA_HEAP)) {
allFormalOutToMethod.put(y, entryName);
}
}
}
}
this.formalInMethodMap = allFormalInToMethod;
this.formalOutMethodMap = allFormalOutToMethod;
}
public String generateString() {
StringBuilder result = new StringBuilder();
ArrayList<String> setOfEntries = new ArrayList<String>();
for(String s : formalInMethodMap.values()) {
if (!setOfEntries.contains(s)) {
setOfEntries.add(s);
}
}
for (String s : setOfEntries) {
result.append(s + ": \n");
result.append(TAB+"formalIns: \n");
formalInMethodMap.forEach((node, value) -> {
if (value.equals(s)) {
result.append(TAB+TAB+node.getLabel()+"\n");
}
});
result.append("\n");
result.append(TAB+"formalOuts: \n");
formalOutMethodMap.forEach((node, value) -> {
if (value.equals(s)) {
result.append(TAB+TAB+node.getLabel()+"\n");
}
});
result.append("\n");
}
return result.toString();
}
}
package assertions;
import java.io.File;
import com.ibm.wala.ipa.cha.ClassHierarchyException;
import com.ibm.wala.util.CancelException;
import com.ibm.wala.util.graph.GraphIntegrity;
import com.ibm.wala.util.graph.GraphIntegrity.UnsoundGraphException;
import com.sun.org.apache.xalan.internal.xsltc.compiler.CompilerException;
import edu.kit.joana.ifc.sdg.graph.SDGSerializer;
import joanakey.customlistener.PreProcessor;
import joanakey.errorhandling.ErrorLogger;
import joanakey.slicing.ProgramSimplifier;
import joanakey.slicing.SourceCodeSlicer;
import specgui.helper.JarCreator;
import specgui.joanahandler.JoanaInstance;
import java.io.IOException;
import java.util.Collection;
import java.util.HashSet;
import java.util.Set;
import java.util.SortedSet;
import java.util.TreeSet;
import com.ibm.wala.ipa.callgraph.pruned.ApplicationLoaderPolicy;
import com.ibm.wala.ipa.cha.ClassHierarchyException;
import com.ibm.wala.util.CancelException;
import com.ibm.wala.util.NullProgressMonitor;
import com.ibm.wala.util.graph.GraphIntegrity;
import edu.kit.joana.api.IFCAnalysis;
import edu.kit.joana.api.sdg.SDGConfig;
import edu.kit.joana.api.sdg.SDGFormalParameter;
import edu.kit.joana.api.sdg.SDGMethod;
import edu.kit.joana.api.sdg.SDGProgram;
import edu.kit.joana.api.sdg.SDGProgramPart;
import edu.kit.joana.ifc.sdg.graph.SDG;
import edu.kit.joana.ifc.sdg.graph.SDGNode;
import edu.kit.joana.ifc.sdg.mhpoptimization.MHPType;
import edu.kit.joana.ifc.sdg.util.JavaMethodSignature;
import edu.kit.joana.util.Stubs;
import edu.kit.joana.wala.core.SDGBuilder;
import joanakey.SDGAnalysis;
import joanakey.StateSaver;
import joanakey.StateSaverCGConsumerBuilder;
import edu.kit.joana.api.sdg.SDGConfig;
import edu.kit.joana.api.sdg.SDGProgram;
import edu.kit.joana.ifc.sdg.mhpoptimization.MHPType;
import edu.kit.joana.ifc.sdg.util.JavaMethodSignature;
import joanakey.StateSaverCGConsumerBuilder;
public class SDGCreator {
private String currentMainMethod;
private String currentJarPath;
private SDGProgram program;
public SDGCreator(String mainMethod, String currentJarPath) {
this.currentMainMethod = mainMethod;
this.currentJarPath = currentJarPath;
}
/**
* create SDG program
* @param file
* @return true if sdg program generation was successful
*/
public boolean createSDGProgram() {
JavaMethodSignature entryMethod =
JavaMethodSignature.mainMethodOfClass(currentMainMethod);
SDGConfig config =
new SDGConfig(currentJarPath, entryMethod.toBCString(),
Stubs.JRE_15); //changed from JRE_14 to JRE_15
config.setComputeInterferences(true);
config.setMhpType(MHPType.PRECISE);
config.setPointsToPrecision(SDGBuilder.PointsToPrecision.INSTANCE_BASED);
config.setExceptionAnalysis(SDGBuilder.ExceptionAnalysis.INTERPROC);
config.setFieldPropagation(SDGBuilder.FieldPropagation.OBJ_GRAPH_NO_MERGE_AT_ALL);
// save intermediate results of SDG generation points to call graph
// config.setCGConsumer(null);
// Schneidet beim SDG application edges raus, so besser sichtbar mit dem graphviewer
config.setPruningPolicy(ApplicationLoaderPolicy.INSTANCE);
SDGProgram program = null;
boolean success = false;
try {
program = SDGProgram.createSDGProgram(config, System.out,
new NullProgressMonitor());
success = true;
} catch (ClassHierarchyException e) {
// TODO Auto-generated catch block
e.printStackTrace();
} catch (IOException e) {
// TODO Auto-generated catch block
e.printStackTrace();
} catch (UnsoundGraphException e) {
// TODO Auto-generated catch block
e.printStackTrace();
} catch (CancelException e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
this.program = program;
if (success) {
return true;
} else {
return false;
}
}
public SDG getSDG() {
return program.getSDG();
}
public Collection<SDGMethod> getAllSDGMethods() {
return program.getAllMethods();
}
}
package assertions;
import java.io.File;
public class start {
public static void main(String[] args) {
String mainMethod = "IFLoop";
String currentJarPath ="testdata/jUnitData/CallGraph/testdata/build/src.jar";
// "home/joachim/JoanaKeYBeispiele/SecureExamples/IFLoop/program/testdata/build/src.jar";
File f = new File(currentJarPath);
System.out.println((f.exists()));
SDGCreator creator = new SDGCreator(mainMethod, currentJarPath);
creator.createSDGProgram();
FormalNodeCollector collector = new FormalNodeCollector(creator.getSDG());
collector.collectAllFormalNodesForProcedure();
String result = collector.generateString();
System.out.println("result: \n");
System.out.println(result);
}
}
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