diff --git a/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java b/svcomp/src/main/java/com/dat3m/svcomp/SVCOMPRunner.java
index 6b8eca7a61..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.*;
@@ -29,45 +31,49 @@
@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 {
- throw new IllegalArgumentException("Unrecognized property " + p);
- }
- }
-
- @Option(
- name=UMIN,
- description="Starting unrolling bound <integer>.")
- private int umin = 1;
-
- @Option(
- name=UMAX,
- description="Ending unrolling bound <integer>.")
- private int umax = Integer.MAX_VALUE;
-
- @Option(
- name=STEP,
- description="Step size for the increasing unrolling bound <integer>.")
- 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;
-
- private static final Set<String> supportedFormats =
- ImmutableSet.copyOf(Arrays.asList(".c", ".i"));
+ private static final Logger logger = LogManager.getLogger(SVCOMPRunner.class);
+
+ 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 <integer>.")
+ private int umin = 1;
+
+ @Option(
+ name=UMAX,
+ description="Ending unrolling bound <integer>.")
+ private int umax = Integer.MAX_VALUE;
+
+ @Option(
+ name=STEP,
+ description="Step size for the increasing unrolling bound <integer>.")
+ 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;
+
+ private static final Set<String> supportedFormats =
+ ImmutableSet.copyOf(Arrays.asList(".c", ".i"));
public static void main(String[] args) throws Exception {
@@ -76,30 +82,35 @@ 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) {
+ logger.warn("Unrecognized property");
+ System.out.println("UNKNOWN");
+ return;
+ }
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;
@@ -109,66 +120,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<String> 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<String> 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<String> filterOptions(Configuration config) {
- // BOUND is computed based on umin and the information from the witness
- List<String> skip = Arrays.asList(PROPERTYPATH, UMIN, UMAX, STEP, SANITIZE, BOUND);
+ // BOUND is computed based on umin and the information from the witness
+ List<String> 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