diff --git a/build-aprove.xml b/build-aprove.xml index 1b6a2ba3..1a7f2cf4 100644 --- a/build-aprove.xml +++ b/build-aprove.xml @@ -760,4 +760,21 @@ + + + + + + + + + + + + + + + + + diff --git a/src/aprove/cli/Main.java b/src/aprove/cli/Main.java index 9be6fa1d..2892dc87 100644 --- a/src/aprove/cli/Main.java +++ b/src/aprove/cli/Main.java @@ -1,5 +1,6 @@ package aprove.cli; +import aprove.input.Programs.haskell.StrictPositivityException; import gnu.getopt.*; import java.io.*; @@ -23,6 +24,8 @@ import aprove.verification.oldframework.Logic.*; import aprove.verification.oldframework.Utility.GenericStructures.*; +import static aprove.verification.complexity.TruthValue.ComplexityYNM.MAYBE; + public class Main { private final static String HTML_FOOTER = ""; diff --git a/src/aprove/input/Programs/haskell/GraphBuilder.java b/src/aprove/input/Programs/haskell/GraphBuilder.java new file mode 100644 index 00000000..c13c11b3 --- /dev/null +++ b/src/aprove/input/Programs/haskell/GraphBuilder.java @@ -0,0 +1,275 @@ +package aprove.input.Programs.haskell; + +import aprove.verification.oldframework.Haskell.BasicTerms.Apply; +import aprove.verification.oldframework.Haskell.BasicTerms.Cons; +import aprove.verification.oldframework.Haskell.BasicTerms.Var; +import aprove.verification.oldframework.Haskell.Declarations.DataDecl; +import aprove.verification.oldframework.Haskell.Declarations.SynTypeDecl; +import aprove.verification.oldframework.Haskell.HaskellObject; +import aprove.verification.oldframework.Haskell.Modules.TyConsEntity; +import aprove.verification.oldframework.Haskell.Typing.DataCon; + +import java.util.*; +import java.util.stream.IntStream; + +public class GraphBuilder { + private final OccurrenceGraph graph; + + private String currentDef; + + private final Set datatypeNames; + + private Map paramIndex; + + private Map preludeTyCons; + + // should be read directly from Prelude + private Set preludeNames = new LinkedHashSet<>(Set.of( + "IO", "Either", "IOResult", "FilePath", "Integer", "ReadS", "Obj", "ShowS", + "Int", "Rational", "WHNF", "Maybe", "IOError", "Nat", "Float", "IOFinished", "HugsException", + "IOErrorKind", "Char", "Ordering", "Double", "String", "AET", "Ratio" + )); + + public GraphBuilder() { + this.datatypeNames = new HashSet<>(); + this.graph = new OccurrenceGraph(); + } + + public OccurrenceGraph buildFromDataDecl(List dataDecls, List synTypeDecls, Map preludeTyConsMap) { + this.preludeTyCons = preludeTyConsMap; + dataDecls.forEach(d -> datatypeNames.add(d.getDefType().getToken().getText())); + synTypeDecls.forEach(d -> datatypeNames.add(d.getDefType().getToken().getText())); + synTypeDecls.forEach(this::processSynTypes); + for (DataDecl d : dataDecls) { + processDataDecl(d, d.getDefType().getToken().getText()); + } + return graph; + } + + public OccurrenceGraph buildFromDataDecl(List dataDecls, List synTypeDecls) { + dataDecls.forEach(d -> datatypeNames.add(d.getDefType().getToken().getText())); + synTypeDecls.forEach(d -> datatypeNames.add(d.getDefType().getToken().getText())); + synTypeDecls.forEach(this::processSynTypes); + for (DataDecl d : dataDecls) { + processDataDecl(d, d.getDefType().getToken().getText()); + } + return graph; + } + + public OccurrenceGraph buildFromTyConsEntity(List types) { + for (TyConsEntity entity : types) { + datatypeNames.add(entity.getName()); + } + + for (TyConsEntity entity : types) { + processDataDecl((DataDecl) entity.getValue(), entity.getName()); + } + + return graph; + } + + private void processSynTypes(SynTypeDecl synTypeDecl) { + currentDef = synTypeDecl.getDefType().getToken().getText(); + paramIndex = new HashMap<>(); + + if (synTypeDecl.getDefType() instanceof Apply apply) { + //collect vars from data declaration + List vars = new ArrayList<>(); + var _ = flattenApp(apply, vars); + + //add vars to paramIndex with innermost index 0 + IntStream.range(0, vars.size()) + .forEach(index -> paramIndex.put(((Var) vars.get(index)).getSymbol().toString(), index)); + } + + graph.addNode( + new OccurrenceGraph.DefNode(currentDef) + ); + + walkType( + synTypeDecl.getType(), + Occurrence.STRICT_POS, + new OccurrenceGraph.DefNode(currentDef) + ); + + } + + private void processDataDecl(DataDecl dd, String name) { + //reset + currentDef = name; + paramIndex = new LinkedHashMap<>(); + + if (dd.getDefType() instanceof Apply apply) { + + //collect vars from data declaration + List vars = new ArrayList<>(); + var _ = flattenApp(apply, vars); + + //add vars to paramIndex with innermost index 0 + IntStream.range(0, vars.size()) + .forEach(index -> paramIndex.put(((Var) vars.get(index)).getSymbol().toString(), index)); + } + //create node + graph.addNode( + new OccurrenceGraph.DefNode(currentDef) + ); + + for (DataCon ctor : dd.getDataCons()) { + processConstructor(ctor); + } + + } + + /** + * Collects arguments from a data declaration and returns the head of the function + * + * @param app some Apply (e.g. Foo a b c) + * @param args array storing the arguments (e.g. Foo a b c => args = [a, b, c] + * @return head (Foo a b c => Foo) + */ + private HaskellObject flattenApp(Apply app, List args) { + List reversed = new ArrayList<>(); + HaskellObject current = app; + + while (current instanceof Apply apply) { + reversed.add(apply.getArgument()); + current = apply.getFunction(); + } + + for (int i = reversed.size() - 1; i >= 0; i--) { + args.add(reversed.get(i)); + } + + return current; + } + + private void processConstructor(DataCon ctor) { + // e.g. data List a = Nil | Cons a (List a) + // => ctor = `Cons a (List a)` + // => ctor.getTypes() -> ['a', '(List a)'] + for (var type : ctor.getTypes()) { + walkType( + type, + Occurrence.STRICT_POS, + new OccurrenceGraph.DefNode(currentDef) + ); + } + } + + private void walkType(HaskellObject type, Occurrence pol, OccurrenceGraph.Node target) { + if (type instanceof Cons cons) { + walkCons(cons, pol, target); + } else if (type instanceof Var var) { + walkVar(var, pol, target); + } else if (type instanceof Apply apply) { + walkApply(apply, pol, target); + } + } + + // e.g. Foo = mkFoo Bar => cons -> `Bar` + private void walkCons(Cons cons, Occurrence pol, OccurrenceGraph.Node target) { + String name = cons.getSymbol().toString(); + if (datatypeNames.contains(name)) { + graph.addEdge( + new OccurrenceGraph.DefNode(name), + target, + pol + ); + } else if (preludeTyCons != null && preludeTyCons.containsKey(name)) { + TyConsEntity entity = preludeTyCons.get(name); + if (entity.getValue() instanceof SynTypeDecl synTypeDecl) { + walkType(synTypeDecl.getType(), pol, target); + } else if (entity.getValue() instanceof DataDecl dataDecl) { + processDataDecl(dataDecl, name); + } + } + } + + private void walkVar(Var var, Occurrence pol, OccurrenceGraph.Node target) { + String name = var.getSymbol().toString(); + if (paramIndex.containsKey(name)) { + int index = paramIndex.get(name); + graph.addEdge( + new OccurrenceGraph.ArgNode(currentDef, index), + target, + pol + ); + } + } + + + private void walkApply(Apply apply, Occurrence pol, OccurrenceGraph.Node target) { + List args = new ArrayList<>(); + var head = flattenApp(apply, args); + + if (head instanceof Cons cons) { + + String name = cons.getSymbol().toString(); + + //check if arrow function + if (name.equals("->")) { + // System.out.println("WalkArrow called"); + walkArrow(apply, pol, target); + return; + } + + + if (datatypeNames.contains(name)) { + graph.addEdge( + new OccurrenceGraph.DefNode(name), + target, + pol + ); + } + + for (int i = 0; i < args.size(); i++) { + Occurrence argPol = pol.otimes(argPolarity(name)); + var argTarget = argTarget(name, i, target); + walkType(args.get(i), argPol, argTarget); + } + } else if (head instanceof Var var) { + String name = var.getSymbol().toString(); + walkType(head, pol, target); + if (paramIndex.containsKey(name)) { + int index = paramIndex.get(name); + target = new OccurrenceGraph.ArgNode(currentDef, index); + } + for (var a : args) { + walkType(a, pol.otimes(Occurrence.MIXED), target); + } + } else { + walkType(head, pol, target); + for (var a : args) { + walkType(a, pol.otimes(Occurrence.MIXED), target); + } + } + } + + private Occurrence argPolarity(String name) { + if (datatypeNames.contains(name) || preludeNames.contains(name)) { +// return Occurrence.GUARD_POS; + return Occurrence.STRICT_POS; + } + return Occurrence.MIXED; + } + + private OccurrenceGraph.Node argTarget( + String name, int argIndex, OccurrenceGraph.Node currentTarget + ) { + if (datatypeNames.contains(name) || preludeNames.contains(name)) { + return new OccurrenceGraph.ArgNode(name, argIndex); + } + return currentTarget; + } + + private void walkArrow(Apply apply, Occurrence pol, OccurrenceGraph.Node target) { + var codomain = apply.getArgument(); + if (apply.getFunction() instanceof Apply apply2) { + var domain = apply2.getArgument(); + walkType(domain, pol.otimes(Occurrence.JUST_NEG), target); + walkType(codomain, pol, target); + } else { + //should not happen + } + } +} diff --git a/src/aprove/input/Programs/haskell/HaskellParserCheck.java b/src/aprove/input/Programs/haskell/HaskellParserCheck.java new file mode 100644 index 00000000..64120292 --- /dev/null +++ b/src/aprove/input/Programs/haskell/HaskellParserCheck.java @@ -0,0 +1,7 @@ +package aprove.input.Programs.haskell; + +public class HaskellParserCheck extends RuntimeException { + public HaskellParserCheck(String message) { + super(message); + } +} diff --git a/src/aprove/input/Programs/haskell/Occurrence.java b/src/aprove/input/Programs/haskell/Occurrence.java new file mode 100644 index 00000000..cd4803cd --- /dev/null +++ b/src/aprove/input/Programs/haskell/Occurrence.java @@ -0,0 +1,72 @@ +package aprove.input.Programs.haskell; + +/** + * Occurrence is a + * complete lattice + * with least element 'MIXED' and greatest element 'UNUSED'. + */ +public enum Occurrence { + MIXED, // + and - + JUST_NEG, + JUST_POS, + STRICT_POS, + UNUSED; // does not occur + + /** + * Simulates behavior of additive of the Occurrence semiring (a+b): + * 'UNUSED' is neutral (zero) and 'MIXED' is dominant + * + * @param other the other Occurrence (b) added to 'this' (a) + * @return 'this + other' + */ + public Occurrence oplus(Occurrence other) { + + if (this == MIXED || other == MIXED) return MIXED; // dominant + + if (this == UNUSED) return other; + if (other == UNUSED) return this; + + if (this == JUST_NEG && other == JUST_NEG) return JUST_NEG; + if (this == JUST_NEG || other == JUST_NEG) return MIXED; + + if (this == STRICT_POS) return other; + if (other == STRICT_POS) return this; + + return JUST_POS; // both JUST_POS + } + + /** + * Simulates behavior of multiplicative of the Occurrence semiring (a*b): + * 'STRICT_POS' is neutral (one) and 'UNUSED' dominant + * + * @param other the other Occurrence (b) 'this' (a) is to be multiplied by + * @return 'this * other' + */ + public Occurrence otimes(Occurrence other) { + if (this == UNUSED || other == UNUSED) return UNUSED; + if (this == MIXED || other == MIXED) return MIXED; + if (this == JUST_NEG && other == JUST_NEG) return JUST_POS; + if (this == JUST_NEG || other == JUST_NEG) return JUST_NEG; + if (this == JUST_POS || other == JUST_POS) return JUST_POS; + return STRICT_POS; + } + + /** + * @return true => mixed, just negative or just positive,

false => strict positive, guarded positive or unused + */ + public boolean isNotStrictlyPositive() { + return this == MIXED || this == JUST_NEG || this == JUST_POS; + } + + + public String toPrettyString() { + return switch (this) { + case MIXED -> "±"; + case JUST_NEG -> "-"; + case JUST_POS -> "+"; + case STRICT_POS -> "++"; +// case GUARD_POS -> "g+"; + case UNUSED -> "0"; + }; + } +} diff --git a/src/aprove/input/Programs/haskell/OccurrenceGraph.java b/src/aprove/input/Programs/haskell/OccurrenceGraph.java new file mode 100644 index 00000000..81e21013 --- /dev/null +++ b/src/aprove/input/Programs/haskell/OccurrenceGraph.java @@ -0,0 +1,408 @@ +package aprove.input.Programs.haskell; + +import java.util.*; + +/** + * Graph consisting of DefNode and ArgNode with directed edges between them. + * Each edge has a certain polarity (Occurrence) + */ +public class OccurrenceGraph { + + // adjacency map edges + // we map a src -> (target -> occurrence) + private final Map> edges = new LinkedHashMap<>(); + //nodes + private final Set nodes = new LinkedHashSet<>(); + + // future use to handle Prelude + private final Set prelimNodes = new LinkedHashSet<>(Set.of( + new DefNode("ReadS") + , new DefNode("String") + , new ArgNode("ReadS", 0) + , new DefNode("ShowS") + , new DefNode("Char") + , new DefNode("Rational") + , new DefNode("Ratio") + , new DefNode("Integer") + , new ArgNode("Ratio", 0) + , new DefNode("FilePath") + , new DefNode("WHNF") + , new ArgNode("WHNF", 0) + , new DefNode("Nat") + , new DefNode("Maybe") + , new ArgNode("Maybe", 0) + , new DefNode("Either") + , new ArgNode("Either", 0) + , new ArgNode("Either", 1) + , new DefNode("Ordering") + , new DefNode("Int") + , new DefNode("Float") + , new DefNode("Double") + , new DefNode("IOError") + , new DefNode("IOErrorKind") + , new DefNode("Obj") + , new DefNode("IO") + , new DefNode("IOResult") + , new ArgNode("IO", 0) + , new DefNode("AET") + , new DefNode("HugsException") + , new DefNode("IOFinished") + , new ArgNode("IOFinished", 0) + )); + + //future use to handle Prelude + private final Map> prelimTypeEdges = new LinkedHashMap<>( + Map.ofEntries( + Map.entry( + new DefNode("String"), + Map.of( + new DefNode("ReadS"), Occurrence.MIXED, + new DefNode("ShowS"), Occurrence.MIXED, + new DefNode("FilePath"), Occurrence.STRICT_POS, + new DefNode("IOError"), Occurrence.STRICT_POS, + new ArgNode("Maybe", 0), Occurrence.STRICT_POS, + new DefNode("IO"), Occurrence.STRICT_POS, + new DefNode("AET"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new ArgNode("ReadS", 0), + Map.of( + new DefNode("ReadS"), Occurrence.MIXED + ) + ), + Map.entry( + new DefNode("Char"), + Map.of( + new DefNode("String"), Occurrence.MIXED + ) + ), + Map.entry( + new DefNode("Ratio"), + Map.of( + new DefNode("Rational"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new DefNode("Integer"), + Map.of( + new ArgNode("Ratio", 0), Occurrence.STRICT_POS + ) + ), + Map.entry( + new ArgNode("WHNF", 0), + Map.of( + new DefNode("WHNF"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new DefNode("Nat"), + Map.of( + new DefNode("Char"), Occurrence.STRICT_POS, + new DefNode("Int"), Occurrence.STRICT_POS, + new DefNode("Nat"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new ArgNode("Maybe", 0), + Map.of( + new DefNode("Maybe"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new ArgNode("Either", 0), + Map.of( + new DefNode("Either"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new ArgNode("Either", 1), + Map.of( + new DefNode("Either"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new DefNode("Int"), + Map.of( + new DefNode("Integer"), Occurrence.STRICT_POS, + new DefNode("Float"), Occurrence.STRICT_POS, + new DefNode("Double"), Occurrence.STRICT_POS, + new DefNode("IOResult"), Occurrence.STRICT_POS, + new DefNode("IOFinished"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new ArgNode("Ratio", 0), + Map.of( + new DefNode("Ratio"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new DefNode("IOErrorKind"), + Map.of( + new DefNode("IOError"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new DefNode("Maybe"), + Map.of( + new DefNode("IOError"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new DefNode("IOError"), + Map.of( + new DefNode("IO"), Occurrence.JUST_POS, + new DefNode("AET"), Occurrence.STRICT_POS, + new DefNode("IOResult"), Occurrence.MIXED, + new DefNode("IOFinished"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new DefNode("IOResult"), + Map.of( + new DefNode("IO"), Occurrence.MIXED, + new DefNode("IOResult"), Occurrence.MIXED + ) + ), + Map.entry( + new ArgNode("IO", 0), + Map.of( + new DefNode("IO"), Occurrence.JUST_POS + ) + ), + Map.entry( + new DefNode("AET"), + Map.of( + new DefNode("IO"), Occurrence.STRICT_POS + ) + ), + Map.entry( + new DefNode("HugsException"), + Map.of( + new DefNode("IOResult"), Occurrence.JUST_NEG + ) + ), + Map.entry( + new DefNode("Obj"), + Map.of( + new DefNode("IOResult"), Occurrence.MIXED + ) + ), + Map.entry( + new ArgNode("IOFinished", 0), + Map.of( + new DefNode("IOFinished"), Occurrence.STRICT_POS + ) + ) + ) + ); + + /** + * Adds a new edge to the graph + * + * @param source source node + * @param target target node + * @param occ polarity of the node + */ + public void addEdge(Node source, Node target, Occurrence occ) { + + if (!nodes.contains(source) && !prelimNodes.contains(source)) + nodes.add(source); + if (!nodes.contains(target) && !prelimNodes.contains(target)) + nodes.add(target); + + edges + .computeIfAbsent(source, k -> new LinkedHashMap<>()) + .merge(target, occ, Occurrence::oplus); + + } + + public void addNode(Node node) { + nodes.add(node); + } + + + /** + * Simple getter for all the nodes + * + * @return unmodifiable set of all the nodes in the graph + */ + public Set nodes() { + return Collections.unmodifiableSet(nodes); + } + + /** + * + * + * Returns the polarity of the direct edge (source -> target), returns UNUSED if no + * such edge exists + * + * @param source source node + * @param target target node + * @return polarity of the direct edge between source and target + */ + public Occurrence directEdge(Node source, Node target) { + return edges + .getOrDefault(source, Map.of()) + .getOrDefault(target, Occurrence.UNUSED); + } + + /** + * + * Returns all edges going out of the given node + * + * @param source node of the occurrence graph + * @return edges having the given node as source + */ + public Map outEdges(Node source) { + return edges.getOrDefault(source, Map.of()); + } + + /** + * multiplies all path polarities between source and target, using a dfs + * + * @param source source node + * @param target target node + * @return product of all path polarities + */ + public Occurrence transitiveOccurrence(Node source, Node target) { + //DFS: seen = pairs already explored + Set>> seen = new HashSet<>(); + return dfs(Optional.empty(), source, target, Optional.empty(), Occurrence.UNUSED, seen); + } + + /** + * Depth-first search (recursive) used to find all paths between two nodes and sums the polarities of each path + * to then multiply the polarities of the paths + * + * @param current current node + * @param target target node + * @param pathPol current path polarity + * @param acc accumulator, sum of all already traversed paths + * @param seen set of all nodes that were already traversed + * @return polarity + */ + private Occurrence dfs( + Optional previous, + Node current, + Node target, + Optional pathPol, + Occurrence acc, + Set>> seen + ) { + if (previous.isPresent()) { + var key = Map.entry(previous.get(), Map.entry(pathPol.orElse(Occurrence.UNUSED), current)); + if (seen.contains(key)) return acc; + seen.add(key); + } + if (current.equals(target) && pathPol.isPresent()) { + acc = acc.oplus(pathPol.get()); +// if (acc == Occurrence.MIXED) return acc; + return acc; + + } + + // Recurse into neighbours + for (var entry : outEdges(current).entrySet()) { + Node next = entry.getKey(); + Occurrence edgeOcc = entry.getValue(); + Occurrence newPath = pathPol + .map(p -> p.otimes(edgeOcc)) + .orElse(edgeOcc); + acc = dfs(Optional.of(current), next, target, Optional.of(newPath), acc, seen); + if (acc == Occurrence.MIXED) return acc; + } + + return acc; + } + + public String toStringWithoutUnused() { + var sb = new StringBuilder(); + for (var src : edges.keySet()) { + for (var edge : edges.get(src).entrySet()) { + if (!edge.getValue().equals(Occurrence.UNUSED)) { + sb.append(" ").append(src) + .append(" -[") + .append(edge.getValue().toPrettyString()) + .append("]-> ") + .append(edge.getKey()) + .append("\n"); + } + } + } + return (sb.length() == 0) ? " (empty graph)\n" : sb.toString(); + } + + public String prelimGraphToString() { + var sb = new StringBuilder(); + //form: src-[occ]->target + for (var node : prelimNodes) { + sb.append(" ").append(node).append("\n"); + } + + for (var src : prelimTypeEdges.keySet()) { + for (var edge : prelimTypeEdges.get(src).entrySet()) { + sb.append(" ").append(src) + .append(" -[") + .append(edge.getValue().toPrettyString()) + .append("]-> ") + .append(edge.getKey()) + .append("\n"); + } + } + return (sb.length() == 0) ? " (empty graph)\n" : sb.toString(); + } + + @Override + public String toString() { + var sb = new StringBuilder(); + //form: src-[occ]->target + for (var node : nodes) { + sb.append(" ").append(node).append("\n"); + } + + for (var src : edges.keySet()) { + for (var edge : edges.get(src).entrySet()) { + sb.append(" ").append(src) + .append(" -[") + .append(edge.getValue().toPrettyString()) + .append("]-> ") + .append(edge.getKey()) + .append("\n"); + } + } + return (sb.length() == 0) ? " (empty graph)\n" : sb.toString(); + } + + public sealed interface Node permits DefNode, ArgNode { + } + + /** + * Node in the Occurrence graph for a data definition + * e.g. `data Foo` => DefNode("Foo") + * + * @param name Name of the datatype + */ + public record DefNode(String name) implements Node { + @Override + public String toString() { + return name; + } + } + + /** + * Node in the Occurrence graph for an argument of a data definition + * e.g. `data Foo a` => ArgNode("Foo", 0) would represent "a" + * + * @param name Name of the datatype this argument belongs to + * @param index Index in which this argument appears in the data definition + */ + public record ArgNode(String name, int index) implements Node { + @Override + public String toString() { + return name + "." + index; + } + } + +} diff --git a/src/aprove/input/Programs/haskell/PositivityChecker.java b/src/aprove/input/Programs/haskell/PositivityChecker.java new file mode 100644 index 00000000..2c85e80c --- /dev/null +++ b/src/aprove/input/Programs/haskell/PositivityChecker.java @@ -0,0 +1,154 @@ +package aprove.input.Programs.haskell; + +import aprove.verification.oldframework.Haskell.BasicTerms.Apply; +import aprove.verification.oldframework.Haskell.BasicTerms.Cons; +import aprove.verification.oldframework.Haskell.Declarations.DataDecl; +import aprove.verification.oldframework.Haskell.Declarations.HaskellDecl; +import aprove.verification.oldframework.Haskell.Declarations.SynTypeDecl; +import aprove.verification.oldframework.Haskell.Expressions.HaskellExp; +import aprove.verification.oldframework.Haskell.HaskellObject; +import aprove.verification.oldframework.Haskell.Modules.*; +import aprove.verification.oldframework.Haskell.Modules.Module; +import aprove.verification.oldframework.Utility.GenericStructures.Pair; + +import java.util.*; + +public class PositivityChecker { + + private static String typeName(DataDecl decl) { + return decl.getDefType().getToken().getText(); + } + + private Result computeResult(Modules mods) { + + final Map modMap = mods.getModMap(); + final List decls = new ArrayList<>(List.of()); + + for (var module : modMap.values()) { + decls.addAll(module.getDecls()); + } +// may be helpful to have the prelude types in the graph, but not for now not consistent (e.g. Nat is not exported therefore Int not handled correctly) +// final Set entities = mods.getPrelude().getExpEntities(); +// final HashMap preludeTyCons = new HashMap<>(); +// for (HaskellEntity entity : entities) { +// if (entity instanceof TyConsEntity tyConsEntity && !Objects.equals(entity.getName(), "->")) { +// preludeTyCons.put(tyConsEntity.getName(), tyConsEntity); +// } +// } + + final List dataDecl = decls.stream() + .filter(decl -> decl instanceof DataDecl) + .map(decl -> (DataDecl) decl) + .toList(); + + final List synTypeDecls = decls.stream() + .filter(decl -> decl instanceof SynTypeDecl) + .map(decl -> (SynTypeDecl) decl) + .toList(); + + + GraphBuilder builder = new GraphBuilder(); + OccurrenceGraph graph = builder.buildFromDataDecl(dataDecl, synTypeDecls); +// OccurrenceGraph graph = builder.buildFromDataDecl(dataDecl, synTypeDecls, preludeTyCons); + + List violations = new ArrayList<>(); + Map selfLoops = new LinkedHashMap<>(); + + for (DataDecl d : dataDecl) { + var defNode = new OccurrenceGraph.DefNode(typeName(d)); + var loop = graph.transitiveOccurrence(defNode, defNode); + selfLoops.put(typeName(d), loop); + + if (loop.isNotStrictlyPositive()) { + violations.add(new Violation(d, loop)); + } + } + + return new Result(graph, violations, selfLoops); + } + + public void check(Modules mods) throws StrictPositivityException { +// debug(mods); + Result result = computeResult(mods); + if (!result.isValid()) { + StringBuilder sb = new StringBuilder(); + sb.append("Strict positivity check failed:\n"); + result.violations().forEach(v -> sb.append(" ").append(v).append("\n")); + throw new StrictPositivityException(sb.toString()); + } + } + + private void walkType(HaskellObject type){ + if (type instanceof Cons cons && cons.getSymbol().toString().equals("IOResult") && cons.getSymbol().getEntity().getModule().equals("Prelude")) throw new StrictPositivityException("IOResult type is not strictly positive"); + else if (type instanceof Apply apply) { + walkType(apply.getFunction()); + walkType(apply.getArgument()); + } + } + + public void checkForIOResult(Modules mods) { + Module main = mods.getMainModule(); + List> startTerms = mods.getStartTerms(); + for (Pair startTerm : startTerms) { + walkType(startTerm.getValue().getTypeTerm()); + } + for (HaskellEntity entity : main.getExpEntities()) { + if (entity.getName().equals("IOResult")) continue; // then it is user defined and was checked previously + else if (entity instanceof ConsEntity consEntity) walkType(consEntity.getType()); + else if (entity instanceof VarEntity varEntity) walkType(varEntity.getValue().getTypeTerm()); + } + } + + public void debug(Modules mods) { + System.out.println("=== Positivity check ==="); + Result result = computeResult(mods); + + System.out.println("Occurrence graph:"); +// System.out.println(result.graph.toStringWithoutUnused()); + System.out.println(result.graph); + + System.out.println("Self-loop polarities:"); + for (Map.Entry entry : result.selfLoops().entrySet()) { + String name = entry.getKey(); + Occurrence occ = entry.getValue(); + System.out.println(name + ": " + occ); + } + + if (result.isValid()) { + System.out.println("RESULT: PASSED (strictly positive)"); + } else { + System.out.println("RESULT: FAILED"); + result.violations().forEach(v -> System.out.println(" " + v)); + } + + System.out.println(); + } + + public record Violation(DataDecl datatype, Occurrence loopOccurrence) { + @Override + public String toString() { +// return typeName(datatype) + " is not strictly positive" + +// " (self-loop polarity = " + loopOccurrence.toString() + ")"; + return typeName(datatype) + " at line " + datatype.getToken().getLine() + " is not strictly positive" + + " (self-loop polarity = " + loopOccurrence.toString() + ")"; + } + + public DataDecl decl() { + return datatype; + } + + public Occurrence occ() { + return loopOccurrence; + } + } + + public record Result( + OccurrenceGraph graph, + List violations, + Map selfLoops + ) { + public boolean isValid() { + return violations.isEmpty(); + } + } +} diff --git a/src/aprove/input/Programs/haskell/StrictPositivityException.java b/src/aprove/input/Programs/haskell/StrictPositivityException.java new file mode 100644 index 00000000..eeea17c8 --- /dev/null +++ b/src/aprove/input/Programs/haskell/StrictPositivityException.java @@ -0,0 +1,7 @@ +package aprove.input.Programs.haskell; + +public class StrictPositivityException extends RuntimeException { + public StrictPositivityException(String message) { + super(message); + } +} diff --git a/src/aprove/input/Programs/haskell/Translator.java b/src/aprove/input/Programs/haskell/Translator.java index 046d7596..120aca6f 100644 --- a/src/aprove/input/Programs/haskell/Translator.java +++ b/src/aprove/input/Programs/haskell/Translator.java @@ -348,6 +348,10 @@ public void translate(final Input input) throws TranslationException { while (mods.needMoreModules()) { this.loadModule(mods.getNextNeededModule(), mods); } + + final PositivityChecker positivityChecker = new PositivityChecker(); + positivityChecker.check(mods); + this.setState(mods.buildHaskellProgram()); //JTreeDialog.create("Modules",new StructureTreeModel(new ReflectTreeEntry("","Modules",mods))).show(); @@ -384,6 +388,12 @@ public void translate(final Input input) throws TranslationException { } catch (final ParserException e) { this.handlePLException(e); this.setState(null); + }catch (final StrictPositivityException e) { + final ParseError pe = new ParseError(ParseError.ERROR); + pe.setMessage(e.getMessage()); + this.getErrors().add(pe); + this.setState(null); +// throw e; } catch (final LexerException e) { this.handlePLException(e); this.setState(null); diff --git a/src/aprove/runtime/AProVE.java b/src/aprove/runtime/AProVE.java index 9fcb8cf5..97fc86f4 100644 --- a/src/aprove/runtime/AProVE.java +++ b/src/aprove/runtime/AProVE.java @@ -4,10 +4,13 @@ import java.util.logging.*; import aprove.*; +import aprove.input.Programs.haskell.PositivityChecker; +import aprove.input.Programs.haskell.HaskellParserCheck; import aprove.input.Utility.*; import aprove.prooftree.Obligations.*; import aprove.strategies.ExecutableStrategies.*; import aprove.strategies.Parameters.*; +import aprove.verification.dpframework.HaskellProblem.HaskellProgram; import aprove.verification.dpframework.JBCProblem.*; import aprove.verification.oldframework.Input.*; import aprove.verification.oldframework.Input.Annotators.*; @@ -57,13 +60,23 @@ static boolean waitForHandle(final StrategyExecutionHandle handle, final long ti public AProVE(final Input input) throws SourceException { this.input = input; Globals.programFile = input.getPath(); - this.parse(null); + try { + this.parse(null); + } catch (final HaskellParserCheck e) { + System.exit(0); + } +// this.parse(null); this.metadata = this.buildMetadata(); } public AProVE(final Input input, final HandlingMode handlingMode) throws SourceException { this.input = input; - this.parse(handlingMode); + try { + this.parse(handlingMode); + } catch (final HaskellParserCheck e) { + System.exit(0); + } +// this.parse(handlingMode); this.metadata = this.buildMetadata(); } @@ -102,7 +115,7 @@ public ExecutableStrategy getResult() { public ObligationNode getRoot() { return this.root; } - + public TypedInput getTypedInput() { return this.typedInput; } @@ -179,6 +192,21 @@ private void parse(final HandlingMode forcedHandling) throws SourceException { Main.firstObligation = false; this.root = rootAndPositions.x; this.positions = rootAndPositions.y; + if (this.getTypedInput().getLanguage().equals(Language.HASKELL)) { + final PositivityChecker checker = new PositivityChecker(); + checker.checkForIOResult(((HaskellProgram) this.typedInput.getInput()).getModules()); + } + throw new HaskellParserCheck("Passed"); +// if (forcedHandling != null) { +// this.forceHandlingMode(forcedHandling); +// } +// final PublicAnnotator annotator = new DefaultAnnotator(); +// final AnnotatedInput annotate = annotator.annotate(this.typedInput); +// final ObligationFactory of = new MetaObligationFactory(); +// final Pair> rootAndPositions = of.getRootAndPositions(annotate); +// Main.firstObligation = false; +// this.root = rootAndPositions.x; +// this.positions = rootAndPositions.y; } } diff --git a/src/aprove/verification/oldframework/Input/TypeAnalyzers/ExtensionTypeAnalyzer.java b/src/aprove/verification/oldframework/Input/TypeAnalyzers/ExtensionTypeAnalyzer.java index 890f465c..f0d35720 100644 --- a/src/aprove/verification/oldframework/Input/TypeAnalyzers/ExtensionTypeAnalyzer.java +++ b/src/aprove/verification/oldframework/Input/TypeAnalyzers/ExtensionTypeAnalyzer.java @@ -3,6 +3,7 @@ import java.io.*; import java.util.*; +import aprove.input.Programs.haskell.StrictPositivityException; import aprove.input.Utility.*; import aprove.verification.oldframework.Input.*; import aprove.verification.oldframework.Rewriting.*;