From 3d0d1f05e5f6ed923f445026575216bd3002679d Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Mon, 18 Dec 2023 20:56:10 +0100 Subject: [PATCH 1/3] Missing changes to fully support svcomp properties Signed-off-by: Hernan Ponce de Leon --- Dartagnan-SVCOMP.sh | 12 ++++++++-- .../java/com/dat3m/dartagnan/Dartagnan.java | 23 +++++++++++++++---- .../dartagnan/witness/WitnessBuilder.java | 10 ++++---- .../dartagnan/witness/BuildWitnessTest.java | 2 +- .../java/com/dat3m/svcomp/SVCOMPRunner.java | 6 ++--- 5 files changed, 38 insertions(+), 15 deletions(-) diff --git a/Dartagnan-SVCOMP.sh b/Dartagnan-SVCOMP.sh index 51f14df62f..f4472a5be3 100755 --- a/Dartagnan-SVCOMP.sh +++ b/Dartagnan-SVCOMP.sh @@ -22,9 +22,17 @@ else export DAT3M_HOME=$(pwd) export DAT3M_OUTPUT=$DAT3M_HOME/output - export CFLAGS="-fgnu89-inline" + export OPTFLAGS="-mem2reg -sroa -early-cse -indvars -loop-unroll -fix-irreducible -loop-simplify -simplifycfg -gvn" + if [[ $propertypath == *"no-overflow.prp"* ]]; then + export CFLAGS="-fgnu89-inline -fsanitize=signed-integer-overflow" + elif [[ $propertypath == *"valid-memsafety.prp"* ]]; then + export CFLAGS="-fgnu89-inline -fsanitize=null" + else + export CFLAGS="-fgnu89-inline" + fi + cmd="java -jar svcomp/target/svcomp.jar --method=assume --program.processing.constantPropagation=false --encoding.integers=true --svcomp.step=5 --svcomp.umax=27 cat/svcomp.cat --svcomp.property="$propertypath" "$programpath" "$witness $cmd -fi +fi \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 16ad2173e8..fca9b24de4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -195,12 +195,13 @@ public static void main(String[] args) throws Exception { } long endTime = System.currentTimeMillis(); - System.out.print(generateResultSummary(task, prover, modelChecker)); + String summary = generateResultSummary(task, prover, modelChecker); + System.out.print(summary); System.out.println("Total verification time(ms): " + (endTime - startTime)); if (!o.runValidator()) { // We only generate witnesses if we are not validating one. - generateWitnessIfAble(task, prover, modelChecker); + generateWitnessIfAble(task, prover, modelChecker, summary); } } } catch (InterruptedException e) { @@ -214,12 +215,13 @@ public static void main(String[] args) throws Exception { } } - private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker) { + private static void generateWitnessIfAble(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker, String summary) { // ------------------ Generate Witness, if possible ------------------ final EnumSet properties = task.getProperty(); if (modelChecker.hasModel() && properties.contains(PROGRAM_SPEC)) { try { - WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, modelChecker.getResult()); + String ltlProperty = getLtlPropertyFromSummary(summary); + WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, modelChecker.getResult(), ltlProperty); if (w.canBeBuilt()) { // We can only write witnesses if the path to the original C file was given. w.build().write(); @@ -230,6 +232,19 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme } } + private static String getLtlPropertyFromSummary(String summary) { + if(summary.contains("integer overflow")) { + return "CHECK( init(main()), LTL(G ! overflow))"; + } + if(summary.contains("invalid dereference")) { + return "CHECK( init(main()), LTL(G valid-deref))"; + } + if(summary.contains("user assertion")) { + return "CHECK( init(main()), LTL(G ! call(reach_error())))"; + } + throw new UnsupportedOperationException("Violation found for unsupported property"); + } + public static String generateResultSummary(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker) throws SolverException { // ----------------- Generate output of verification result ----------------- final Program p = task.getProgram(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java index 8e16106c18..d124c1d82f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java @@ -44,6 +44,7 @@ public class WitnessBuilder { private final EncodingContext context; private final ProverEnvironment prover; private final String type; + private final String ltlProperty; // =========================== Configurables =========================== @@ -59,14 +60,15 @@ public class WitnessBuilder { private final Map eventThreadMap = new HashMap<>(); - private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r) { + private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String ltl) { context = checkNotNull(c); prover = checkNotNull(p); type = r.equals(FAIL) ? "violation" : "correctness"; + ltlProperty = ltl; } - public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result) throws InvalidConfigurationException { - WitnessBuilder b = new WitnessBuilder(context, prover, result); + public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, String ltlProperty) throws InvalidConfigurationException { + WitnessBuilder b = new WitnessBuilder(context, prover, result, ltlProperty); context.getTask().getConfig().inject(b); return b; } @@ -83,7 +85,7 @@ public WitnessGraph build() { graph.addAttribute(WITNESSTYPE.toString(), type + "_witness"); graph.addAttribute(SOURCECODELANG.toString(), "C"); graph.addAttribute(PRODUCER.toString(), "Dartagnan"); - graph.addAttribute(SPECIFICATION.toString(), "CHECK( init(main()), LTL(G ! call(reach_error())))"); + graph.addAttribute(SPECIFICATION.toString(), ltlProperty); graph.addAttribute(PROGRAMFILE.toString(), originalProgramFilePath); graph.addAttribute(PROGRAMHASH.toString(), getFileSHA256(new File(originalProgramFilePath))); graph.addAttribute(ARCHITECTURE.toString(), "32bit"); diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java index 652eed0626..d315311330 100644 --- a/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java +++ b/dartagnan/src/test/java/com/dat3m/dartagnan/witness/BuildWitnessTest.java @@ -44,7 +44,7 @@ public void BuildWriteEncode() throws Exception { ProverEnvironment prover = ctx.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { IncrementalSolver modelChecker = IncrementalSolver.run(ctx, prover, task); Result res = modelChecker.getResult(); - WitnessBuilder witnessBuilder = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, res); + WitnessBuilder witnessBuilder = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, res, "user assertion"); config.inject(witnessBuilder); WitnessGraph graph = witnessBuilder.build(); File witnessFile = new File(getOutputDirectory() + "/witness.graphml"); diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index b33d1eae6c..6e9c087996 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -43,12 +43,10 @@ private void property(String p) { //TODO process the property file instead of assuming its contents based of its name if(p.contains("no-data-race")) { property = Property.DATARACEFREEDOM; - } else if(p.contains("unreach-call")) { + } else if(p.contains("unreach-call") || p.contains("no-overflow") || p.contains("valid-memsafety")) { property = Property.PROGRAM_SPEC; } else { - // To comply with SVCOMP qualification rules, we should return UNKNOWN - // instead of throwing an exception for unhandled properties - property = null; + throw new IllegalArgumentException("Unrecognized property " + p); } } From 450fb8b8c259f4a0dc7a41ed0bc62272442efaa5 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 19 Dec 2023 10:48:26 +0100 Subject: [PATCH 2/3] Format Signed-off-by: Hernan Ponce de Leon --- .../dartagnan/witness/WitnessBuilder.java | 401 +++++++++--------- 1 file changed, 203 insertions(+), 198 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java index d124c1d82f..6801442b82 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java @@ -41,216 +41,221 @@ @Options public class WitnessBuilder { - private final EncodingContext context; - private final ProverEnvironment prover; - private final String type; + private final EncodingContext context; + private final ProverEnvironment prover; + private final String type; private final String ltlProperty; // =========================== Configurables =========================== - @Option( - name=WITNESS_ORIGINAL_PROGRAM_PATH, - description="Path to the original C file (for which to create a witness).", - secure=true) - private String originalProgramFilePath; + @Option( + name=WITNESS_ORIGINAL_PROGRAM_PATH, + description="Path to the original C file (for which to create a witness).", + secure=true) + private String originalProgramFilePath; - public boolean canBeBuilt() { return originalProgramFilePath != null; } + public boolean canBeBuilt() { + return originalProgramFilePath != null; + } // ===================================================================== - private final Map eventThreadMap = new HashMap<>(); + private final Map eventThreadMap = new HashMap<>(); - private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String ltl) { - context = checkNotNull(c); - prover = checkNotNull(p); - type = r.equals(FAIL) ? "violation" : "correctness"; + private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String ltl) { + context = checkNotNull(c); + prover = checkNotNull(p); + type = r.equals(FAIL) ? "violation" : "correctness"; ltlProperty = ltl; - } - - public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, String ltlProperty) throws InvalidConfigurationException { - WitnessBuilder b = new WitnessBuilder(context, prover, result, ltlProperty); - context.getTask().getConfig().inject(b); - return b; - } - - public WitnessGraph build() { - for(Thread t : context.getTask().getProgram().getThreads()) { - for(Event e : t.getEntry().getSuccessors()) { - eventThreadMap.put(e, t.getId() - 1); - } - } - - WitnessGraph graph = new WitnessGraph(); - graph.addAttribute(UNROLLBOUND.toString(), valueOf(context.getTask().getProgram().getUnrollingBound())); - graph.addAttribute(WITNESSTYPE.toString(), type + "_witness"); - graph.addAttribute(SOURCECODELANG.toString(), "C"); - graph.addAttribute(PRODUCER.toString(), "Dartagnan"); - graph.addAttribute(SPECIFICATION.toString(), ltlProperty); - graph.addAttribute(PROGRAMFILE.toString(), originalProgramFilePath); - graph.addAttribute(PROGRAMHASH.toString(), getFileSHA256(new File(originalProgramFilePath))); - graph.addAttribute(ARCHITECTURE.toString(), "32bit"); - - DateFormat df = new SimpleDateFormat("yyyy-MM-dd'T'HH:mm:ss"); - df.setTimeZone(TimeZone.getTimeZone("UTC")); - // "If the timestamp is in UTC time, it ends with a 'Z'." - // https://github.com/sosy-lab/sv-witnesses/blob/main/README-GraphML.md - graph.addAttribute(CREATIONTIME.toString(), df.format(new Date())+"Z"); - - Node v0 = new Node("N0"); - v0.addAttribute("entry", "true"); - Node v1 = new Node("N1"); - Node v2 = new Node("N2"); - - Edge edge = new Edge(v0, v1); - edge.addAttribute(CREATETHREAD.toString(), "0"); - graph.addEdge(edge); - edge = new Edge(v1, v2); - edge.addAttribute(THREADID.toString(), "0"); - edge.addAttribute(ENTERFUNCTION.toString(), "main"); - graph.addEdge(edge); - - int nextNode = 2; - int threads = 1; - - if(type.equals("correctness")) { - return graph; - } - - try (Model model = prover.getModel()) { - List execution = reOrderBasedOnAtomicity(context.getTask().getProgram(), getSCExecutionOrder(model)); - - for (int i = 0; i < execution.size(); i++) { - Event e = execution.get(i); - if (i + 1 < execution.size()) { - Event next = execution.get(i + 1); - if (e.hasEqualMetadata(next, SourceLocation.class) && e.getThread() == next.getThread()) { - continue; - } - } - - int cLine = e.hasMetadata(SourceLocation.class) ? e.getMetadata(SourceLocation.class).lineNumber() : -1; - edge = new Edge(new Node("N" + nextNode), new Node("N" + (nextNode + 1))); - edge.addAttribute(THREADID.toString(), valueOf(eventThreadMap.get(e))); - edge.addAttribute(STARTLINE.toString(), valueOf(cLine)); - - // End is also WRITE and PTHREAD, but it does not have - // CLines and thus won't create an edge (as expected) - if (e.hasTag(WRITE) && e.hasTag(PTHREAD)) { - edge.addAttribute(CREATETHREAD.toString(), valueOf(threads)); - threads++; - } - - // FIXME: The tracking of "globalId" here is very fragile - // If we generate a Witness and try to use it after adapting any processing pass - // the matching will fail. In particular, a Witness can only be validated - // by the version of Dartagnan that created it and only with identical configurations. - if(e instanceof Load l) { - edge.addAttribute(EVENTID.toString(), valueOf(e.getGlobalId())); - edge.addAttribute(LOADEDVALUE.toString(), String.valueOf(model.evaluate(context.result(l)))); - } - - if(e instanceof Store s) { - edge.addAttribute(EVENTID.toString(), valueOf(e.getGlobalId())); - Object valueObject = checkNotNull(model.evaluate(context.value(s))); - edge.addAttribute(STOREDVALUE.toString(), valueObject.toString()); - } - - graph.addEdge(edge); - - nextNode++; - if (e instanceof Assert) { - // FIXME: Execution of an assertion is not a problem, if the assertion holds! - break; - } - } - } catch (SolverException ignore) { - // The if above guarantees that if we reach this try, a Model exists - } - graph.getNode("N" + nextNode).addAttribute("violation", "true"); - return graph; - } - - private List getSCExecutionOrder(Model model) { - // TODO: we recently added many cline to many events and this might affect the witness generation. - Predicate executedCEvents = e -> Boolean.TRUE.equals(model.evaluate(context.execution(e))) - && e.hasMetadata(SourceLocation.class); - List execEvents = context.getTask().getProgram().getThreadEvents().stream().filter(executedCEvents).toList(); - Map> map = new HashMap<>(); - for(Event e : execEvents) { - // TODO improve this: these events correspond to return statements - if(e instanceof Store store && store.getMemValue() instanceof BConst bVal && !bVal.getValue()) { - continue; - } - BigInteger var = model.evaluate(context.clockVariable("hb", e)); - if(var != null) { - map.computeIfAbsent(var.intValue(), x -> new ArrayList<>()).add(e); - } + } + + public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, + String ltlProperty) throws InvalidConfigurationException { + WitnessBuilder b = new WitnessBuilder(context, prover, result, ltlProperty); + context.getTask().getConfig().inject(b); + return b; + } + + public WitnessGraph build() { + for (Thread t : context.getTask().getProgram().getThreads()) { + for (Event e : t.getEntry().getSuccessors()) { + eventThreadMap.put(e, t.getId() - 1); + } + } + + WitnessGraph graph = new WitnessGraph(); + graph.addAttribute(UNROLLBOUND.toString(), valueOf(context.getTask().getProgram().getUnrollingBound())); + graph.addAttribute(WITNESSTYPE.toString(), type + "_witness"); + graph.addAttribute(SOURCECODELANG.toString(), "C"); + graph.addAttribute(PRODUCER.toString(), "Dartagnan"); + graph.addAttribute(SPECIFICATION.toString(), ltlProperty); + graph.addAttribute(PROGRAMFILE.toString(), originalProgramFilePath); + graph.addAttribute(PROGRAMHASH.toString(), getFileSHA256(new File(originalProgramFilePath))); + graph.addAttribute(ARCHITECTURE.toString(), "32bit"); + + DateFormat df = new SimpleDateFormat("yyyy-MM-dd'T'HH:mm:ss"); + df.setTimeZone(TimeZone.getTimeZone("UTC")); + // "If the timestamp is in UTC time, it ends with a 'Z'." + // https://github.com/sosy-lab/sv-witnesses/blob/main/README-GraphML.md + graph.addAttribute(CREATIONTIME.toString(), df.format(new Date()) + "Z"); + + Node v0 = new Node("N0"); + v0.addAttribute("entry", "true"); + Node v1 = new Node("N1"); + Node v2 = new Node("N2"); + + Edge edge = new Edge(v0, v1); + edge.addAttribute(CREATETHREAD.toString(), "0"); + graph.addEdge(edge); + edge = new Edge(v1, v2); + edge.addAttribute(THREADID.toString(), "0"); + edge.addAttribute(ENTERFUNCTION.toString(), "main"); + graph.addEdge(edge); + + int nextNode = 2; + int threads = 1; + + if (type.equals("correctness")) { + return graph; + } + + try (Model model = prover.getModel()) { + List execution = reOrderBasedOnAtomicity(context.getTask().getProgram(), getSCExecutionOrder(model)); + + for (int i = 0; i < execution.size(); i++) { + Event e = execution.get(i); + if (i + 1 < execution.size()) { + Event next = execution.get(i + 1); + if (e.hasEqualMetadata(next, SourceLocation.class) && e.getThread() == next.getThread()) { + continue; + } + } + + int cLine = e.hasMetadata(SourceLocation.class) ? e.getMetadata(SourceLocation.class).lineNumber() : -1; + edge = new Edge(new Node("N" + nextNode), new Node("N" + (nextNode + 1))); + edge.addAttribute(THREADID.toString(), valueOf(eventThreadMap.get(e))); + edge.addAttribute(STARTLINE.toString(), valueOf(cLine)); + + // End is also WRITE and PTHREAD, but it does not have + // CLines and thus won't create an edge (as expected) + if (e.hasTag(WRITE) && e.hasTag(PTHREAD)) { + edge.addAttribute(CREATETHREAD.toString(), valueOf(threads)); + threads++; + } + + // FIXME: The tracking of "globalId" here is very fragile + // If we generate a Witness and try to use it after adapting any processing pass + // the matching will fail. In particular, a Witness can only be validated + // by the version of Dartagnan that created it and only with identical + // configurations. + if (e instanceof Load l) { + edge.addAttribute(EVENTID.toString(), valueOf(e.getGlobalId())); + edge.addAttribute(LOADEDVALUE.toString(), String.valueOf(model.evaluate(context.result(l)))); + } + + if (e instanceof Store s) { + edge.addAttribute(EVENTID.toString(), valueOf(e.getGlobalId())); + Object valueObject = checkNotNull(model.evaluate(context.value(s))); + edge.addAttribute(STOREDVALUE.toString(), valueObject.toString()); + } + + graph.addEdge(edge); + + nextNode++; + if (e instanceof Assert) { + // FIXME: Execution of an assertion is not a problem, if the assertion holds! + break; + } + } + } catch (SolverException ignore) { + // The if above guarantees that if we reach this try, a Model exists + } + graph.getNode("N" + nextNode).addAttribute("violation", "true"); + return graph; + } + + private List getSCExecutionOrder(Model model) { + // TODO: we recently added many cline to many events and this might affect the + // witness generation. + Predicate executedCEvents = e -> Boolean.TRUE.equals(model.evaluate(context.execution(e))) + && e.hasMetadata(SourceLocation.class); + List execEvents = context.getTask().getProgram().getThreadEvents().stream().filter(executedCEvents) + .toList(); + Map> map = new HashMap<>(); + for (Event e : execEvents) { + // TODO improve this: these events correspond to return statements + if (e instanceof Store store && store.getMemValue() instanceof BConst bVal && !bVal.getValue()) { + continue; + } + BigInteger var = model.evaluate(context.clockVariable("hb", e)); + if (var != null) { + map.computeIfAbsent(var.intValue(), x -> new ArrayList<>()).add(e); + } } List exec = map.keySet().stream().sorted() - .flatMap(key -> map.get(key).stream()).collect(Collectors.toList()); + .flatMap(key -> map.get(key).stream()).collect(Collectors.toList()); return exec.isEmpty() ? execEvents : exec; - } - - private List reOrderBasedOnAtomicity(Program program, List order) { - List result = new ArrayList<>(); - Set processedEvents = new HashSet<>(); // Maintained for constant lookup time - // All the atomic blocks in the code that have to stay together in any execution - List> atomicBlocks = program.getThreadEvents().stream() - .filter(e -> e.hasTag(Tag.SVCOMP.SVCOMPATOMIC)) - .map(e -> ((EndAtomic)e).getBlock().stream(). - filter(order::contains). - collect(Collectors.toList())) - .toList(); - - for (Event next : order) { - if (processedEvents.contains(next)) { - // next was added as part of a previous block - continue; - } - List block = atomicBlocks.stream() - .filter(b -> Collections.binarySearch(b, next) >= 0).findFirst() - .orElseGet(() -> Collections.singletonList(next)); - result.addAll(block); - processedEvents.addAll(block); - } - return result; - } - - private String getFileSHA256(File file) { - try { - MessageDigest digest = MessageDigest.getInstance("SHA-256"); - - //Get file input stream for reading the file content - FileInputStream fis = new FileInputStream(file); - - //Create byte array to read data in chunks - byte[] byteArray = new byte[1024]; - int bytesCount = 0; - - //Read file data and update in message digest - while ((bytesCount = fis.read(byteArray)) != -1) { - digest.update(byteArray, 0, bytesCount); - }; - - //close the stream; We don't need it now. - fis.close(); - - //Get the hash's bytes - byte[] bytes = digest.digest(); - - //This bytes[] has bytes in decimal format; - //Convert it to hexadecimal format - StringBuilder sb = new StringBuilder(); - for(int i=0; i < bytes.length ;i++) { - sb.append(Integer.toString((bytes[i] & 0xff) + 0x100, 16).substring(1)); - } - - //return complete hash - return sb.toString(); - } catch (Exception e) { - e.printStackTrace(); - } - return ""; - } + } + + private List reOrderBasedOnAtomicity(Program program, List order) { + List result = new ArrayList<>(); + Set processedEvents = new HashSet<>(); // Maintained for constant lookup time + // All the atomic blocks in the code that have to stay together in any execution + List> atomicBlocks = program.getThreadEvents().stream() + .filter(e -> e.hasTag(Tag.SVCOMP.SVCOMPATOMIC)) + .map(e -> ((EndAtomic) e).getBlock().stream().filter(order::contains).collect(Collectors.toList())) + .toList(); + + for (Event next : order) { + if (processedEvents.contains(next)) { + // next was added as part of a previous block + continue; + } + List block = atomicBlocks.stream() + .filter(b -> Collections.binarySearch(b, next) >= 0).findFirst() + .orElseGet(() -> Collections.singletonList(next)); + result.addAll(block); + processedEvents.addAll(block); + } + return result; + } + + private String getFileSHA256(File file) { + try { + MessageDigest digest = MessageDigest.getInstance("SHA-256"); + + // Get file input stream for reading the file content + FileInputStream fis = new FileInputStream(file); + + // Create byte array to read data in chunks + byte[] byteArray = new byte[1024]; + int bytesCount = 0; + + // Read file data and update in message digest + while ((bytesCount = fis.read(byteArray)) != -1) { + digest.update(byteArray, 0, bytesCount); + } + ; + + // close the stream; We don't need it now. + fis.close(); + + // Get the hash's bytes + byte[] bytes = digest.digest(); + + // This bytes[] has bytes in decimal format; + // Convert it to hexadecimal format + StringBuilder sb = new StringBuilder(); + for (int i = 0; i < bytes.length; i++) { + sb.append(Integer.toString((bytes[i] & 0xff) + 0x100, 16).substring(1)); + } + + // return complete hash + return sb.toString(); + } catch (Exception e) { + e.printStackTrace(); + } + return ""; + } } \ No newline at end of file From 602be1696fdc45cf1f508dfcd747ec65417f2417 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 19 Dec 2023 10:56:38 +0100 Subject: [PATCH 3/3] Move computation of LTL string from summary to WitnessBuilder Signed-off-by: Hernan Ponce de Leon --- .../java/com/dat3m/dartagnan/Dartagnan.java | 16 +--------------- .../dat3m/dartagnan/witness/WitnessBuilder.java | 17 +++++++++++++++-- 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index fca9b24de4..718ac152e4 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -220,8 +220,7 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme final EnumSet properties = task.getProperty(); if (modelChecker.hasModel() && properties.contains(PROGRAM_SPEC)) { try { - String ltlProperty = getLtlPropertyFromSummary(summary); - WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, modelChecker.getResult(), ltlProperty); + WitnessBuilder w = WitnessBuilder.of(modelChecker.getEncodingContext(), prover, modelChecker.getResult(), summary); if (w.canBeBuilt()) { // We can only write witnesses if the path to the original C file was given. w.build().write(); @@ -232,19 +231,6 @@ private static void generateWitnessIfAble(VerificationTask task, ProverEnvironme } } - private static String getLtlPropertyFromSummary(String summary) { - if(summary.contains("integer overflow")) { - return "CHECK( init(main()), LTL(G ! overflow))"; - } - if(summary.contains("invalid dereference")) { - return "CHECK( init(main()), LTL(G valid-deref))"; - } - if(summary.contains("user assertion")) { - return "CHECK( init(main()), LTL(G ! call(reach_error())))"; - } - throw new UnsupportedOperationException("Violation found for unsupported property"); - } - public static String generateResultSummary(VerificationTask task, ProverEnvironment prover, ModelChecker modelChecker) throws SolverException { // ----------------- Generate output of verification result ----------------- final Program p = task.getProgram(); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java index 6801442b82..05dc153e71 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/WitnessBuilder.java @@ -62,11 +62,11 @@ public boolean canBeBuilt() { private final Map eventThreadMap = new HashMap<>(); - private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String ltl) { + private WitnessBuilder(EncodingContext c, ProverEnvironment p, Result r, String summary) { context = checkNotNull(c); prover = checkNotNull(p); type = r.equals(FAIL) ? "violation" : "correctness"; - ltlProperty = ltl; + ltlProperty = getLtlPropertyFromSummary(summary); } public static WitnessBuilder of(EncodingContext context, ProverEnvironment prover, Result result, @@ -76,6 +76,19 @@ public static WitnessBuilder of(EncodingContext context, ProverEnvironment prove return b; } + private static String getLtlPropertyFromSummary(String summary) { + if(summary.contains("integer overflow")) { + return "CHECK( init(main()), LTL(G ! overflow))"; + } + if(summary.contains("invalid dereference")) { + return "CHECK( init(main()), LTL(G valid-deref))"; + } + if(summary.contains("user assertion")) { + return "CHECK( init(main()), LTL(G ! call(reach_error())))"; + } + throw new UnsupportedOperationException("Violation found for unsupported property"); + } + public WitnessGraph build() { for (Thread t : context.getTask().getProgram().getThreads()) { for (Event e : t.getEntry().getSuccessors()) {