v0.8.0

Dockerfile

@@ -1,12 +1,18 @@
+# To upload the Docker images to Dockerhub, log into the Docker console, and then run
+#
+#   docker buildx build --push --platform linux/amd64,linux/arm64 -t aaronbembenek/formulog:vX.Y.Z .
+#
+# (with the appropriate version number substituted for X.Y.Z).
+
 FROM maven:3.8.6-openjdk-11 AS build
 WORKDIR /root/formulog/
 COPY src src
 COPY pom.xml pom.xml 
 RUN mvn package -DskipTests
 
 FROM ubuntu:23.04
-WORKDIR /root/formulog/
-ARG version=0.7.0-SNAPSHOT
+ARG version=0.8.0-SNAPSHOT
+WORKDIR /root/
 RUN apt-get update \
   && DEBIAN_FRONTEND=noninteractive \
   apt-get install -y \
@@ -28,13 +34,15 @@ RUN apt-get update \
   make \
   mcpp \
   python3 \
-  sqlite \
-  zlib1g-dev
-COPY --from=build /root/formulog/target/formulog-${version}-jar-with-dependencies.jar formulog.jar
-COPY examples examples
-RUN git clone https://github.com/souffle-lang/souffle.git \
+  sqlite3 \
+  zlib1g-dev \
+  # Install modified Souffle
+  && git clone --branch eager-eval https://github.com/aaronbembenek/souffle.git \
   && cd souffle \
-  && cmake -S . -B build \
-  && cmake --build build --target install -j 4 \
-  && cd .. \
-  && rm -rf souffle
+  && cmake -S . -B build -DCMAKE_BUILD_TYPE=Release -DSOUFFLE_ENABLE_TESTING=OFF \
+  && cmake --build build -j$(nproc) \
+  && cmake --build build --target install \
+  && cmake --build build --target clean
+WORKDIR /root/formulog/
+COPY --from=build /root/formulog/target/formulog-${version}-jar-with-dependencies.jar formulog.jar
+COPY examples examples

changelog.md

@@ -2,6 +2,27 @@
 
 All notable changes to this project will be documented in this file.
 
+## [0.8.0] - 2024-10-18
+
+### Added
+
+- Support for eager evaluation in both interpreter (`--eager-eval` option) and compiler.
+- Reorganized documentation and added a lot of new material, including a tutorial.
+- Apply Google Java format with Maven.
+- Various improvements to the code generator.
+
+### Changed
+
+- Better error reporting for type arity mismatch.
+- Clean up CI.
+- Better, more consistent CLI options for interpreter and generated code.
+
+### Fixed
+
+- Lexing of arithmetic expressions without spaces.
+- Various (rare) interpreter bugs.
+- Various bugs in the C++ runtime and generated code.
+
 ## [0.7.0] - 2023-02-14
 
 ### Added

docs/eval_modes/compile.md

@@ -14,7 +14,7 @@ Within this directory you can use `cmake` to compile the generated code into a b
 For example, to compile and execute the `greeting.flg` program from above, you can use these steps:
 
 ```
-java -jar formulog.jar -c greeting.flg && \
+java -jar formulog.jar -c examples/greeting.flg && \
   cd codegen && \
   cmake -B build -S . && \
   cmake --build build -j && \

docs/eval_modes/eager.md

@@ -16,7 +16,7 @@ When you configure `cmake` on the generated code, you need to add `-DFLG_EAGER_E
 For example, to build a version of the greeting program that uses eager evaluation, use these commands:
 
 ```
-java -jar formulog.jar -c greeting.flg && \
+java -jar formulog.jar -c examples/greeting.flg && \
   cd codegen && \
   cmake -B build -S . -DFLG_EAGER_EVAL=On && \
   cmake --build build -j && \

docs/starting.md

@@ -19,7 +19,7 @@ There are three main ways to set up Formulog (listed in increasing order of numb
 
 ### Use the Docker image
 
-Prebuilt images are available on [Docker Hub](https://hub.docker.com/r/aaronbembenek/formulog).
+Prebuilt images are available on [Docker Hub](https://hub.docker.com/r/aaronbembenek/formulog/tags).
 If you have Docker installed, you can spin up an Ubuntu container with Formulog, our custom version of Soufflé, and some example programs by running this command (replace `X.Y.Z` with the latest version):
 
 ```bash

docs/tutorial/index.md

@@ -35,7 +35,7 @@ Our typical approach when implementing an analysis in Formulog is thus to try to
 
 This is the approach we will follow in this tutorial: directly translate the formalism of JV as we encounter it, and then go back to patch our implementation as necessary.
 Concretely, we will work our way through JV Sections 3.1 and 3.2.
-For the full, final code, see [tutorial.flg](https://github.com/HarvardPL/formulog/blob/master/docs/tutorial/tutorial.flg).
+For the full, final code, see [tutorial.flg](https://github.com/HarvardPL/formulog/blob/master/examples/tutorial.flg).
 
 ## Definitions
 

docs/tutorial/tutorial.flg → examples/tutorial.flg

@@ -1,3 +1,10 @@
+(***
+
+This is the full code listing for the Formulog tutorial, which is available at
+<https://harvardpl.github.io/formulog/tutorial/>.
+
+***)
+
 (*******************************************************************************
 DEFINITIONS
 *******************************************************************************)

pom.xml

@@ -4,7 +4,7 @@
     <modelVersion>4.0.0</modelVersion>
     <groupId>edu.harvard.seas.pl</groupId>
     <artifactId>formulog</artifactId>
-    <version>0.7.0-SNAPSHOT</version>
+    <version>0.8.0-SNAPSHOT</version>
     <name>formulog</name>
     <properties>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>

src/main/java/edu/harvard/seas/pl/formulog/Main.java

@@ -69,7 +69,7 @@
 @Command(
     name = "formulog",
     mixinStandardHelpOptions = true,
-    version = "Formulog 0.7.0",
+    version = "Formulog 0.8.0",
     description = "Runs Formulog.")
 public final class Main implements Callable<Integer> {
 

src/main/java/edu/harvard/seas/pl/formulog/ast/Var.java

@@ -28,7 +28,7 @@
 import java.util.Set;
 import java.util.concurrent.atomic.AtomicInteger;
 
-public class Var extends AbstractTerm implements Term {
+public class Var extends AbstractTerm {
 
   static final AtomicInteger cnt = new AtomicInteger();
 

src/main/java/edu/harvard/seas/pl/formulog/db/SortedIndexedFactDb.java

@@ -27,8 +27,19 @@
 import edu.harvard.seas.pl.formulog.symbols.SymbolComparator;
 import edu.harvard.seas.pl.formulog.util.Pair;
 import edu.harvard.seas.pl.formulog.util.Util;
-import java.util.*;
+import java.lang.reflect.InvocationTargetException;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
 import java.util.Map.Entry;
+import java.util.NavigableSet;
+import java.util.Set;
 import java.util.concurrent.ConcurrentSkipListSet;
 import java.util.concurrent.atomic.AtomicInteger;
 import java.util.stream.Collectors;
@@ -511,7 +522,12 @@ private static IndexedFactSet make(List<Integer> order) {
       if (Configuration.genComparators) {
         try {
           cmp = gen.generate(a);
-        } catch (InstantiationException | IllegalAccessException e) {
+        } catch (InstantiationException
+            | IllegalAccessException
+            | IllegalArgumentException
+            | InvocationTargetException
+            | NoSuchMethodException
+            | SecurityException e) {
           throw new AssertionError(e);
         }
       } else {

src/main/java/edu/harvard/seas/pl/formulog/db/TupleComparatorGenerator.java

@@ -22,6 +22,7 @@
 import edu.harvard.seas.pl.formulog.ast.Term;
 import edu.harvard.seas.pl.formulog.util.IntArrayWrapper;
 import edu.harvard.seas.pl.formulog.util.Pair;
+import java.lang.reflect.InvocationTargetException;
 import java.util.Comparator;
 import java.util.Map;
 import java.util.concurrent.ConcurrentHashMap;
@@ -52,7 +53,12 @@ public class TupleComparatorGenerator extends ClassLoader {
   private Map<IntArrayWrapper, Comparator<Term[]>> memo = new ConcurrentHashMap<>();
 
   public Comparator<Term[]> generate(int[] accessPat)
-      throws InstantiationException, IllegalAccessException {
+      throws InstantiationException,
+          IllegalAccessException,
+          IllegalArgumentException,
+          InvocationTargetException,
+          NoSuchMethodException,
+          SecurityException {
     IntArrayWrapper key = new IntArrayWrapper(accessPat);
     Comparator<Term[]> cmp = memo.get(key);
     if (cmp == null) {
@@ -67,7 +73,12 @@ public Comparator<Term[]> generate(int[] accessPat)
 
   @SuppressWarnings("unchecked")
   public Comparator<Term[]> generate1(int[] accessPat)
-      throws InstantiationException, IllegalAccessException {
+      throws InstantiationException,
+          IllegalAccessException,
+          IllegalArgumentException,
+          InvocationTargetException,
+          NoSuchMethodException,
+          SecurityException {
     String className = "edu.harvard.seas.pl.formulog.db.CustomComparator" + cnt.getAndIncrement();
     ClassGen classGen =
         new ClassGen(
@@ -82,7 +93,7 @@ public Comparator<Term[]> generate1(int[] accessPat)
 
     byte[] data = classGen.getJavaClass().getBytes();
     Class<?> c = defineClass(className, data, 0, data.length);
-    return (Comparator<Term[]>) c.newInstance();
+    return (Comparator<Term[]>) c.getDeclaredConstructor().newInstance();
   }
 
   private void addCompareMethod(ClassGen cg, int[] accessPat) {

src/main/java/edu/harvard/seas/pl/formulog/validating/ValidRule.java

@@ -97,23 +97,23 @@ public static void order(
     atoms.addAll(newList);
   }
 
-  private static Set<Var> checkBody(Rule<UserPredicate, ComplexLiteral> rule)
-      throws InvalidProgramException {
-    Set<Var> boundVars = new HashSet<>();
-    Map<Var, Integer> varCounts = rule.countVariables();
-    for (ComplexLiteral lit : rule) {
-      if (!Unification.canBindVars(lit, boundVars, varCounts)) {
-        throw new InvalidProgramException(
-            "Rule cannot be evaluated given the supplied order.\n"
-                + "The problematic rule is:\n"
-                + rule
-                + "\nThe problematic literal is: "
-                + lit);
-      }
-      boundVars.addAll(lit.varSet());
-    }
-    return boundVars;
-  }
+  // private static Set<Var> checkBody(Rule<UserPredicate, ComplexLiteral> rule)
+  //     throws InvalidProgramException {
+  //   Set<Var> boundVars = new HashSet<>();
+  //   Map<Var, Integer> varCounts = rule.countVariables();
+  //   for (ComplexLiteral lit : rule) {
+  //     if (!Unification.canBindVars(lit, boundVars, varCounts)) {
+  //       throw new InvalidProgramException(
+  //           "Rule cannot be evaluated given the supplied order.\n"
+  //               + "The problematic rule is:\n"
+  //               + rule
+  //               + "\nThe problematic literal is: "
+  //               + lit);
+  //     }
+  //     boundVars.addAll(lit.varSet());
+  //   }
+  //   return boundVars;
+  // }
 
   private ValidRule(UserPredicate head, List<ComplexLiteral> body) {
     super(head, body);