From 5e504ef4ad7ec9f393be1af53a40223462938e5c Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 14 Nov 2023 10:35:48 +0100 Subject: [PATCH 1/4] Return UNKNOWN instead of throwing an exception for SVCOMP unsupported properties --- svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 6b8eca7a61..f7d97d11e1 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -42,7 +42,9 @@ private void property(String p) { } else if(p.contains("unreach-call")) { property = Property.PROGRAM_SPEC; } else { - throw new IllegalArgumentException("Unrecognized property " + p); + // To comply with SVCOMP qualification rules, we should return UNKNOWN + // instead of throwing an exception for unhandled properties + property = null; } } @@ -93,6 +95,11 @@ public static void main(String[] args) throws Exception { SVCOMPRunner r = new SVCOMPRunner(); config.recursiveInject(r); + if(r.property == null) { + System.out.println("UNKNOWN"); + return; + } + WitnessGraph witness = new WitnessGraph(); if(r.witnessPath != null) { witness = new ParserWitness().parse(new File(r.witnessPath)); From 22616152336b673495097456ad258587c78c3c10 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 14 Nov 2023 10:44:37 +0100 Subject: [PATCH 2/4] Format --- .../java/com/dat3m/svcomp/SVCOMPRunner.java | 214 +++++++++--------- 1 file changed, 106 insertions(+), 108 deletions(-) diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index f7d97d11e1..2f8b6daafa 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -29,47 +29,47 @@ @Options public class SVCOMPRunner extends BaseOptions { - private Property property; - - @Option( - name= PROPERTYPATH, - required=true, - description="The path to the property to be checked.") - 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")) { - property = Property.PROGRAM_SPEC; - } else { + private Property property; + + @Option( + name= PROPERTYPATH, + required=true, + description="The path to the property to be checked.") + 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")) { + 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; - } - } + } + } - @Option( - name=UMIN, - description="Starting unrolling bound .") - private int umin = 1; + @Option( + name=UMIN, + description="Starting unrolling bound .") + private int umin = 1; - @Option( - name=UMAX, - description="Ending unrolling bound .") - private int umax = Integer.MAX_VALUE; + @Option( + name=UMAX, + description="Ending unrolling bound .") + private int umax = Integer.MAX_VALUE; - @Option( - name=STEP, - description="Step size for the increasing unrolling bound .") - private int step = 1; + @Option( + name=STEP, + description="Step size for the increasing unrolling bound .") + private int step = 1; - @Option( - name=VALIDATE, - description="Run Dartagnan as a violation witness validator. Argument is the path to the witness file.") - private String witnessPath; + @Option( + name=VALIDATE, + description="Run Dartagnan as a violation witness validator. Argument is the path to the witness file.") + private String witnessPath; - private static final Set supportedFormats = - ImmutableSet.copyOf(Arrays.asList(".c", ".i")); + private static final Set supportedFormats = + ImmutableSet.copyOf(Arrays.asList(".c", ".i")); public static void main(String[] args) throws Exception { @@ -78,22 +78,22 @@ public static void main(String[] args) throws Exception { return; } - if(Arrays.stream(args).noneMatch(a -> supportedFormats.stream().anyMatch(a::endsWith))) { - throw new IllegalArgumentException("Input program not given or format not recognized"); - } - if(Arrays.stream(args).noneMatch(a -> a.endsWith(".cat"))) { - throw new IllegalArgumentException("CAT model not given or format not recognized"); - } - File fileModel = new File(Arrays.stream(args).filter(a -> a.endsWith(".cat")).findFirst().get()); - String programPath = Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith)).findFirst().get(); - File fileProgram = new File(programPath); - - String[] argKeyword = Arrays.stream(args) - .filter(s->s.startsWith("-")) - .toArray(String[]::new); - Configuration config = Configuration.fromCmdLineArguments(argKeyword); - SVCOMPRunner r = new SVCOMPRunner(); - config.recursiveInject(r); + if(Arrays.stream(args).noneMatch(a -> supportedFormats.stream().anyMatch(a::endsWith))) { + throw new IllegalArgumentException("Input program not given or format not recognized"); + } + if(Arrays.stream(args).noneMatch(a -> a.endsWith(".cat"))) { + throw new IllegalArgumentException("CAT model not given or format not recognized"); + } + File fileModel = new File(Arrays.stream(args).filter(a -> a.endsWith(".cat")).findFirst().get()); + String programPath = Arrays.stream(args).filter(a -> supportedFormats.stream().anyMatch(a::endsWith)).findFirst().get(); + File fileProgram = new File(programPath); + + String[] argKeyword = Arrays.stream(args) + .filter(s->s.startsWith("-")) + .toArray(String[]::new); + Configuration config = Configuration.fromCmdLineArguments(argKeyword); + SVCOMPRunner r = new SVCOMPRunner(); + config.recursiveInject(r); if(r.property == null) { System.out.println("UNKNOWN"); @@ -102,11 +102,10 @@ public static void main(String[] args) throws Exception { WitnessGraph witness = new WitnessGraph(); if(r.witnessPath != null) { - witness = new ParserWitness().parse(new File(r.witnessPath)); - if(!fileProgram.getName(). - equals(Paths.get(witness.getProgram()).getFileName().toString())) { - throw new RuntimeException("The witness was generated from a different program than " + fileProgram); - } + witness = new ParserWitness().parse(new File(r.witnessPath)); + if(!fileProgram.getName().equals(Paths.get(witness.getProgram()).getFileName().toString())) { + throw new RuntimeException("The witness was generated from a different program than " + fileProgram); + } } int bound = witness.hasAttributed(UNROLLBOUND.toString()) ? parseInt(witness.getAttributed(UNROLLBOUND.toString())) : r.umin; @@ -116,66 +115,65 @@ public static void main(String[] args) throws Exception { while(output.equals("UNKNOWN")) { file = compileWithClang(fileProgram, ""); file = applyLlvmPasses(file); + + String llvmName = System.getenv().get("DAT3M_HOME") + "/output/" + Files.getNameWithoutExtension(programPath) + "-opt.ll"; - String llvmName = System.getenv().get("DAT3M_HOME") + "/output/" + - Files.getNameWithoutExtension(programPath) + "-opt.ll"; - - ArrayList cmd = new ArrayList<>(); - cmd.add("java"); - cmd.add("-Dlog4j.configurationFile=" + System.getenv().get("DAT3M_HOME") + "/dartagnan/src/main/resources/log4j2.xml"); - cmd.add("-DLOGNAME=" + Files.getNameWithoutExtension(programPath)); - cmd.addAll(Arrays.asList("-jar", System.getenv().get("DAT3M_HOME") + "/dartagnan/target/dartagnan.jar")); - cmd.add(fileModel.toString()); - cmd.add(llvmName); - cmd.add(String.format("--%s=%s", PROPERTY, r.property.asStringOption())); - cmd.add(String.format("--%s=%s", BOUND, bound)); - cmd.add(String.format("--%s=%s", WITNESS_ORIGINAL_PROGRAM_PATH, programPath)); - cmd.addAll(filterOptions(config)); - - ProcessBuilder processBuilder = new ProcessBuilder(cmd); - try { - Process proc = processBuilder.start(); - BufferedReader read = new BufferedReader(new InputStreamReader(proc.getInputStream())); - proc.waitFor(); - while(read.ready()) { - String next = read.readLine(); - // This is now the last line in the console. - // We avoid updating the output - if(next.contains("Total verification time(ms):")) { - break; - } - output = next; - System.out.println(output); - } - if(proc.exitValue() == 1) { - BufferedReader error = new BufferedReader(new InputStreamReader(proc.getErrorStream())); - while(error.ready()) { - System.out.println(error.readLine()); - } - System.exit(0); - } - } catch(Exception e) { - System.out.println(e.getMessage()); - System.exit(0); - } - if(bound > r.umax) { - System.out.println("PASS"); - break; - } - // We always do iterations 1 and 2 and then use the step - bound = bound == 1 ? 2 : bound + r.step; - } + ArrayList cmd = new ArrayList<>(); + cmd.add("java"); + cmd.add("-Dlog4j.configurationFile=" + System.getenv().get("DAT3M_HOME") + "/dartagnan/src/main/resources/log4j2.xml"); + cmd.add("-DLOGNAME=" + Files.getNameWithoutExtension(programPath)); + cmd.addAll(Arrays.asList("-jar", System.getenv().get("DAT3M_HOME") + "/dartagnan/target/dartagnan.jar")); + cmd.add(fileModel.toString()); + cmd.add(llvmName); + cmd.add(String.format("--%s=%s", PROPERTY, r.property.asStringOption())); + cmd.add(String.format("--%s=%s", BOUND, bound)); + cmd.add(String.format("--%s=%s", WITNESS_ORIGINAL_PROGRAM_PATH, programPath)); + cmd.addAll(filterOptions(config)); + + ProcessBuilder processBuilder = new ProcessBuilder(cmd); + try { + Process proc = processBuilder.start(); + BufferedReader read = new BufferedReader(new InputStreamReader(proc.getInputStream())); + proc.waitFor(); + while(read.ready()) { + String next = read.readLine(); + // This is now the last line in the console. + // We avoid updating the output + if(next.contains("Total verification time(ms):")) { + break; + } + output = next; + System.out.println(output); + } + if(proc.exitValue() == 1) { + BufferedReader error = new BufferedReader(new InputStreamReader(proc.getErrorStream())); + while(error.ready()) { + System.out.println(error.readLine()); + } + System.exit(0); + } + } catch(Exception e) { + System.out.println(e.getMessage()); + System.exit(0); + } + if(bound > r.umax) { + System.out.println("PASS"); + break; + } + // We always do iterations 1 and 2 and then use the step + bound = bound == 1 ? 2 : bound + r.step; + } } private static List filterOptions(Configuration config) { - // BOUND is computed based on umin and the information from the witness - List skip = Arrays.asList(PROPERTYPATH, UMIN, UMAX, STEP, SANITIZE, BOUND); + // BOUND is computed based on umin and the information from the witness + List skip = Arrays.asList(PROPERTYPATH, UMIN, UMAX, STEP, SANITIZE, BOUND); - return Arrays.stream(config.asPropertiesString().split("\n")). - filter(p -> skip.stream().noneMatch(s -> s.equals(p.split(" = ")[0]))). - map(p -> "--" + p.split(" = ")[0] + "=" + p.split(" = ")[1]). - collect(Collectors.toList()); + return Arrays.stream(config.asPropertiesString().split("\n")). + filter(p -> skip.stream().noneMatch(s -> s.equals(p.split(" = ")[0]))). + map(p -> "--" + p.split(" = ")[0] + "=" + p.split(" = ")[1]). + collect(Collectors.toList()); } } \ No newline at end of file From 7d6b01fc7b825c360354c49631d67951479af466 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 14 Nov 2023 18:30:02 +0100 Subject: [PATCH 3/4] Log a warning for unrecognized properties Signed-off-by: Hernan Ponce de Leon --- svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 2f8b6daafa..44d1438850 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -29,6 +29,8 @@ @Options public class SVCOMPRunner extends BaseOptions { + private static final Logger logger = LogManager.getLogger(SVCOMPRunner.class); + private Property property; @Option( @@ -96,6 +98,7 @@ public static void main(String[] args) throws Exception { config.recursiveInject(r); if(r.property == null) { + logger.warn("Unrecognized property"); System.out.println("UNKNOWN"); return; } From 53bdec7b248eb6dc757b0747f1e2d607a5c0a3d0 Mon Sep 17 00:00:00 2001 From: Hernan Ponce de Leon Date: Tue, 14 Nov 2023 22:30:38 +0100 Subject: [PATCH 4/4] Add missing imports --- svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java index 44d1438850..b33d1eae6c 100644 --- a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java +++ b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java @@ -19,6 +19,8 @@ import java.util.List; import java.util.Set; import java.util.stream.Collectors; +import org.apache.logging.log4j.LogManager; +import org.apache.logging.log4j.Logger; import static com.dat3m.dartagnan.configuration.OptionInfo.collectOptions; import static com.dat3m.dartagnan.configuration.OptionNames.*;