From b545fa532ad90750f5e71c42b970e94278e689c4 Mon Sep 17 00:00:00 2001 From: kylekim72 <133502080+kylekim72@users.noreply.github.com> Date: Mon, 3 Jun 2024 22:50:52 +0900 Subject: [PATCH 01/31] Update README.md A test PR for gradle-build branch. Please reject this. --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index ee288b968..36a96129a 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,4 @@ +# PR by Kyle, please reject this # Symbolic PathFinder (SPF) ![build SPF](https://github.com/gaurangkudale/SPF/actions/workflows/main.yml/badge.svg) From 8199510e76eeb1f3a508fce293a33ef5a0d3def6 Mon Sep 17 00:00:00 2001 From: kylekim72 <133502080+kylekim72@users.noreply.github.com> Date: Mon, 3 Jun 2024 22:55:26 +0900 Subject: [PATCH 02/31] Update README.md --- README.md | 1 - 1 file changed, 1 deletion(-) diff --git a/README.md b/README.md index 36a96129a..ee288b968 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,3 @@ -# PR by Kyle, please reject this # Symbolic PathFinder (SPF) ![build SPF](https://github.com/gaurangkudale/SPF/actions/workflows/main.yml/badge.svg) From 947685b89231eb41452aeb07d864b7f7cc28a35d Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Wed, 14 Aug 2024 20:44:00 +0900 Subject: [PATCH 03/31] Adding witness generation to SymbolicListener GSoC 2024 project --- .../gov/nasa/jpf/symbc/SymbolicListener.java | 273 ++++++++++++++++-- 1 file changed, 244 insertions(+), 29 deletions(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java index c3e9128cc..fb24a8510 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java @@ -21,15 +21,9 @@ import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; import gov.nasa.jpf.PropertyListenerAdapter; -import gov.nasa.jpf.vm.ChoiceGenerator; -import gov.nasa.jpf.vm.ClassInfo; -import gov.nasa.jpf.vm.Instruction; -import gov.nasa.jpf.vm.LocalVarInfo; -import gov.nasa.jpf.vm.MethodInfo; -import gov.nasa.jpf.vm.StackFrame; -import gov.nasa.jpf.vm.ThreadInfo; -import gov.nasa.jpf.vm.Types; -import gov.nasa.jpf.vm.VM; +import gov.nasa.jpf.symbc.numeric.*; +import gov.nasa.jpf.symbc.numeric.Comparator; +import gov.nasa.jpf.vm.*; import gov.nasa.jpf.jvm.bytecode.ARETURN; import gov.nasa.jpf.jvm.bytecode.DRETURN; @@ -46,28 +40,15 @@ import gov.nasa.jpf.symbc.bytecode.INVOKESTATIC; import gov.nasa.jpf.symbc.concolic.PCAnalyzer; -import gov.nasa.jpf.symbc.numeric.Comparator; -import gov.nasa.jpf.symbc.numeric.Expression; -import gov.nasa.jpf.symbc.numeric.IntegerConstant; -import gov.nasa.jpf.symbc.numeric.IntegerExpression; -import gov.nasa.jpf.symbc.numeric.PCChoiceGenerator; -import gov.nasa.jpf.symbc.numeric.PathCondition; -import gov.nasa.jpf.symbc.numeric.RealConstant; -import gov.nasa.jpf.symbc.numeric.RealExpression; -import gov.nasa.jpf.symbc.numeric.SymbolicInteger; -import gov.nasa.jpf.symbc.numeric.SymbolicReal; - -import gov.nasa.jpf.symbc.numeric.SymbolicConstraintsGeneral; //import gov.nasa.jpf.symbc.numeric.SymbolicInteger; import gov.nasa.jpf.util.Pair; +import org.apache.commons.lang.ObjectUtils; -import java.io.PrintWriter; -import java.util.HashMap; -import java.util.Iterator; -import java.util.Map; -import java.util.StringTokenizer; -import java.util.Vector; +import java.io.*; +import java.util.*; +import java.util.regex.Matcher; +import java.util.regex.Pattern; public class SymbolicListener extends PropertyListenerAdapter implements PublisherExtension { @@ -118,11 +99,147 @@ public SymbolicListener(Config conf, JPF jpf) { // } catch (Exception e) { // } // } + public static class VerifierInfo{ + private final int lineNumber; + private final String returnType; + + private final String varName; + + private Object varValue = null; + + public VerifierInfo(int lineNumber, String returnType, String varName){ + this.lineNumber = lineNumber; + this.returnType = returnType; + this.varName = varName; + } + } + + // A list to save line number and return type + private List verifierInfoList = new ArrayList<>(); + + // Integrate two + + private String nodeWriter(int length, boolean noCounterExample){ + String node = "\n"; + // If there is no symbolic variable, generate empty witness + if(length == 0 || noCounterExample){ + node += String.format(" \n", 0); + node += " true true\n"; + node += " "; + return node; + } + node += String.format(" \n", 0); + node += " true\n"; + node += " \n"; + for(int i = 0; i", i+1); + //System.out.println(nodeId); + nodeId += System.lineSeparator(); + if(i == verifierInfoList.size()-1){ + nodeId += " true"; + nodeId += System.lineSeparator(); + } + nodeId += " "; + nodeId += System.lineSeparator(); + node += nodeId; + } + return node; + } + private String edgeWriter(int length, String fileName){ + // later, I have to handle the case when length == 0 and string type for assumption + String edge = ""; + for(int i=0; i\n", i, i+1); + //edgeId += System.lineSeparator(); + edgeId += String.format(" %s.java\n", fileName); + //edgeId += System.lineSeparator(); + edgeId += String.format(" %d\n", verifierInfoList.get(i).lineNumber); + // If variable value is null, it means that this variable doesn't appear in PC + // (i.e. it doesn't matters program's correctness. In this case, just put arbitrary default value) + if(verifierInfoList.get(i).returnType.equals("double") || verifierInfoList.get(i).returnType.equals("float")){ + if(verifierInfoList.get(i).varValue == null) edgeId += String.format(" %s == %f\n", verifierInfoList.get(i).varName, 2.0); + else edgeId += String.format(" %s == %f\n", verifierInfoList.get(i).varName, verifierInfoList.get(i).varValue); + } + + else if(verifierInfoList.get(i).returnType.equals("boolean")){ + if(verifierInfoList.get(i).varValue == null) edgeId += String.format(" %s == %b\n", verifierInfoList.get(i).varName, false); + else edgeId += String.format(" %s == %b\n", verifierInfoList.get(i).varName, verifierInfoList.get(i).varValue); + } + else if(verifierInfoList.get(i).returnType.equals("java.lang.String")){ + if(verifierInfoList.get(i).varValue == null) edgeId += String.format(" %s == %s\n", verifierInfoList.get(i).varName, "\"\""); + else edgeId += String.format(" %s == %s\n", verifierInfoList.get(i).varName, verifierInfoList.get(i).varValue); + } + + else{ + // Use == to follow standard graphml format + if(verifierInfoList.get(i).varValue == null) edgeId += String.format(" %s == %d\n", verifierInfoList.get(i).varName, 4); + else edgeId += String.format(" %s == %d\n", verifierInfoList.get(i).varName, verifierInfoList.get(i).varValue); + } + //edgeId += System.lineSeparator(); + edgeId += String.format(" java::L%s;\n", assumptionScope); + //edgeId += System.lineSeparator(); + edgeId += " \n"; + edge += edgeId; + } + return edge; + } + private void parseSymVar(String pathCondition){ + // Currently not handling String type + // Extract variable name and value + Pattern pattern = Pattern.compile("(\\w+)\\[(-?\\d+(\\.\\d+)?([eE][-+]?\\d+)?)\\]"); + Matcher matcher = pattern.matcher(pathCondition); + + + // Insert value to list + while (matcher.find()) { + String pcVariableName = matcher.group(1); + String pcVariableValue = matcher.group(2); + // There are 3 cases, real number, string and other numeric types + if (pcVariableName.contains("double") || pcVariableName.contains("float") || pcVariableName.contains("REAL")) { + double value = Double.parseDouble(pcVariableValue); // 실수로 파싱 + for(int i=0; i cg = vm.getChoiceGenerator(); if (!(cg instanceof PCChoiceGenerator)) { @@ -132,6 +249,25 @@ public void propertyViolated(Search search) { } cg = prev_cg; } + try (BufferedReader reader = new BufferedReader(new FileReader(inputFilePath)); + FileWriter writer = new FileWriter(outputFilePath)){ + String line; + while ((line = reader.readLine()) != null) { + //System.out.println(line); + writer.write(line); + writer.write(System.lineSeparator()); + } + // + String witnessNode = nodeWriter(verifierInfoList.size(), true); + writer.write(witnessNode); + writer.write(System.lineSeparator()); + + // wrap-up the witness file + writer.write( System.lineSeparator() + " " + System.lineSeparator()); + writer.write("" + System.lineSeparator()); + }catch (IOException e){ + System.out.println("IOException detected: " + e.getMessage()); + } if ((cg instanceof PCChoiceGenerator) && ((PCChoiceGenerator) cg).getCurrentPC() != null) { PathCondition pc = ((PCChoiceGenerator) cg).getCurrentPC(); String error = search.getLastError().getDetails(); @@ -158,13 +294,58 @@ public void propertyViolated(Search search) { methodSummary = new MethodSummary(); methodSummary.addPathCondition(pcPair); allSummaries.put(currentMethodName, methodSummary); + //System.out.println(verifierInfoList.get(0).lineNumber); + //System.out.println(verifierInfoList.get(0).returnType); + String strPathCondition = pc.toString(); + //List temp = parsePC(strPathCondition); System.out.println("Property Violated: PC is " + pc.toString()); System.out.println("Property Violated: result is " + error); System.out.println("****************************"); + + + + + try (BufferedReader reader = new BufferedReader(new FileReader(inputFilePath)); + FileWriter writer = new FileWriter(outputFilePath)) { + String line; + while ((line = reader.readLine()) != null) { + //System.out.println(line); + writer.write(line); + writer.write(System.lineSeparator()); + } + // node part + String witnessNode = nodeWriter(verifierInfoList.size(), false); + //System.out.println(witnessNode); + writer.write(witnessNode); + writer.write(System.lineSeparator()); + + // edge part, match symbolic variable's value + parseSymVar(strPathCondition); + String edges = edgeWriter(verifierInfoList.size(), fileName); + writer.write(edges); + writer.write(System.lineSeparator()); + // wrap-up the witness file + writer.write( System.lineSeparator() + " " + System.lineSeparator()); + writer.write("" + System.lineSeparator()); + } catch (IOException e) { + System.out.println("IOException detected: " + e.getMessage()); + //e.printStackTrace(); + } } // } } + boolean interceptSymbolic = false; + boolean fileNameParsed = false; + String fileName = ""; + String assumptionScope = ""; + // 3 informations about nodeterministic variable + // generated by invocation of Verifier.nondet~~ + // initialization + int symLineNumber = 0; + String symRetrunType = ""; + String symVarName = ""; + @Override public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nextInstruction, Instruction executedInstruction) { @@ -174,7 +355,21 @@ public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nex // SystemState ss = vm.getSystemState(); ThreadInfo ti = currentThread; Config conf = vm.getConfig(); + String strInsn = executedInstruction.toString(); + //System.out.println(strInsn); + // Debug.makeSymbolic + if(strInsn.contains("invokestatic") && strInsn.contains("Verifier.nondet")){ + interceptSymbolic = true; + } + if(!fileNameParsed){ + ApplicationContext app = ti.getApplicationContext(); + String className = app.getMainClassName(); + String[] parts = className.split("\\."); + fileName = parts[parts.length - 1]; + assumptionScope = String.join(".", parts); + fileNameParsed = true; + } if (insn instanceof JVMInvokeInstruction) { JVMInvokeInstruction md = (JVMInvokeInstruction) insn; String methodName = md.getInvokedMethodName(); @@ -184,15 +379,23 @@ public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nex ClassInfo ci = mi.getClassInfo(); String className = ci.getName(); + StackFrame sf = ti.getTopFrame(); String shortName = methodName; String longName = mi.getLongName(); if (methodName.contains("(")) shortName = methodName.substring(0, methodName.indexOf("(")); - + if(methodName.contains("Symbolic")){ + String mn = md.getInvokedMethodName(); + } if (!mi.equals(sf.getMethodInfo())) return; - + // catch the invokestatic.Verifier.nondet~~ + // and store the line number and type + if(className.contains("Verifier") && methodName.contains("nondet")){ + symLineNumber = md.getLineNumber(); + symRetrunType = md.getReturnTypeName(); + } if ((BytecodeUtils.isClassSymbolic(conf, className, mi, methodName)) || BytecodeUtils.isMethodSymbolic(conf, mi.getFullName(), numberOfArgs, null)) { @@ -265,6 +468,18 @@ public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nex String longName = mi.getLongName(); int numberOfArgs = mi.getNumberOfArguments(); + StackFrame sf = ti.getTopFrame(); + Object symbolicVar = sf.getOperandAttr(); + + if(interceptSymbolic && strInsn.contains("nativereturn") && strInsn.contains("makeSymbolic")){ + symVarName = symbolicVar.toString(); + VerifierInfo Info = new VerifierInfo(symLineNumber, symRetrunType, symVarName); + verifierInfoList.add(Info); + symLineNumber = 0; + symRetrunType = ""; + symVarName = ""; + } + if (((BytecodeUtils.isClassSymbolic(conf, className, mi, methodName)) || BytecodeUtils.isMethodSymbolic(conf, mi.getFullName(), numberOfArgs, null))) { From 3c0ef5fd1fa2fb64d4e24f5553d93612b95f084c Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Wed, 14 Aug 2024 20:54:40 +0900 Subject: [PATCH 04/31] Change Verifier.randomBool() to Debug.makeSymbolicBoolean to generate witness --- .../src/classes/org/sosy_lab/sv_benchmarks/Verifier.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/jpf-symbc/src/classes/org/sosy_lab/sv_benchmarks/Verifier.java b/jpf-symbc/src/classes/org/sosy_lab/sv_benchmarks/Verifier.java index 202081651..8a1464ba0 100644 --- a/jpf-symbc/src/classes/org/sosy_lab/sv_benchmarks/Verifier.java +++ b/jpf-symbc/src/classes/org/sosy_lab/sv_benchmarks/Verifier.java @@ -22,8 +22,8 @@ public static void assume(boolean condition) { } public static boolean nondetBoolean() { - //return Debug.makeSymbolicBoolean("bool"+counter++); - return Verify.randomBool(); + return Debug.makeSymbolicBoolean("bool"+counter++); + //return Verify.randomBool(); } public static byte nondetByte() { From 657447734dc5cbe14a0b34493fc3d378f320b416 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Wed, 14 Aug 2024 20:57:58 +0900 Subject: [PATCH 05/31] Adding witness generation to SymbolicListener GSoC 2024 project --- .../witness_template/witness_template.txt | 48 +++++++++++++++++++ .../witness_template_minimal.txt | 17 +++++++ 2 files changed, 65 insertions(+) create mode 100644 jpf-symbc/witness_template/witness_template.txt create mode 100644 jpf-symbc/witness_template/witness_template_minimal.txt diff --git a/jpf-symbc/witness_template/witness_template.txt b/jpf-symbc/witness_template/witness_template.txt new file mode 100644 index 000000000..5215a1c25 --- /dev/null +++ b/jpf-symbc/witness_template/witness_template.txt @@ -0,0 +1,48 @@ + + + + <command-line> + + + + + false + + + false + + + false + + + false + + + false + + + 0 + + + 0 + + + + + + + + + + + + + + + + + violation_witness + + + + true diff --git a/jpf-symbc/witness_template/witness_template_minimal.txt b/jpf-symbc/witness_template/witness_template_minimal.txt new file mode 100644 index 000000000..2fcd42709 --- /dev/null +++ b/jpf-symbc/witness_template/witness_template_minimal.txt @@ -0,0 +1,17 @@ + + + + <command-line> + + + false + + + false + + + + + + + SPF From a9b664e76e9f478e3f67ce4ff073990950518ad1 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Wed, 14 Aug 2024 21:00:46 +0900 Subject: [PATCH 06/31] Adding witness generation to SymbolicListener GSoC 2024 project --- jpf-symbc/witness_template/witness_template.txt | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/jpf-symbc/witness_template/witness_template.txt b/jpf-symbc/witness_template/witness_template.txt index 5215a1c25..cb48ccad0 100644 --- a/jpf-symbc/witness_template/witness_template.txt +++ b/jpf-symbc/witness_template/witness_template.txt @@ -41,8 +41,4 @@ - violation_witness - - - - true + SPF From 2ae9d6c4ec03716eae46af9ae2fa34142410f868 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sat, 17 Aug 2024 23:00:55 +0900 Subject: [PATCH 07/31] Adding additional header and key to be able to run on gwit --- jpf-symbc/witness_template/witness_template_minimal.txt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/jpf-symbc/witness_template/witness_template_minimal.txt b/jpf-symbc/witness_template/witness_template_minimal.txt index 2fcd42709..5081043be 100644 --- a/jpf-symbc/witness_template/witness_template_minimal.txt +++ b/jpf-symbc/witness_template/witness_template_minimal.txt @@ -13,5 +13,7 @@ + + violation_witness SPF From ed96270d76cec8c76eaf9236b0d93bdd24694cc9 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 15:56:40 +0900 Subject: [PATCH 08/31] Moved to src/main/resources --- .../witness_template/witness_template.txt | 44 ------------------- .../witness_template_minimal.txt | 19 -------- 2 files changed, 63 deletions(-) delete mode 100644 jpf-symbc/witness_template/witness_template.txt delete mode 100644 jpf-symbc/witness_template/witness_template_minimal.txt diff --git a/jpf-symbc/witness_template/witness_template.txt b/jpf-symbc/witness_template/witness_template.txt deleted file mode 100644 index cb48ccad0..000000000 --- a/jpf-symbc/witness_template/witness_template.txt +++ /dev/null @@ -1,44 +0,0 @@ - - - - <command-line> - - - - - false - - - false - - - false - - - false - - - false - - - 0 - - - 0 - - - - - - - - - - - - - - - - - SPF diff --git a/jpf-symbc/witness_template/witness_template_minimal.txt b/jpf-symbc/witness_template/witness_template_minimal.txt deleted file mode 100644 index 5081043be..000000000 --- a/jpf-symbc/witness_template/witness_template_minimal.txt +++ /dev/null @@ -1,19 +0,0 @@ - - - - <command-line> - - - false - - - false - - - - - - - - violation_witness - SPF From 2ffdab4656fa4f7a5c268e1fdf3ea5a11f365e8e Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 15:57:38 +0900 Subject: [PATCH 09/31] Add template for witness generation --- .../witness_template/witness_template.txt | 44 +++++++++++++++++++ .../witness_template_minimal.txt | 19 ++++++++ 2 files changed, 63 insertions(+) create mode 100644 jpf-symbc/src/main/resources/witness_template/witness_template.txt create mode 100644 jpf-symbc/src/main/resources/witness_template/witness_template_minimal.txt diff --git a/jpf-symbc/src/main/resources/witness_template/witness_template.txt b/jpf-symbc/src/main/resources/witness_template/witness_template.txt new file mode 100644 index 000000000..cb48ccad0 --- /dev/null +++ b/jpf-symbc/src/main/resources/witness_template/witness_template.txt @@ -0,0 +1,44 @@ + + + + <command-line> + + + + + false + + + false + + + false + + + false + + + false + + + 0 + + + 0 + + + + + + + + + + + + + + + + + SPF diff --git a/jpf-symbc/src/main/resources/witness_template/witness_template_minimal.txt b/jpf-symbc/src/main/resources/witness_template/witness_template_minimal.txt new file mode 100644 index 000000000..5081043be --- /dev/null +++ b/jpf-symbc/src/main/resources/witness_template/witness_template_minimal.txt @@ -0,0 +1,19 @@ + + + + <command-line> + + + false + + + false + + + + + + + + violation_witness + SPF From 022c68233ad80414e84da3360849619b4eb8d921 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 16:00:47 +0900 Subject: [PATCH 10/31] Adding witness generation to SymbolicListener GSoC 2024 project --- .../gov/nasa/jpf/symbc/SymbolicListener.java | 242 +++++------------- 1 file changed, 64 insertions(+), 178 deletions(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java index fb24a8510..984c49d93 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java @@ -16,6 +16,38 @@ * limitations under the License. */ +/** + * v.nasa.jpf.symbc.witness package + * + * Edge edge = new Edge(Node node1, Node node2); + * edges.toString() + * * node1.toString() + * node2.toString() + * + * + * class GraphMl + * boolean allowMethodAssumptions = false; + * graphml.toString() + * template + * edges.print(allowMethodAssumptions) + * node.toString + * graphml.serialize() + * String witnessStr = graphml.toString() + * printToWitnessFile(witnessStr) + * + * classes + * Node : toString/Serialize method + * Edge + * GraphMl + * + * + * SymbolicListener + * Edge edge = new Edge(Node node1, Node node2); + * GraphMl graphml = new GraphMl(List edges) + * graphml.serialize(); + * + */ + package gov.nasa.jpf.symbc; import gov.nasa.jpf.Config; @@ -39,11 +71,15 @@ import gov.nasa.jpf.symbc.bytecode.BytecodeUtils; import gov.nasa.jpf.symbc.bytecode.INVOKESTATIC; import gov.nasa.jpf.symbc.concolic.PCAnalyzer; +import gov.nasa.jpf.symbc.witness.SymbolicVariableInfo; +import gov.nasa.jpf.symbc.witness.Node; +import gov.nasa.jpf.symbc.witness.Edge; +import gov.nasa.jpf.symbc.witness.GraphML; +import gov.nasa.jpf.symbc.witness.PathConditionParser; //import gov.nasa.jpf.symbc.numeric.SymbolicInteger; import gov.nasa.jpf.util.Pair; -import org.apache.commons.lang.ObjectUtils; import java.io.*; import java.util.*; @@ -99,137 +135,14 @@ public SymbolicListener(Config conf, JPF jpf) { // } catch (Exception e) { // } // } - public static class VerifierInfo{ - private final int lineNumber; - private final String returnType; - - private final String varName; - - private Object varValue = null; - public VerifierInfo(int lineNumber, String returnType, String varName){ - this.lineNumber = lineNumber; - this.returnType = returnType; - this.varName = varName; - } - } // A list to save line number and return type - private List verifierInfoList = new ArrayList<>(); - - // Integrate two - - private String nodeWriter(int length, boolean noCounterExample){ - String node = "\n"; - // If there is no symbolic variable, generate empty witness - if(length == 0 || noCounterExample){ - node += String.format(" \n", 0); - node += " true true\n"; - node += " "; - return node; - } - node += String.format(" \n", 0); - node += " true\n"; - node += " \n"; - for(int i = 0; i", i+1); - //System.out.println(nodeId); - nodeId += System.lineSeparator(); - if(i == verifierInfoList.size()-1){ - nodeId += " true"; - nodeId += System.lineSeparator(); - } - nodeId += " "; - nodeId += System.lineSeparator(); - node += nodeId; - } - return node; - } - private String edgeWriter(int length, String fileName){ - // later, I have to handle the case when length == 0 and string type for assumption - String edge = ""; - for(int i=0; i\n", i, i+1); - //edgeId += System.lineSeparator(); - edgeId += String.format(" %s.java\n", fileName); - //edgeId += System.lineSeparator(); - edgeId += String.format(" %d\n", verifierInfoList.get(i).lineNumber); - // If variable value is null, it means that this variable doesn't appear in PC - // (i.e. it doesn't matters program's correctness. In this case, just put arbitrary default value) - if(verifierInfoList.get(i).returnType.equals("double") || verifierInfoList.get(i).returnType.equals("float")){ - if(verifierInfoList.get(i).varValue == null) edgeId += String.format(" %s == %f\n", verifierInfoList.get(i).varName, 2.0); - else edgeId += String.format(" %s == %f\n", verifierInfoList.get(i).varName, verifierInfoList.get(i).varValue); - } + public List symbolicVariableInfoList = new ArrayList<>(); - else if(verifierInfoList.get(i).returnType.equals("boolean")){ - if(verifierInfoList.get(i).varValue == null) edgeId += String.format(" %s == %b\n", verifierInfoList.get(i).varName, false); - else edgeId += String.format(" %s == %b\n", verifierInfoList.get(i).varName, verifierInfoList.get(i).varValue); - } - else if(verifierInfoList.get(i).returnType.equals("java.lang.String")){ - if(verifierInfoList.get(i).varValue == null) edgeId += String.format(" %s == %s\n", verifierInfoList.get(i).varName, "\"\""); - else edgeId += String.format(" %s == %s\n", verifierInfoList.get(i).varName, verifierInfoList.get(i).varValue); - } + boolean allowMethodInvocation = false; - else{ - // Use == to follow standard graphml format - if(verifierInfoList.get(i).varValue == null) edgeId += String.format(" %s == %d\n", verifierInfoList.get(i).varName, 4); - else edgeId += String.format(" %s == %d\n", verifierInfoList.get(i).varName, verifierInfoList.get(i).varValue); - } - //edgeId += System.lineSeparator(); - edgeId += String.format(" java::L%s;\n", assumptionScope); - //edgeId += System.lineSeparator(); - edgeId += " \n"; - edge += edgeId; - } - return edge; - } - private void parseSymVar(String pathCondition){ - // Currently not handling String type - // Extract variable name and value - Pattern pattern = Pattern.compile("(\\w+)\\[(-?\\d+(\\.\\d+)?([eE][-+]?\\d+)?)\\]"); - Matcher matcher = pattern.matcher(pathCondition); - - - // Insert value to list - while (matcher.find()) { - String pcVariableName = matcher.group(1); - String pcVariableValue = matcher.group(2); - // There are 3 cases, real number, string and other numeric types - if (pcVariableName.contains("double") || pcVariableName.contains("float") || pcVariableName.contains("REAL")) { - double value = Double.parseDouble(pcVariableValue); // 실수로 파싱 - for(int i=0; i" + System.lineSeparator()); - writer.write("" + System.lineSeparator()); - }catch (IOException e){ - System.out.println("IOException detected: " + e.getMessage()); - } + + Node nodeForEmptyWitness = new Node(1, 0, true); + String strNode = nodeForEmptyWitness.serializeNode(); + GraphML emptyWitness = new GraphML(inputFilePath, outputFilePath); + String headerForEmptyWitness = emptyWitness.constructHeader(); + emptyWitness.serializeEmptyWitness(strNode, headerForEmptyWitness); + if ((cg instanceof PCChoiceGenerator) && ((PCChoiceGenerator) cg).getCurrentPC() != null) { PathCondition pc = ((PCChoiceGenerator) cg).getCurrentPC(); String error = search.getLastError().getDetails(); @@ -294,43 +195,28 @@ public void propertyViolated(Search search) { methodSummary = new MethodSummary(); methodSummary.addPathCondition(pcPair); allSummaries.put(currentMethodName, methodSummary); - //System.out.println(verifierInfoList.get(0).lineNumber); - //System.out.println(verifierInfoList.get(0).returnType); + String strPathCondition = pc.toString(); - //List temp = parsePC(strPathCondition); + System.out.println("Property Violated: PC is " + pc.toString()); System.out.println("Property Violated: result is " + error); System.out.println("****************************"); - - try (BufferedReader reader = new BufferedReader(new FileReader(inputFilePath)); - FileWriter writer = new FileWriter(outputFilePath)) { - String line; - while ((line = reader.readLine()) != null) { - //System.out.println(line); - writer.write(line); - writer.write(System.lineSeparator()); - } - // node part - String witnessNode = nodeWriter(verifierInfoList.size(), false); - //System.out.println(witnessNode); - writer.write(witnessNode); - writer.write(System.lineSeparator()); - - // edge part, match symbolic variable's value - parseSymVar(strPathCondition); - String edges = edgeWriter(verifierInfoList.size(), fileName); - writer.write(edges); - writer.write(System.lineSeparator()); - // wrap-up the witness file - writer.write( System.lineSeparator() + " " + System.lineSeparator()); - writer.write("" + System.lineSeparator()); - } catch (IOException e) { - System.out.println("IOException detected: " + e.getMessage()); - //e.printStackTrace(); + List nodeList = new ArrayList<>(); + List edgeList = new ArrayList<>(); + PathConditionParser parser = new PathConditionParser(); + parser.parseSymVar(strPathCondition, symbolicVariableInfoList); + for(int i=0; i Date: Sun, 25 Aug 2024 16:01:20 +0900 Subject: [PATCH 11/31] Adding package for witness generation GSoC 2024 project --- .../main/gov/nasa/jpf/symbc/witness/Edge.java | 77 +++++++++++++++++++ .../gov/nasa/jpf/symbc/witness/GraphML.java | 67 ++++++++++++++++ .../main/gov/nasa/jpf/symbc/witness/Node.java | 48 ++++++++++++ .../symbc/witness/PathConditionParser.java | 65 ++++++++++++++++ .../symbc/witness/SymbolicVariableInfo.java | 21 +++++ 5 files changed, 278 insertions(+) create mode 100644 jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Edge.java create mode 100644 jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java create mode 100644 jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java create mode 100644 jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/PathConditionParser.java create mode 100644 jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/SymbolicVariableInfo.java diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Edge.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Edge.java new file mode 100644 index 000000000..5c9b3aac8 --- /dev/null +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Edge.java @@ -0,0 +1,77 @@ +package gov.nasa.jpf.symbc.witness; + +import java.util.List; + + +public class Edge{ + public int indexOfEdge; + public String fileName; + + public List symbolicVariableInfoList; + + public String assumptionScope; + + public boolean allowMethodInvocation; + + public Edge(int indexOfEdge, String fileName, List symbolicVariableInfoList, boolean allowMethodInvocation, String assumptionScope){ + this.indexOfEdge = indexOfEdge; + this.fileName = fileName; + this.symbolicVariableInfoList = symbolicVariableInfoList; + this.allowMethodInvocation = allowMethodInvocation; + this.assumptionScope = assumptionScope; + } + private String serializeEdge(){ + // later, I have to handle the case when length == 0 and string type for assumption + StringBuilder edgeBuilder = new StringBuilder(); + edgeBuilder.append(String.format(" \n", indexOfEdge, indexOfEdge+1)); + //edgeId += System.lineSeparator(); + edgeBuilder.append(String.format(" %s.java\n", fileName)); + //edgeId += System.lineSeparator(); + edgeBuilder.append(String.format(" %d\n", symbolicVariableInfoList.get(indexOfEdge).lineNumber)); + // If variable value is null, it means that this variable doesn't appear in PC + // (i.e. it doesn't matters program's correctness. In this case, just put arbitrary default value) + if(symbolicVariableInfoList.get(indexOfEdge).returnType.equals("double") || + symbolicVariableInfoList.get(indexOfEdge).returnType.equals("float")){ + if(symbolicVariableInfoList.get(indexOfEdge).varValue == null) { + edgeBuilder.append(String.format(" %s == %f\n", symbolicVariableInfoList.get(indexOfEdge).varName, 2.0)); + } + else edgeBuilder.append(String.format(" %s == %f\n", symbolicVariableInfoList.get(indexOfEdge).varName, symbolicVariableInfoList.get(indexOfEdge).varValue)); + } + + else if(symbolicVariableInfoList.get(indexOfEdge).returnType.equals("boolean")){ + if(symbolicVariableInfoList.get(indexOfEdge).varValue == null) edgeBuilder.append(String.format(" %s == %b\n", symbolicVariableInfoList.get(indexOfEdge).varName, false)); + else edgeBuilder.append(String.format(" %s == %b\n", symbolicVariableInfoList.get(indexOfEdge).varName, symbolicVariableInfoList.get(indexOfEdge).varValue)); + } + + else if(symbolicVariableInfoList.get(indexOfEdge).returnType.equals("java.lang.String")){ + if(allowMethodInvocation){ + if(symbolicVariableInfoList.get(indexOfEdge).varValue == null) edgeBuilder.append(String.format(" %s.equals(%s)\n", symbolicVariableInfoList.get(indexOfEdge).varName, "\"\"")); + else edgeBuilder.append(String.format(" %s.equals(%s)\n", symbolicVariableInfoList.get(indexOfEdge).varName,symbolicVariableInfoList.get(indexOfEdge).varValue)); + } + else{ + if(symbolicVariableInfoList.get(indexOfEdge).varValue == null) edgeBuilder.append(String.format(" %s==%s\n", symbolicVariableInfoList.get(indexOfEdge).varName, "\"\"")); + else edgeBuilder.append(String.format(" %s==%s\n", symbolicVariableInfoList.get(indexOfEdge).varName, symbolicVariableInfoList.get(indexOfEdge).varValue)); + } + } + + else{ + // Use == to follow standard graphml format + if(symbolicVariableInfoList.get(indexOfEdge).varValue == null) edgeBuilder.append(String.format(" %s == %d\n", symbolicVariableInfoList.get(indexOfEdge).varName, 4)); + else edgeBuilder.append(String.format(" %s == %d\n", symbolicVariableInfoList.get(indexOfEdge).varName, symbolicVariableInfoList.get(indexOfEdge).varValue)); + } + + edgeBuilder.append(String.format(" java::L%s;\n", assumptionScope)); + + edgeBuilder.append(" \n"); + return edgeBuilder.toString(); + } + + public static String serializeAllEdges(List edgeList){ + StringBuilder allEdgesBuilder = new StringBuilder(); + for(Edge edge : edgeList){ + allEdgesBuilder.append(edge.serializeEdge()); + } + return allEdgesBuilder.toString(); + } + +} \ No newline at end of file diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java new file mode 100644 index 000000000..d56a072f0 --- /dev/null +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java @@ -0,0 +1,67 @@ +package gov.nasa.jpf.symbc.witness; + +import java.io.BufferedReader; +import java.io.FileReader; +import java.io.FileWriter; +import java.io.IOException; +import java.util.List; + + +public class GraphML{ + public String inputFilePath; + + public String outputFilePath; + + public GraphML(String inputFilePath, String outputFilePath){ + this.inputFilePath = inputFilePath; + this.outputFilePath = outputFilePath; + } + + public String constructHeader(){ + StringBuilder header = new StringBuilder(); + try (BufferedReader reader = new BufferedReader(new FileReader(inputFilePath))){ + String line; + while ((line = reader.readLine()) != null) { + header.append(line); + header.append(System.lineSeparator()); + } + + }catch (IOException e){ + System.out.println("IOException detected: " + e.getMessage()); + } + return header.toString(); + } + + public void serializeWitness(List edgeList, List nodeList, String header){ + try (FileWriter writer = new FileWriter(outputFilePath)){ + StringBuilder witnessBuilder = new StringBuilder(); + + witnessBuilder.append(header); + witnessBuilder.append(Node.serializeAllNodes(nodeList)); + witnessBuilder.append(Edge.serializeAllEdges(edgeList)); + + witnessBuilder.append(System.lineSeparator() + " " + System.lineSeparator()); + witnessBuilder.append("" + System.lineSeparator()); + writer.write(witnessBuilder.toString()); + }catch (IOException e){ + System.out.println("IOException detected: " + e.getMessage()); + } + } + + public void serializeEmptyWitness(String node, String header){ + try (FileWriter writer = new FileWriter(outputFilePath)){ + StringBuilder emptyWitnessBuilder = new StringBuilder(); + + emptyWitnessBuilder.append(header); + emptyWitnessBuilder.append(node); + + emptyWitnessBuilder.append(System.lineSeparator() + " " + System.lineSeparator()); + emptyWitnessBuilder.append("" + System.lineSeparator()); + writer.write(emptyWitnessBuilder.toString()); + }catch (IOException e){ + System.out.println("IOException detected: " + e.getMessage()); + } + } +} + + diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java new file mode 100644 index 000000000..970762889 --- /dev/null +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java @@ -0,0 +1,48 @@ +package gov.nasa.jpf.symbc.witness; + +import java.util.List; + + +public class Node{ + public int numberOfNode; + + public int indexOfNode; + public boolean noCounterExample; + + public String serializeNode(){ + // StringBuilder for serializing node of witness + StringBuilder nodeBuilder = new StringBuilder(System.lineSeparator()); + // If there is no symbolic variable, generate empty witness + if(numberOfNode == 0 || noCounterExample){ + nodeBuilder.append(String.format(" \n", 0)); + nodeBuilder.append(" true true\n"); + nodeBuilder.append(" "); + return nodeBuilder.toString(); + } + + nodeBuilder.append(String.format(" \n", indexOfNode)); + if(indexOfNode == 0){ + nodeBuilder.append(" true\n"); + } + else if(indexOfNode == numberOfNode-1){ + nodeBuilder.append(" true\n"); + } + nodeBuilder.append(" \n"); + return nodeBuilder.toString(); + } + + public static String serializeAllNodes(List nodeList){ + StringBuilder allNodesBuilder = new StringBuilder(); + for(Node node : nodeList){ + allNodesBuilder.append(node.serializeNode()); + } + return allNodesBuilder.toString(); + } + + public Node(int numberOfNode, int indexOfNode, boolean noCounterExample){ + this.numberOfNode = numberOfNode; + this.indexOfNode = indexOfNode; + this.noCounterExample = noCounterExample; + } + +} \ No newline at end of file diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/PathConditionParser.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/PathConditionParser.java new file mode 100644 index 000000000..c998f3b17 --- /dev/null +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/PathConditionParser.java @@ -0,0 +1,65 @@ +package gov.nasa.jpf.symbc.witness; + + +import java.util.List; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +public class PathConditionParser{ + + public void parseSymVar(String strPathCondition, List symbolicVariableInfoList){ + // Currently not handling String type + // Extract variable name and value + Pattern pattern = Pattern.compile("(\\w+)\\[(-?\\d+(\\.\\d+)?([eE][-+]?\\d+)?)\\]"); + Matcher matcher = pattern.matcher(strPathCondition); + + + // Insert value to list + while (matcher.find()) { + String pcVariableName = matcher.group(1); + String pcVariableValue = matcher.group(2); + // There are 3 cases, real number, string and other numeric types + if (pcVariableName.contains("double") || pcVariableName.contains("float") || pcVariableName.contains("REAL")) { + double value = Double.parseDouble(pcVariableValue); // 실수로 파싱 + for(int i=0; i Date: Sun, 25 Aug 2024 16:04:09 +0900 Subject: [PATCH 12/31] Adding package for witness generation GSoC 2024 project --- .../gov/nasa/jpf/symbc/SymbolicListener.java | 39 ++----------------- 1 file changed, 3 insertions(+), 36 deletions(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java index 984c49d93..0c3b78c34 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java @@ -16,37 +16,6 @@ * limitations under the License. */ -/** - * v.nasa.jpf.symbc.witness package - * - * Edge edge = new Edge(Node node1, Node node2); - * edges.toString() - * * node1.toString() - * node2.toString() - * - * - * class GraphMl - * boolean allowMethodAssumptions = false; - * graphml.toString() - * template - * edges.print(allowMethodAssumptions) - * node.toString - * graphml.serialize() - * String witnessStr = graphml.toString() - * printToWitnessFile(witnessStr) - * - * classes - * Node : toString/Serialize method - * Edge - * GraphMl - * - * - * SymbolicListener - * Edge edge = new Edge(Node node1, Node node2); - * GraphMl graphml = new GraphMl(List edges) - * graphml.serialize(); - * - */ package gov.nasa.jpf.symbc; @@ -83,8 +52,6 @@ import java.io.*; import java.util.*; -import java.util.regex.Matcher; -import java.util.regex.Pattern; public class SymbolicListener extends PropertyListenerAdapter implements PublisherExtension { @@ -238,12 +205,11 @@ public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nex if (!vm.getSystemState().isIgnored()) { Instruction insn = executedInstruction; - // SystemState ss = vm.getSystemState(); + ThreadInfo ti = currentThread; Config conf = vm.getConfig(); String strInsn = executedInstruction.toString(); - //System.out.println(strInsn); - // Debug.makeSymbolic + if(strInsn.contains("invokestatic") && strInsn.contains("Verifier.nondet")){ interceptSymbolic = true; } @@ -363,6 +329,7 @@ public void instructionExecuted(VM vm, ThreadInfo currentThread, Instruction nex symLineNumber = 0; symRetrunType = ""; symVarName = ""; + // Initialize interceptSymbolic interceptSymbolic = false; } From 4bf6eff47b7d7e7133f7e259cc93fb3e99cb5898 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 21:04:35 +0900 Subject: [PATCH 13/31] Add comments for object and methods --- .../gov/nasa/jpf/symbc/witness/GraphML.java | 31 +++++++++++++++++-- 1 file changed, 29 insertions(+), 2 deletions(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java index d56a072f0..fbe01dced 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java @@ -1,3 +1,11 @@ +/** + * Object that represents violation witness + * It has 3 methods, constructHeader(), serializeWitness() and serializeEmptyWitness() + * Two class variables are required : inputFilePath and outputFilePath + * inputFilePath denotes the path to the witness template + * outputFilePath denotes the path where the violation witness will exist + */ + package gov.nasa.jpf.symbc.witness; import java.io.BufferedReader; @@ -17,7 +25,13 @@ public GraphML(String inputFilePath, String outputFilePath){ this.outputFilePath = outputFilePath; } - public String constructHeader(){ + /** + * It reads witness template at inputFilePath + * Then it assigns basic declaration of violation witness, such as key attribute declaration + * to StringBuilder object + * @return String consist of basic header information of violation witness(headers, witness type, producer name) + */ + public String constructHeader(){ StringBuilder header = new StringBuilder(); try (BufferedReader reader = new BufferedReader(new FileReader(inputFilePath))){ String line; @@ -32,6 +46,12 @@ public String constructHeader(){ return header.toString(); } + /** + * Method that serializes violation witness based on 3 parameters + * @param edgeList contains edges for violation witness + * @param nodeList contains nodes for violation witness + * @param header is the String that contains basic header information for violation witness + */ public void serializeWitness(List edgeList, List nodeList, String header){ try (FileWriter writer = new FileWriter(outputFilePath)){ StringBuilder witnessBuilder = new StringBuilder(); @@ -48,7 +68,14 @@ public void serializeWitness(List edgeList, List nodeList, String he } } - public void serializeEmptyWitness(String node, String header){ + /** + * Method that serializes empty violation witness + * This method will be invoked when there is no counterexample or symbolic variable(invocation of Verifier.nondet~()) + * @param node represents the node for empty witness. It has two keys, which are entry and violation + * that denotes start node of violation witness and represents the node that has violation, respectively. + * @param header is the String that contains basic header information for violation witness + */ + public void serializeEmptyWitness(String node, String header){ try (FileWriter writer = new FileWriter(outputFilePath)){ StringBuilder emptyWitnessBuilder = new StringBuilder(); From 89bf697e59612239cddc119a7113879d6fa81e3b Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 21:46:11 +0900 Subject: [PATCH 14/31] Add comments for object and methods --- .../main/gov/nasa/jpf/symbc/witness/Node.java | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java index 970762889..55203fe27 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java @@ -1,3 +1,11 @@ +/** + * Object that represents the node part of violation witness + * It has two methods, serializeNode() and serializeAllNodes() + * Variable numberOfNode denotes the total number of node of violation witness + * Variable indexOfNode denotes the index of the node + * Variable noCounterExample is a flag that shows whether the counterexample is exists or not + */ + package gov.nasa.jpf.symbc.witness; import java.util.List; @@ -9,6 +17,13 @@ public class Node{ public int indexOfNode; public boolean noCounterExample; + /** + * It serializes a single node of violation witness + * If there is no counterexample or the number of node is zero, it generates the node + * that contains two keys, entry and violation + * Else, it generates the node as String + * @return A string that represents single node of violation witness + */ public String serializeNode(){ // StringBuilder for serializing node of witness StringBuilder nodeBuilder = new StringBuilder(System.lineSeparator()); @@ -31,6 +46,11 @@ else if(indexOfNode == numberOfNode-1){ return nodeBuilder.toString(); } + /** + * It serializes every node in nodeList + * @param nodeList contains all nodes of the violation witness + * @return A string that represents every node of the violation witness + */ public static String serializeAllNodes(List nodeList){ StringBuilder allNodesBuilder = new StringBuilder(); for(Node node : nodeList){ From 8417ccba630b7cc2178db5322fd05363cb34d29c Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 21:47:54 +0900 Subject: [PATCH 15/31] Add comments for object and methods --- jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java index 55203fe27..e16c8922e 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java @@ -1,5 +1,5 @@ /** - * Object that represents the node part of violation witness + * Object that represents a single node of the violation witness * It has two methods, serializeNode() and serializeAllNodes() * Variable numberOfNode denotes the total number of node of violation witness * Variable indexOfNode denotes the index of the node From 1af805c8f61f871cb3c64e3091fd545843f916ab Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 21:49:30 +0900 Subject: [PATCH 16/31] Add comments for object and methods --- .../src/main/gov/nasa/jpf/symbc/witness/Node.java | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java index e16c8922e..e2df896fe 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java @@ -17,6 +17,12 @@ public class Node{ public int indexOfNode; public boolean noCounterExample; + public Node(int numberOfNode, int indexOfNode, boolean noCounterExample){ + this.numberOfNode = numberOfNode; + this.indexOfNode = indexOfNode; + this.noCounterExample = noCounterExample; + } + /** * It serializes a single node of violation witness * If there is no counterexample or the number of node is zero, it generates the node @@ -59,10 +65,4 @@ public static String serializeAllNodes(List nodeList){ return allNodesBuilder.toString(); } - public Node(int numberOfNode, int indexOfNode, boolean noCounterExample){ - this.numberOfNode = numberOfNode; - this.indexOfNode = indexOfNode; - this.noCounterExample = noCounterExample; - } - } \ No newline at end of file From 90a3d14bfc9c48eaedb627a5b2685b575062041b Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 21:59:32 +0900 Subject: [PATCH 17/31] Add comments for object and methods --- .../main/gov/nasa/jpf/symbc/witness/Edge.java | 24 ++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Edge.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Edge.java index 5c9b3aac8..06fee9e8e 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Edge.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Edge.java @@ -1,3 +1,15 @@ +/** + * Object that represents a single edge of the violation witness + * It has two methods, serializeEdge() and serializeAllEdges() + * Variable indexOfEdge denotes an index of the node + * Variable fileName denotes the value of the key "originfile" in the edge + * Variable assumptionScope denotes the value of the key "assumption.scope" in the edge + * Variable allowMethodInvocation is a flag that shows whether invocation of method is allowed + * to represent the string value of assumption or not + * List symbolicVariableInfoList is a list that contains the value of + * the key "startline" and "assumption" + */ + package gov.nasa.jpf.symbc.witness; import java.util.List; @@ -20,8 +32,13 @@ public Edge(int indexOfEdge, String fileName, List symboli this.allowMethodInvocation = allowMethodInvocation; this.assumptionScope = assumptionScope; } + + /** + * It serializes a single edge of the violation witness + * @return A string that represents single edge + */ private String serializeEdge(){ - // later, I have to handle the case when length == 0 and string type for assumption + StringBuilder edgeBuilder = new StringBuilder(); edgeBuilder.append(String.format(" \n", indexOfEdge, indexOfEdge+1)); //edgeId += System.lineSeparator(); @@ -66,6 +83,11 @@ else if(symbolicVariableInfoList.get(indexOfEdge).returnType.equals("java.lang.S return edgeBuilder.toString(); } + /** + * It serializes every edge in edgeList + * @param edgeList contains all edges of the violation witness + * @return A string that represents every edge of the violation witness + */ public static String serializeAllEdges(List edgeList){ StringBuilder allEdgesBuilder = new StringBuilder(); for(Edge edge : edgeList){ From cfbe68441e4f0aa329db694382d9b53ad4e682a1 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 22:06:29 +0900 Subject: [PATCH 18/31] Add comments for object --- .../gov/nasa/jpf/symbc/witness/SymbolicVariableInfo.java | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/SymbolicVariableInfo.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/SymbolicVariableInfo.java index df4a495c1..33c520916 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/SymbolicVariableInfo.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/SymbolicVariableInfo.java @@ -1,5 +1,12 @@ -package gov.nasa.jpf.symbc.witness; +/** + * Object that contains the required information to construct violation witness + * Variable lineNumber denotes the line number of symbolic variable(Verifier.nondet~()'s invocation) + * Variable returnType denotes the type of symbolic variable + * Variable varName denotes the name of symbolic variable + * Variable varValue denotes the value of symbolic variable + */ +package gov.nasa.jpf.symbc.witness; public class SymbolicVariableInfo{ From 1e91da896227a94b6a84e3438daf5d18b4dc971b Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sun, 25 Aug 2024 22:11:09 +0900 Subject: [PATCH 19/31] Add comments for object and methods --- .../symbc/witness/PathConditionParser.java | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/PathConditionParser.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/PathConditionParser.java index c998f3b17..8067dd9c6 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/PathConditionParser.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/PathConditionParser.java @@ -1,3 +1,7 @@ +/** + * Object for parsing symbolic variable at PathCondition + * It has one method, parseSymVar() + */ package gov.nasa.jpf.symbc.witness; @@ -6,9 +10,12 @@ import java.util.regex.Pattern; public class PathConditionParser{ - + /** + * It parses a value of symbolic variable from PathCondition, and match it to corresponding variable + * @param strPathCondition is a String type PathCondition + * @param symbolicVariableInfoList is a list that contains the information of symbolic variables + */ public void parseSymVar(String strPathCondition, List symbolicVariableInfoList){ - // Currently not handling String type // Extract variable name and value Pattern pattern = Pattern.compile("(\\w+)\\[(-?\\d+(\\.\\d+)?([eE][-+]?\\d+)?)\\]"); Matcher matcher = pattern.matcher(strPathCondition); @@ -19,6 +26,8 @@ public void parseSymVar(String strPathCondition, List symb String pcVariableName = matcher.group(1); String pcVariableValue = matcher.group(2); // There are 3 cases, real number, string and other numeric types + + // For real type if (pcVariableName.contains("double") || pcVariableName.contains("float") || pcVariableName.contains("REAL")) { double value = Double.parseDouble(pcVariableValue); // 실수로 파싱 for(int i=0; i symb } } - + // For String type else if (pcVariableName.contains("string")) { for (int i = 0; i < symbolicVariableInfoList.size(); i++) { if (symbolicVariableInfoList.get(i).varName.equals(pcVariableName)) { @@ -39,12 +48,12 @@ else if (pcVariableName.contains("string")) { } } - + // Other types else { int value = Integer.parseInt(pcVariableValue); for(int i=0; i Date: Mon, 26 Aug 2024 03:08:49 +0900 Subject: [PATCH 20/31] Fix small bug --- jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java | 2 ++ jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java index 0c3b78c34..4b47c89ac 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java @@ -181,6 +181,8 @@ public void propertyViolated(Search search) { Edge edge = new Edge(i, fileName, symbolicVariableInfoList, allowMethodInvocation, assumptionScope); edgeList.add(edge); } + // Add last node that contains violation key + nodeList.add(new Node(symbolicVariableInfoList.size(), symbolicVariableInfoList.size(), false)); GraphML graphML = new GraphML(inputFilePath, outputFilePath); String header = graphML.constructHeader(); graphML.serializeWitness(edgeList, nodeList, header); diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java index e2df896fe..59f4dcd3c 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/Node.java @@ -45,7 +45,7 @@ public String serializeNode(){ if(indexOfNode == 0){ nodeBuilder.append(" true\n"); } - else if(indexOfNode == numberOfNode-1){ + else if(indexOfNode == numberOfNode){ nodeBuilder.append(" true\n"); } nodeBuilder.append(" \n"); From 7cd55babf3a65c8da27b1715aa6d30cea30328c5 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Mon, 26 Aug 2024 16:39:34 +0900 Subject: [PATCH 21/31] Add a guide to generate witness and validate it --- README.md | 199 ++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 199 insertions(+) diff --git a/README.md b/README.md index ee288b968..bbfe4b16e 100644 --- a/README.md +++ b/README.md @@ -302,6 +302,205 @@ loaded code: classes=85,methods=1648 +## Validate the witness generated by SPF + +Note : make sure to set your working directory to SPF. If not, SPF can't read the witness template so it can't generate violation witness. + +If you want to create violaion witness of certain benchmark on SV-COMP, follow these steps. + +### 1. Run a benchmark at SV-COMP on SPF + +At first, run SPF on certain benchmark. I'm attaching here the script that used at SV-COMP. Don't forget to specify using SymbolicListener at config. + +
+SV-COMP Script + +```bash +#!/bin/bash + +# create site.properties +SITE_PROPERTIES=site.properties +echo "jpf-core = `pwd`/jpf-core" > $SITE_PROPERTIES +echo "jpf-symbc = `pwd`/jpf-symbc" >> $SITE_PROPERTIES +echo "extensions=\${jpf-core},\${jpf-symbc}" >> $SITE_PROPERTIES + +# parse arguments +declare -a BM +BM=() +PROP_FILE="" +WITNESS_FILE="" + +TOOL_BINARY=jpf-core/bin/jpf +FIND_OPTIONS="-name '*.java'" + +while [ -n "$1" ] ; do + case "$1" in + --32|--64) BIT_WIDTH="${1##--}" ; shift 1 ;; + --propertyfile) PROP_FILE="$2" ; shift 2 ;; + --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;; + --version) date -r jpf-symbc/build/jpf-symbc.jar ; exit 0 ;; + *) SRC=(`eval "find $1 $FIND_OPTIONS"`) ; BM=("${BM[@]}" "${SRC[@]}") ; shift 1 ;; + esac +done + +if [ -z "${BM[0]}" ] || [ -z "$PROP_FILE" ] ; then + echo "Missing benchmark or property file" + exit 1 +fi + +if [ ! -s "${BM[0]}" ] || [ ! -s "$PROP_FILE" ] ; then + echo "Empty benchmark or property file" + exit 1 +fi + +# we ignore the property file (there is only one property at the moment) +# we ignore the witness file (not used yet) + +LOG=`mktemp -t jpf-log.XXXXXX` +DIR=`mktemp -d -t jpf-benchmark.XXXXXX` +trap "rm -rf $DIR" EXIT + +# create target directory +mkdir -p $DIR/target/classes + +# build src files from benchmark +/usr/lib/jvm/java-8-openjdk-amd64/bin/javac -g -cp $DIR/target/classes -d $DIR/target/classes "${BM[@]}" + +# create configuration file +echo "target=Main" > $DIR/config.jpf +echo "classpath=`pwd`/jpf-symbc/build/classes:$DIR/target/classes" >> $DIR/config.jpf +echo "symbolic.dp=z3bitvector" >> $DIR/config.jpf +echo "symbolic.bvlength=64" >> $DIR/config.jpf +echo "search.depth_limit=200" >> $DIR/config.jpf +echo "symbolic.strings=true" >> $DIR/config.jpf +echo "symbolic.string_dp=ABC" >> $DIR/config.jpf +echo "symbolic.string_dp_timeout_ms=3000" >> $DIR/config.jpf +echo "symbolic.lazy=on" >> $DIR/config.jpf +echo "symbolic.arrays=true" >> $DIR/config.jpf +echo "listener = .symbc.SymbolicListener" >> $DIR/config.jpf + +# run SPF +export LD_LIBRARY_PATH=`pwd`/jpf-symbc/lib:$LD_LIBRARY_PATH +#jpf-core/bin/jpf $DIR/config.jpf +if test -z "$JVM_FLAGS"; then + JVM_FLAGS="-Xmx1024m -ea" +fi +/usr/lib/jvm/java-8-openjdk-amd64/bin/java $JVM_FLAGS -jar `pwd`/jpf-core/build/RunJPF.jar $DIR/config.jpf | tee $LOG + +# check the result +grep "no errors detected" $LOG > /dev/null +if [ $? -eq 0 ]; then + echo "SAFE" +else + grep "^error.*NoUncaughtExceptionsProperty.*AssertionError" $LOG > /dev/null + if [ $? -eq 0 ]; then + echo "UNSAFE" + else + echo "UNKNOWN" + fi +fi +``` +
+ +With the script above, run SPF. Here I ran `jbmc-regression/assert2` on SPF. If you `ls`, you can check generated witness, `witness.graphml`. + +
+Console Output + +``` +(base) ➜ SPF git:(sv-comp) ✗ ./jpf-sv-comp.sh --propertyfile ../wit4java/sv-benchmarks/java/properties/assert_java.prp ../wit4java/sv-benchmarks/java/common ../wit4java/sv-benchmarks/java/jbmc-regression/assert2 +symbolic.min_int=-2147483648 +symbolic.min_long=-9223372036854775808 +symbolic.min_short=-32768 +symbolic.min_byte=-128 +symbolic.min_char=0 +symbolic.max_int=2147483647 +symbolic.max_long=9223372036854775807 +symbolic.max_short=32767 +symbolic.max_byte=127 +symbolic.max_char=65535 +symbolic.min_double=4.9E-324 +symbolic.max_double=1.7976931348623157E308 +JavaPathfinder core system v8.0 (rev 1e91da896227a94b6a84e3438daf5d18b4dc971b) - (C) 2005-2014 United States Government. All rights reserved. + + +====================================================== system under test +Main.main() + +====================================================== search started: 24. 8. 26 오후 4:20 +Property Violated: PC is constraint # = 2 +int0[1000] <= CONST_1000 && +int0[1000] >= CONST_1000 +Property Violated: result is "java.lang.AssertionError: i is greater 1000..." +**************************** + +====================================================== error 1 +gov.nasa.jpf.vm.NoUncaughtExceptionsProperty +java.lang.AssertionError: i is greater 1000 + at Main.main(Main.java:23) + + +====================================================== snapshot #1 +thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} + call stack: + at Main.main(Main.java:23) + + +====================================================== Method Summaries +Inputs: + +() --> "java.lang.AssertionError: i is greater 1000..." + +====================================================== Method Summaries (HTML) +

Test Cases Generated by Symbolic JavaPath Finder for (Path Coverage)

+ + + +
RETURN
"java.lang.AssertionError: i is greater 1000..."
+ +====================================================== results +error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.AssertionError: i is greater 1000 at Ma..." + +====================================================== statistics +elapsed time: 00:00:00 +states: new=3,visited=0,backtracked=0,end=0 +search: maxDepth=3,constraints=0 +choice generators: thread=1 (signal=0,lock=1,sharedRef=0,threadApi=0,reschedule=0), data=2 +heap: new=484,released=8,maxLive=0,gcCycles=1 +instructions: 6414 +max memory: 245MB +loaded code: classes=89,methods=1869 + +====================================================== search finished: 24. 8. 26 오후 4:20 +UNSAFE +``` +``` +(base) ➜ SPF git:(sv-comp) ✗ ls +README.md build.properties gradlew hs_err_pid64341.log jpf-core jpf-symbc site.properties +build.gradle gradle gradlew.bat hs_err_pid66807.log jpf-sv-comp.sh settings.gradle witness.graphml +``` +
+ + +### 2. Run witness validator tool + + +Run a witness validator tool such as wit4java. You can download here : https://github.com/wit4java/wit4java/tree/main?tab=readme-ov-file + +
+Console Output + +``` +(base) ➜ wit4java git:(main) ✗ ./wit4java-wrapper.py --witness ../SPF/witness.graphml --local-dir ../wit4java/sv-benchmarks/java/common ../wit4java/sv-benchmarks/java/jbmc-regression/assert2 +./bin/wit4java --local-dir ../wit4java/sv-benchmarks/java/jbmc-regression/assert2 --packages ../wit4java/sv-benchmarks/java/common --witness ../SPF/witness.graphml +wit4java version: 3.0 +witness: ../SPF/witness.graphml +wit4java: Witness Correct +``` +
+ +You can find commands to run SPF and wit4java at SV-COMP. Here is the link : https://sv-comp.sosy-lab.org/2024/results/results-verified/spf.results.SV-COMP24.table.html#/table + From 67637cba34bab2b758b9194473a4bb10177e729f Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Mon, 26 Aug 2024 16:42:41 +0900 Subject: [PATCH 22/31] Add a guide to generate witness and validate it --- README.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index bbfe4b16e..eba2a4e71 100644 --- a/README.md +++ b/README.md @@ -402,7 +402,7 @@ fi ``` -With the script above, run SPF. Here I ran `jbmc-regression/assert2` on SPF. If you `ls`, you can check generated witness, `witness.graphml`. +With the script above, run SPF. Here I ran `jbmc-regression/assert2` on SPF.
Console Output @@ -474,6 +474,13 @@ loaded code: classes=89,methods=1869 ====================================================== search finished: 24. 8. 26 오후 4:20 UNSAFE ``` +
+ +If you `ls`, you can check generated witness, `witness.graphml`. + +
+Console Output + ``` (base) ➜ SPF git:(sv-comp) ✗ ls README.md build.properties gradlew hs_err_pid64341.log jpf-core jpf-symbc site.properties From 376c2cd72dcd6400b081e8526e38a97859295719 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Mon, 26 Aug 2024 16:44:13 +0900 Subject: [PATCH 23/31] Add a guide to generate witness and validate it --- README.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index eba2a4e71..c4f87240b 100644 --- a/README.md +++ b/README.md @@ -402,10 +402,11 @@ fi ```
+ With the script above, run SPF. Here I ran `jbmc-regression/assert2` on SPF.
-Console Output +Console Output ``` (base) ➜ SPF git:(sv-comp) ✗ ./jpf-sv-comp.sh --propertyfile ../wit4java/sv-benchmarks/java/properties/assert_java.prp ../wit4java/sv-benchmarks/java/common ../wit4java/sv-benchmarks/java/jbmc-regression/assert2 From 37e5e3541b8fcd5c0f07ebd5756d95d9f6210331 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Fri, 6 Sep 2024 17:42:58 +0900 Subject: [PATCH 24/31] Add link to wit4java and sv-benchmarks and specify directory structure --- README.md | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index c4f87240b..6821323be 100644 --- a/README.md +++ b/README.md @@ -304,10 +304,29 @@ loaded code: classes=85,methods=1648 ## Validate the witness generated by SPF -Note : make sure to set your working directory to SPF. If not, SPF can't read the witness template so it can't generate violation witness. + If you want to create violaion witness of certain benchmark on SV-COMP, follow these steps. +### 0. Download wit4java and sv-benchmarks + +Before start following steps, you need to install wit4java, which is witness validator tool used at SV-COMP, and benchmarks at SV-COMP. Please download these things before we go on. Here is the link for these two. + +Wit4java : https://github.com/wit4java/wit4java +Benchamrks for SV-COMP : https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks + +Or, you can just run these two command on your terminal. +`git clone https://github.com/wit4java/wit4java.git` +`git clone https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git` + +From here, I will assume your directory structure would be like below. All 3 directories are located next to each other. + +```{bash} +SPF +wit4java +sv-benchmarks +``` + ### 1. Run a benchmark at SV-COMP on SPF At first, run SPF on certain benchmark. I'm attaching here the script that used at SV-COMP. Don't forget to specify using SymbolicListener at config. From 98f2d9d1c274d34028db973d477457dfd67c70d2 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Fri, 6 Sep 2024 17:44:23 +0900 Subject: [PATCH 25/31] Add link to wit4java and sv-benchmarks and specify directory structure --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 6821323be..44363c933 100644 --- a/README.md +++ b/README.md @@ -317,6 +317,7 @@ Benchamrks for SV-COMP : https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks Or, you can just run these two command on your terminal. `git clone https://github.com/wit4java/wit4java.git` + `git clone https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git` From here, I will assume your directory structure would be like below. All 3 directories are located next to each other. From 4000a8bcd60e5d84eb2d99f8be15137eaf52b66a Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Fri, 6 Sep 2024 17:45:07 +0900 Subject: [PATCH 26/31] Add link to wit4java and sv-benchmarks and specify directory structure --- README.md | 1 + 1 file changed, 1 insertion(+) diff --git a/README.md b/README.md index 44363c933..6b5be5809 100644 --- a/README.md +++ b/README.md @@ -316,6 +316,7 @@ Wit4java : https://github.com/wit4java/wit4java Benchamrks for SV-COMP : https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks Or, you can just run these two command on your terminal. + `git clone https://github.com/wit4java/wit4java.git` `git clone https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git` From 3003f17b7cf2b26eb46471b1145f78201c8e0207 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sat, 7 Sep 2024 01:12:17 +0900 Subject: [PATCH 27/31] Update README.md --- README.md | 119 +++++++----------------------------------------------- 1 file changed, 15 insertions(+), 104 deletions(-) diff --git a/README.md b/README.md index 6b5be5809..ecf3a2591 100644 --- a/README.md +++ b/README.md @@ -316,7 +316,6 @@ Wit4java : https://github.com/wit4java/wit4java Benchamrks for SV-COMP : https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks Or, you can just run these two command on your terminal. - `git clone https://github.com/wit4java/wit4java.git` `git clone https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git` @@ -331,106 +330,17 @@ sv-benchmarks ### 1. Run a benchmark at SV-COMP on SPF -At first, run SPF on certain benchmark. I'm attaching here the script that used at SV-COMP. Don't forget to specify using SymbolicListener at config. +At first, run SPF on certain benchmark. Here, I will use `jbmc-regression/assert2`. You can find script for running SPF at `jpf-symbc/bin`. Before run the script, please change path to the jdk based on your machine. For example, if you are using amd64 linux machine, replace `/Library/Java/JavaVirtualMachines/zulu-8.jdk/Contents/Home/bin/java` with `/usr/lib/jvm/java-8-openjdk-amd64/bin/java` and `/Library/Java/JavaVirtualMachines/zulu-8.jdk/Contents/Home/bin/javac` with `/usr/lib/jvm/java-8-openjdk-amd64/bin/javac`. Now you are ready to run SPF with the script. -
-SV-COMP Script - -```bash -#!/bin/bash - -# create site.properties -SITE_PROPERTIES=site.properties -echo "jpf-core = `pwd`/jpf-core" > $SITE_PROPERTIES -echo "jpf-symbc = `pwd`/jpf-symbc" >> $SITE_PROPERTIES -echo "extensions=\${jpf-core},\${jpf-symbc}" >> $SITE_PROPERTIES - -# parse arguments -declare -a BM -BM=() -PROP_FILE="" -WITNESS_FILE="" - -TOOL_BINARY=jpf-core/bin/jpf -FIND_OPTIONS="-name '*.java'" - -while [ -n "$1" ] ; do - case "$1" in - --32|--64) BIT_WIDTH="${1##--}" ; shift 1 ;; - --propertyfile) PROP_FILE="$2" ; shift 2 ;; - --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;; - --version) date -r jpf-symbc/build/jpf-symbc.jar ; exit 0 ;; - *) SRC=(`eval "find $1 $FIND_OPTIONS"`) ; BM=("${BM[@]}" "${SRC[@]}") ; shift 1 ;; - esac -done - -if [ -z "${BM[0]}" ] || [ -z "$PROP_FILE" ] ; then - echo "Missing benchmark or property file" - exit 1 -fi - -if [ ! -s "${BM[0]}" ] || [ ! -s "$PROP_FILE" ] ; then - echo "Empty benchmark or property file" - exit 1 -fi - -# we ignore the property file (there is only one property at the moment) -# we ignore the witness file (not used yet) - -LOG=`mktemp -t jpf-log.XXXXXX` -DIR=`mktemp -d -t jpf-benchmark.XXXXXX` -trap "rm -rf $DIR" EXIT - -# create target directory -mkdir -p $DIR/target/classes - -# build src files from benchmark -/usr/lib/jvm/java-8-openjdk-amd64/bin/javac -g -cp $DIR/target/classes -d $DIR/target/classes "${BM[@]}" - -# create configuration file -echo "target=Main" > $DIR/config.jpf -echo "classpath=`pwd`/jpf-symbc/build/classes:$DIR/target/classes" >> $DIR/config.jpf -echo "symbolic.dp=z3bitvector" >> $DIR/config.jpf -echo "symbolic.bvlength=64" >> $DIR/config.jpf -echo "search.depth_limit=200" >> $DIR/config.jpf -echo "symbolic.strings=true" >> $DIR/config.jpf -echo "symbolic.string_dp=ABC" >> $DIR/config.jpf -echo "symbolic.string_dp_timeout_ms=3000" >> $DIR/config.jpf -echo "symbolic.lazy=on" >> $DIR/config.jpf -echo "symbolic.arrays=true" >> $DIR/config.jpf -echo "listener = .symbc.SymbolicListener" >> $DIR/config.jpf - -# run SPF -export LD_LIBRARY_PATH=`pwd`/jpf-symbc/lib:$LD_LIBRARY_PATH -#jpf-core/bin/jpf $DIR/config.jpf -if test -z "$JVM_FLAGS"; then - JVM_FLAGS="-Xmx1024m -ea" -fi -/usr/lib/jvm/java-8-openjdk-amd64/bin/java $JVM_FLAGS -jar `pwd`/jpf-core/build/RunJPF.jar $DIR/config.jpf | tee $LOG - -# check the result -grep "no errors detected" $LOG > /dev/null -if [ $? -eq 0 ]; then - echo "SAFE" -else - grep "^error.*NoUncaughtExceptionsProperty.*AssertionError" $LOG > /dev/null - if [ $? -eq 0 ]; then - echo "UNSAFE" - else - echo "UNKNOWN" - fi -fi -``` -
+The command for running SPF with script looks like this : `jpf-sv-comp.sh --propertyfile /path/to/property classpath1 classpath2 ...`. For example, if you want to run `jbmc-regression/assert2` with the script, the command would be `./jpf-sv-comp.sh --propertyfile ../sv-benchmarks/java/properties/assert_java.prp ../sv-benchmarks/java/common ../sv-benchmarks/java/jbmc-regression/assert2`. -With the script above, run SPF. Here I ran `jbmc-regression/assert2` on SPF. +Here is output for run SPF on `jbmc-regression/assert2`.
Console Output ``` -(base) ➜ SPF git:(sv-comp) ✗ ./jpf-sv-comp.sh --propertyfile ../wit4java/sv-benchmarks/java/properties/assert_java.prp ../wit4java/sv-benchmarks/java/common ../wit4java/sv-benchmarks/java/jbmc-regression/assert2 symbolic.min_int=-2147483648 symbolic.min_long=-9223372036854775808 symbolic.min_short=-32768 @@ -443,13 +353,13 @@ symbolic.max_byte=127 symbolic.max_char=65535 symbolic.min_double=4.9E-324 symbolic.max_double=1.7976931348623157E308 -JavaPathfinder core system v8.0 (rev 1e91da896227a94b6a84e3438daf5d18b4dc971b) - (C) 2005-2014 United States Government. All rights reserved. +JavaPathfinder core system v8.0 (rev 376c2cd72dcd6400b081e8526e38a97859295719) - (C) 2005-2014 United States Government. All rights reserved. ====================================================== system under test Main.main() -====================================================== search started: 24. 8. 26 오후 4:20 +====================================================== search started: 24. 9. 7 오전 12:51 Property Violated: PC is constraint # = 2 int0[1000] <= CONST_1000 && int0[1000] >= CONST_1000 @@ -459,13 +369,13 @@ Property Violated: result is "java.lang.AssertionError: i is greater 1000..." ====================================================== error 1 gov.nasa.jpf.vm.NoUncaughtExceptionsProperty java.lang.AssertionError: i is greater 1000 - at Main.main(Main.java:23) + at Main.main(Main.java:23) ====================================================== snapshot #1 thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0} call stack: - at Main.main(Main.java:23) + at Main.main(Main.java:23) ====================================================== Method Summaries @@ -493,20 +403,20 @@ instructions: 6414 max memory: 245MB loaded code: classes=89,methods=1869 -====================================================== search finished: 24. 8. 26 오후 4:20 +====================================================== search finished: 24. 9. 7 오전 12:51 UNSAFE ```
-If you `ls`, you can check generated witness, `witness.graphml`. +If you `ls` at the directory that you ran SPF, you can check generated witness, `witness.graphml`. For example, if you ran SPF at directory `SPF`, you can see `witness.graphml`.
Console Output ``` (base) ➜ SPF git:(sv-comp) ✗ ls -README.md build.properties gradlew hs_err_pid64341.log jpf-core jpf-symbc site.properties -build.gradle gradle gradlew.bat hs_err_pid66807.log jpf-sv-comp.sh settings.gradle witness.graphml +README.md build.properties gradlew jpf-core jpf-symbc site.properties +build.gradle gradle gradlew.bat jpf-sv-comp.sh settings.gradle witness.graphml ```
@@ -514,14 +424,15 @@ build.gradle gradle gradlew.bat hs_err_pid66807.log ### 2. Run witness validator tool -Run a witness validator tool such as wit4java. You can download here : https://github.com/wit4java/wit4java/tree/main?tab=readme-ov-file +Now, let's run wit4java to validate the generated violation witness! To run wit4java, go to `wit4java` directory. The command for run wit4java looks like this : `./wit4java-wrapper.py --witness /path/to/the/witness --local-dir classpath1 classpath2 ...`. For example, if you want to validate `witness.graphml` generated by running SPF on `jbmc-regression/assert2`, the command would be `./wit4java-wrapper.py --witness ../SPF/witness.graphml --local-dir ../sv-benchmarks/java/common ../sv-benchmarks/java/jbmc-regression/assert2`. + +Here is output for the command above.
Console Output ``` -(base) ➜ wit4java git:(main) ✗ ./wit4java-wrapper.py --witness ../SPF/witness.graphml --local-dir ../wit4java/sv-benchmarks/java/common ../wit4java/sv-benchmarks/java/jbmc-regression/assert2 -./bin/wit4java --local-dir ../wit4java/sv-benchmarks/java/jbmc-regression/assert2 --packages ../wit4java/sv-benchmarks/java/common --witness ../SPF/witness.graphml +./bin/wit4java --local-dir ../sv-benchmarks/java/jbmc-regression/assert2 --packages ../sv-benchmarks/java/common --witness ../SPF/witness.graphml wit4java version: 3.0 witness: ../SPF/witness.graphml wit4java: Witness Correct From 9276524d325a0e734865db37d4af79e8768dfe83 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sat, 7 Sep 2024 01:16:33 +0900 Subject: [PATCH 28/31] Update README.md --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index ecf3a2591..e017b2a03 100644 --- a/README.md +++ b/README.md @@ -439,7 +439,7 @@ wit4java: Witness Correct ```
-You can find commands to run SPF and wit4java at SV-COMP. Here is the link : https://sv-comp.sosy-lab.org/2024/results/results-verified/spf.results.SV-COMP24.table.html#/table +You can find commands to run SPF on other benchmarks and wit4java at SV-COMP. Click elements at "status" column, then it will show commands. Here is the link : https://sv-comp.sosy-lab.org/2024/results/results-verified/spf.results.SV-COMP24.table.html#/table From bb6633bbe49110af857be87839af5e97ba8955d5 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Sat, 7 Sep 2024 01:18:03 +0900 Subject: [PATCH 29/31] Adding script to run SPF on SV-COMP benchmarks --- jpf-symbc/bin/jpf-sv-comp.sh | 90 ++++++++++++++++++++++++++++++++++++ 1 file changed, 90 insertions(+) create mode 100755 jpf-symbc/bin/jpf-sv-comp.sh diff --git a/jpf-symbc/bin/jpf-sv-comp.sh b/jpf-symbc/bin/jpf-sv-comp.sh new file mode 100755 index 000000000..1d54c6cf5 --- /dev/null +++ b/jpf-symbc/bin/jpf-sv-comp.sh @@ -0,0 +1,90 @@ +#!/bin/bash + +# create site.properties +SITE_PROPERTIES=site.properties +echo "jpf-core = `pwd`/jpf-core" > $SITE_PROPERTIES +echo "jpf-symbc = `pwd`/jpf-symbc" >> $SITE_PROPERTIES +echo "extensions=\${jpf-core},\${jpf-symbc}" >> $SITE_PROPERTIES + +# parse arguments +declare -a BM +BM=() +PROP_FILE="" +WITNESS_FILE="" + +TOOL_BINARY=jpf-core/bin/jpf +FIND_OPTIONS="-name '*.java'" + +while [ -n "$1" ] ; do + case "$1" in + --32|--64) BIT_WIDTH="${1##--}" ; shift 1 ;; + --propertyfile) PROP_FILE="$2" ; shift 2 ;; + --graphml-witness) WITNESS_FILE="$2" ; shift 2 ;; + --version) date -r jpf-symbc/build/jpf-symbc.jar ; exit 0 ;; + *) SRC=(`eval "find $1 $FIND_OPTIONS"`) ; BM=("${BM[@]}" "${SRC[@]}") ; shift 1 ;; + esac +done + +if [ -z "${BM[0]}" ] || [ -z "$PROP_FILE" ] ; then + echo "Missing benchmark or property file" + exit 1 +fi + +if [ ! -s "${BM[0]}" ] || [ ! -s "$PROP_FILE" ] ; then + echo "Empty benchmark or property file" + exit 1 +fi + +# we ignore the property file (there is only one property at the moment) +# we ignore the witness file (not used yet) + +LOG=`mktemp -t jpf-log.XXXXXX` +DIR=`mktemp -d -t jpf-benchmark.XXXXXX` +trap "rm -rf $DIR" EXIT + +# create target directory +mkdir -p $DIR/target/classes + +# build src files from benchmark +/Library/Java/JavaVirtualMachines/zulu-8.jdk/Contents/Home/bin/javac -g -cp $DIR/target/classes:../wit4java/sv-benchmarks/java/common:../wit4java/sv-benchmarks/java/securibench/micro:../wit4java/sv-benchmarks/java/java-ranger-regression/infusion/impl -d $DIR/target/classes "${BM[@]}" + +# create configuration file +echo "target=Main" > $DIR/config.jpf +echo "classpath=`pwd`/jpf-symbc/build/classes:$DIR/target/classes" >> $DIR/config.jpf +echo "symbolic.dp=z3bitvector" >> $DIR/config.jpf +echo "symbolic.bvlength=64" >> $DIR/config.jpf +echo "search.depth_limit=200" >> $DIR/config.jpf +echo "symbolic.strings=true" >> $DIR/config.jpf +#echo "symbolic.optimizechoices=false" >> $DIR/config.jpf +echo "symbolic.string_dp=z3str3" >> $DIR/config.jpf +echo "symbolic.string_dp_timeout_ms=3000" >> $DIR/config.jpf +echo "symbolic.lazy=on" >> $DIR/config.jpf +echo "symbolic.arrays=true" >> $DIR/config.jpf +echo "listener = .symbc.SymbolicListener" >> $DIR/config.jpf + +# run SPF +export DYLD_LIBRARY_PATH=`pwd`/jpf-symbc/lib:$DYLD_LIBRARY_PATH +#jpf-core/bin/jpf $DIR/config.jpf +if test -z "$JVM_FLAGS"; then + JVM_FLAGS="-Xmx1024m -ea" +fi +timeout 900 /Library/Java/JavaVirtualMachines/zulu-8.jdk/Contents/Home/bin/java $JVM_FLAGS -jar `pwd`/jpf-core/build/RunJPF.jar $DIR/config.jpf | tee $LOG + +if [ $? -eq 124 ]; then + echo "UNKNOWN" + exit 0 +fi + +# check the result +grep "no errors detected" $LOG > /dev/null +if [ $? -eq 0 ]; then + echo "SAFE" +else + grep "^error.*NoUncaughtExceptionsProperty.*AssertionError" $LOG > /dev/null + if [ $? -eq 0 ]; then + echo "UNSAFE" + else + echo "UNKNOWN" + fi +fi + From 54540050181d5342aea385733aaf557b3eb57323 Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Tue, 10 Sep 2024 12:58:48 +0900 Subject: [PATCH 30/31] Added a setting to find resource properly --- jpf-symbc/build.gradle | 3 +++ 1 file changed, 3 insertions(+) diff --git a/jpf-symbc/build.gradle b/jpf-symbc/build.gradle index b07cc738d..4d0e43c7e 100644 --- a/jpf-symbc/build.gradle +++ b/jpf-symbc/build.gradle @@ -29,6 +29,7 @@ apply from: "gradle/distribution.gradle" apply from: "gradle/source-sets.gradle" apply from: "gradle/build-resources.gradle" + dependencies { // Path of jpf-core build directory is declared as a dependencies for jpf-symbc (Line 35-37) @@ -83,6 +84,7 @@ task createJpfClassesJar(type: Jar) { from sourceSets.main.java.outputDir from sourceSets.annotations.java.outputDir from sourceSets.classes.java.outputDir + from sourceSets.main.resources.srcDirs } task createJpfJar(type: Jar) { @@ -99,6 +101,7 @@ task createJpfJar(type: Jar) { from sourceSets.peers.java.outputDir from sourceSets.annotations.java.outputDir from sourceSets.classes.java.outputDir + from sourceSets.main.resources.srcDirs manifest { attributes "Implementation-Title": "Symbolic Pathfinder system" From fd6b853289f02a16d83c7d240bec4e0e1757553e Mon Sep 17 00:00:00 2001 From: kylekim72 Date: Tue, 10 Sep 2024 13:44:21 +0900 Subject: [PATCH 31/31] Fix to load witness template dynamically --- .../gov/nasa/jpf/symbc/SymbolicListener.java | 30 ++++++++++++++----- .../gov/nasa/jpf/symbc/witness/GraphML.java | 14 +++++---- 2 files changed, 32 insertions(+), 12 deletions(-) diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java index 4b47c89ac..104f304d7 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/SymbolicListener.java @@ -117,7 +117,9 @@ public void propertyViolated(Search search) { VM vm = search.getVM(); // Path to the witness template // Assume working directory is SPF - String inputFilePath = "./jpf-symbc/src/main/resources/witness_template/witness_template_minimal.txt"; + + String resourcePath = "witness_template/witness_template_minimal.txt"; + // Path to output directory, now it is current directory String outputFilePath = "witness.graphml"; @@ -132,9 +134,16 @@ public void propertyViolated(Search search) { Node nodeForEmptyWitness = new Node(1, 0, true); String strNode = nodeForEmptyWitness.serializeNode(); - GraphML emptyWitness = new GraphML(inputFilePath, outputFilePath); - String headerForEmptyWitness = emptyWitness.constructHeader(); - emptyWitness.serializeEmptyWitness(strNode, headerForEmptyWitness); + try(InputStream inputStream = SymbolicListener.class.getClassLoader().getResourceAsStream(resourcePath)){ + if(inputStream == null){ + throw new IllegalArgumentException("Resource not found : " + resourcePath); + } + GraphML emptyWitness = new GraphML(inputStream, outputFilePath); + String headerForEmptyWitness = emptyWitness.constructHeader(); + emptyWitness.serializeEmptyWitness(strNode, headerForEmptyWitness); + }catch (IOException e){ + e.printStackTrace(); + } if ((cg instanceof PCChoiceGenerator) && ((PCChoiceGenerator) cg).getCurrentPC() != null) { PathCondition pc = ((PCChoiceGenerator) cg).getCurrentPC(); @@ -183,9 +192,16 @@ public void propertyViolated(Search search) { } // Add last node that contains violation key nodeList.add(new Node(symbolicVariableInfoList.size(), symbolicVariableInfoList.size(), false)); - GraphML graphML = new GraphML(inputFilePath, outputFilePath); - String header = graphML.constructHeader(); - graphML.serializeWitness(edgeList, nodeList, header); + try(InputStream inputStream = SymbolicListener.class.getClassLoader().getResourceAsStream(resourcePath)){ + if(inputStream == null){ + throw new IllegalArgumentException("Resource not found : " + resourcePath); + } + GraphML graphML = new GraphML(inputStream, outputFilePath); + String header = graphML.constructHeader(); + graphML.serializeWitness(edgeList, nodeList, header); + }catch (IOException e){ + e.printStackTrace(); + } } // } } diff --git a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java index fbe01dced..46acf901b 100644 --- a/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java +++ b/jpf-symbc/src/main/gov/nasa/jpf/symbc/witness/GraphML.java @@ -9,19 +9,21 @@ package gov.nasa.jpf.symbc.witness; import java.io.BufferedReader; -import java.io.FileReader; import java.io.FileWriter; import java.io.IOException; +import java.io.InputStream; +import java.io.InputStreamReader; +import java.nio.charset.StandardCharsets; import java.util.List; public class GraphML{ - public String inputFilePath; + public InputStream inputStream; public String outputFilePath; - public GraphML(String inputFilePath, String outputFilePath){ - this.inputFilePath = inputFilePath; + public GraphML(InputStream inputStream, String outputFilePath){ + this.inputStream = inputStream; this.outputFilePath = outputFilePath; } @@ -33,15 +35,17 @@ public GraphML(String inputFilePath, String outputFilePath){ */ public String constructHeader(){ StringBuilder header = new StringBuilder(); - try (BufferedReader reader = new BufferedReader(new FileReader(inputFilePath))){ + try (BufferedReader reader = new BufferedReader(new InputStreamReader(inputStream))){ String line; while ((line = reader.readLine()) != null) { header.append(line); + //System.out.println(line); header.append(System.lineSeparator()); } }catch (IOException e){ System.out.println("IOException detected: " + e.getMessage()); + System.out.println("here"); } return header.toString(); }