tcr: Add configuration properties, improve output

lorenzleutgeb · Oct 23, 2020 · 508032d · 508032d
1 parent 703e399
commit 508032d
Show file tree

Hide file tree

Showing 21 changed files with 241 additions and 123 deletions.
diff --git a/typechecker/lac.properties b/typechecker/lac.properties
@@ -0,0 +1,39 @@
+# Logging
+# See http://www.slf4j.org/api/org/slf4j/impl/SimpleLogger.html
+org.slf4j.simpleLogger.defaultLogLevel=info
+org.slf4j.simpleLogger.showLogName=false
+org.slf4j.simpleLogger.dateTimeFormat=""
+org.slf4j.simpleLogger.showThreadName=false
+org.slf4j.simplelogger.levelInBrackets=true
+
+org.slf4j.simpleLogger.log.io.micronaut=info
+
+# Z3
+# Configuration properties for Z3 must be prefixed with `com.microsoft.z3`.
+# A list can be obtained by running `z3 -p` in a shell. The complete list
+# of parameters is very long. The most important ones are global parameters:
+# auto_config (bool) (default: true)
+# debug_ref_count (bool) (default: false)
+# dot_proof_file (string) (default: proof.dot)
+# dump_models (bool) (default: false)
+# memory_high_watermark (unsigned int) (default: 0)
+# memory_max_alloc_count (unsigned int) (default: 0)
+# memory_max_size (unsigned int) (default: 0) [bytes]
+# model (bool) (default: true)
+# model_validate (bool) (default: false)
+# proof (bool) (default: false)
+# rlimit (unsigned int) (default: 0)
+# smtlib2_compliant (bool) (default: false)
+# stats (bool) (default: false)
+# timeout (unsigned int) (default: 4294967295) [milliseconds]
+# trace (bool) (default: false)
+# trace_file_name (string) (default: z3.log)
+# type_check (bool) (default: true)
+# unsat_core (bool) (default: false)
+# verbose (unsigned int) (default: 0)
+# warning (bool) (default: true)
+# well_sorted_check (bool) (default: false)
+com.microsoft.z3.timeout=900000
+com.microsoft.z3.memory_max_size=25769803776
+com.microsoft.z3.unsat_core=true
+com.microsoft.z3.trace=false
diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/Main.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/Main.java
@@ -1,5 +1,9 @@
 package xyz.leutgeb.lorenz.lac;
 
+import java.io.IOException;
+import java.nio.file.Files;
+import java.nio.file.Paths;
+import java.util.Properties;
 import picocli.CommandLine;
 import picocli.CommandLine.Command;
 import xyz.leutgeb.lorenz.lac.commands.Haskell;
@@ -11,8 +15,27 @@
     subcommands = {LNF.class, Haskell.class, Run.class})
 public class Main implements Runnable {
   public static void main(String[] args) {
+    readProperties();
     new CommandLine(new Main()).execute(args);
   }
 
+  private static void readProperties() {
+    final var propertiesFile = Paths.get("lac.properties");
+    if (Files.exists(propertiesFile) && Files.isReadable(propertiesFile)) {
+      try (final var reader = Files.newBufferedReader(propertiesFile)) {
+        final Properties properties = new Properties();
+        properties.load(reader);
+        for (final var property : properties.entrySet()) {
+          if (!(property.getKey() instanceof String && property.getValue() instanceof String)) {
+            continue;
+          }
+          System.setProperty((String) property.getKey(), (String) property.getValue());
+        }
+      } catch (IOException ioException) {
+        ioException.printStackTrace();
+      }
+    }
+  }
+
   public void run() {}
 }
diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/Program.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/ast/Program.java
@@ -7,7 +7,6 @@
 import java.io.IOException;
 import java.io.PrintStream;
 import java.nio.file.Path;
-import java.nio.file.Paths;
 import java.util.Collections;
 import java.util.HashMap;
 import java.util.HashSet;
@@ -48,13 +47,16 @@ public class Program {
   @Getter private final List<List<String>> order;
 
   @Getter @Setter private String name;
-  private final Path basePath;
+  @Getter private final Path basePath;
 
-  public Program(Map<String, FunctionDefinition> functionDefinitions, List<List<String>> order) {
+  public Program(
+      Map<String, FunctionDefinition> functionDefinitions,
+      List<List<String>> order,
+      Path basePath) {
     this.functionDefinitions = functionDefinitions;
     this.order = order;
     this.name = flatten(this.order).stream().map(Util::fqnToFlatFilename).collect(joining("+"));
-    this.basePath = Paths.get(".", "out");
+    this.basePath = basePath;
   }
 
   public void infer() throws UnificationError, TypeError {
@@ -88,15 +90,15 @@ public Optional<Map<Coefficient, KnownCoefficient>> solve() {
     return solve(
         new HashMap<>(),
         new HashSet<>(),
-        (program, constraints) -> ConstraintSystemSolver.solve(constraints, name));
+        (program, constraints) -> ConstraintSystemSolver.solve(constraints, basePath));
   }
 
   public Optional<Map<Coefficient, KnownCoefficient>> solve(
       Map<String, CombinedFunctionAnnotation> functionAnnotations) {
     return solve(
         functionAnnotations,
         new HashSet<>(),
-        (program, constraints) -> ConstraintSystemSolver.solve(constraints, name));
+        (program, constraints) -> ConstraintSystemSolver.solve(constraints, basePath));
   }
 
   public Optional<Map<Coefficient, KnownCoefficient>> solve(
@@ -105,7 +107,7 @@ public Optional<Map<Coefficient, KnownCoefficient>> solve(
     return solve(
         functionAnnotations,
         outsideConstraints,
-        (program, constraints) -> ConstraintSystemSolver.solve(constraints, name));
+        (program, constraints) -> ConstraintSystemSolver.solve(constraints, basePath));
   }
 
   public Optional<Prover> prove(

diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Haskell.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Haskell.java
@@ -11,6 +11,7 @@
 import java.nio.file.Path;
 import java.util.regex.Pattern;
 import java.util.stream.Collectors;
+import lombok.extern.slf4j.Slf4j;
 import picocli.CommandLine;
 import xyz.leutgeb.lorenz.lac.ast.FunctionDefinition;
 import xyz.leutgeb.lorenz.lac.ast.Program;
@@ -19,6 +20,7 @@
 import xyz.leutgeb.lorenz.lac.unification.UnificationError;
 
 @CommandLine.Command(name = "hs")
+@Slf4j
 public class Haskell implements Runnable {
   @CommandLine.Parameters(
       index = "0",
@@ -91,7 +93,7 @@ public void run() {
       } catch (IOException ex) {
         ex.printStackTrace();
       }
-      System.out.println(path);
+      log.info("{}", path);
     }
   }
 }
diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Run.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/commands/Run.java
@@ -22,6 +22,7 @@
 import java.util.Set;
 import java.util.regex.Pattern;
 import java.util.stream.Collectors;
+import lombok.extern.slf4j.Slf4j;
 import picocli.CommandLine;
 import xyz.leutgeb.lorenz.lac.ast.FunctionDefinition;
 import xyz.leutgeb.lorenz.lac.ast.Program;
@@ -39,6 +40,7 @@
 import xyz.leutgeb.lorenz.lac.unification.UnificationError;
 
 @CommandLine.Command(name = "run")
+@Slf4j
 public class Run implements Runnable {
   @CommandLine.Parameters(
       index = "0",
@@ -108,7 +110,7 @@ public void run() {
     } catch (UnificationError | TypeError unificationError) {
       throw new RuntimeException(unificationError);
     }
-    // System.out.println("Loaded definitions:");
+    // log.info("Loaded definitions:");
     // program.printAllSimpleSignaturesInOrder(System.out);
     Multimap<String, FunctionDefinition> output = ArrayListMultimap.create();
     Multimap<String, String> imports = HashMultimap.create();
@@ -122,9 +124,11 @@ public void run() {
       }
     }
 
+    log.info("Output will go to {}", program.getBasePath().toAbsolutePath());
+
     Map<String, Path> tacticsMap = new HashMap<>();
 
-    // System.out.println(infer ? "Given for comparison:" : "Will check following types:");
+    // log.info(infer ? "Given for comparison:" : "Will check following types:");
 
     for (int i = 0; i < program.getOrder().size(); i++) {
       final var stratum = program.getOrder().get(i);
@@ -139,29 +143,28 @@ public void run() {
           }
         }
 
-        System.out.println(fd.getAnnotatedSignatureString());
+        log.info(fd.getAnnotatedSignatureString());
 
-        System.out.println("\tDependencies: " + fd.getOcurringFunctionsNonRecursive());
-        System.out.println("\tSource:       " + fd.getBody().getSource().getRoot());
+        log.info("\tDependencies: " + fd.getOcurringFunctionsNonRecursive());
+        log.info("\tSource:       " + fd.getBody().getSource().getRoot());
 
         if (tactics != null) {
           final var p = tacticsMap.get(fd.getFullyQualifiedName());
           if (p == null) {
-            System.out.println("\tTactic:       n/a (will use automatic proof generation)");
+            log.info("\tTactic:       n/a (will use automatic proof generation)");
           } else {
-            System.out.println("\tTactic:       " + p.toAbsolutePath());
+            log.info("\tTactic:       " + p.toAbsolutePath());
           }
         }
       }
     }
 
-    System.out.println();
-    System.out.println("Generating constraints...");
+    log.info("Generating constraints...");
     Optional<Prover> optionalProver = program.proveWithTactics(new HashMap<>(), tacticsMap, infer);
-    System.out.println("Done.");
+    log.info("Done.");
 
     if (optionalProver.isEmpty()) {
-      System.out.println("Nonterminating function definition detected. Aborting.");
+      log.info("Nonterminating function definition detected. Aborting.");
       System.exit(1);
       return;
     }
@@ -187,7 +190,7 @@ public void run() {
 
     Optional<Map<Coefficient, KnownCoefficient>> solution = Optional.empty();
 
-    System.out.println("Solving constraints...");
+    log.info("Solving constraints...");
     if (infer) {
       final List<UnknownCoefficient> setCountingRankCoefficients = new ArrayList<>();
       final List<UnknownCoefficient> setCountingNonRankCoefficients = new ArrayList<>();
@@ -249,9 +252,9 @@ public void run() {
       solution = prover.solve(outsideConstraints, emptyList(), "sat", domain);
     }
 
-    System.out.println("Done. Result(s): ");
+    log.info("Done. Result(s): ");
     if (solution.isEmpty()) {
-      System.out.println("UNSAT");
+      log.info("UNSAT");
       System.exit(1);
       return;
     }

diff --git a/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/module/Loader.java b/typechecker/src/main/java/xyz/leutgeb/lorenz/lac/module/Loader.java
@@ -1,13 +1,21 @@
 package xyz.leutgeb.lorenz.lac.module;
 
-import static java.util.stream.Collectors.*;
+import static java.util.stream.Collectors.toList;
+import static java.util.stream.Collectors.toMap;
+import static java.util.stream.Collectors.toUnmodifiableList;
 
 import com.google.common.base.Functions;
 import java.io.IOException;
 import java.io.OutputStream;
 import java.nio.file.Files;
 import java.nio.file.Path;
-import java.util.*;
+import java.util.Collections;
+import java.util.HashMap;
+import java.util.List;
+import java.util.Map;
+import java.util.Set;
+import java.util.Spliterators;
+import java.util.Stack;
 import java.util.function.Predicate;
 import java.util.regex.Pattern;
 import java.util.stream.Collectors;
@@ -40,6 +48,8 @@ public class Loader {
   private final Graph<String, DefaultEdge> g =
       new DefaultDirectedGraph<>(null, DefaultEdge::new, false);
 
+  @Getter private final String id = String.format("%08x", System.currentTimeMillis() * 31);
+
   public Loader(Path home) {
     if (!Files.exists(home) || !Files.isDirectory(home) || !Files.isReadable(home)) {
       throw new IllegalArgumentException("home must be an existing readable directory");
@@ -174,7 +184,8 @@ public Program load(Set<String> names) throws IOException {
             .collect(toMap(Functions.identity(), functionDefinitions::get)),
         stronglyConnectedSubgraphs.stream()
             .map(g -> g.vertexSet().stream().sorted().collect(toUnmodifiableList()))
-            .collect(toList()));
+            .collect(toList()),
+        Path.of(".", "out", id));
   }
 
   private Path path(String moduleName) {

diff --git a/...checker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/constraints/Constraint.java b/...checker/src/main/java/xyz/leutgeb/lorenz/lac/typing/resources/constraints/Constraint.java
@@ -3,6 +3,7 @@
 import static guru.nidi.graphviz.model.Factory.graph;
 import static guru.nidi.graphviz.model.Factory.node;
 import static xyz.leutgeb.lorenz.lac.util.Util.append;
+import static xyz.leutgeb.lorenz.lac.util.Util.output;
 import static xyz.leutgeb.lorenz.lac.util.Util.rawObjectNode;
 
 import com.google.common.collect.BiMap;
@@ -18,7 +19,6 @@
 import guru.nidi.graphviz.model.Graph;
 import guru.nidi.graphviz.model.Link;
 import guru.nidi.graphviz.model.Node;
-import java.nio.file.Files;
 import java.nio.file.Path;
 import java.util.Collections;
 import java.util.HashMap;
@@ -90,7 +90,7 @@ public static void plot(String name, Set<Constraint> constraints, Path path) {
       Graphviz.useEngine(lel);
       var viz = Graphviz.fromGraph(graph);
       Path target = path.resolve(name + "-constraints.svg");
-      try (final var out = Files.newOutputStream(target)) {
+      try (final var out = output(target)) {
         viz.engine(Engine.DOT).render(Format.SVG).toOutputStream(out);
         log.info("Wrote plot to {}", target);
       }