forked from i21017/JavaTypeUnify
Compare commits
8
Commits
| Author | SHA1 | Date | |
|---|---|---|---|
  stanandClaude Opus 5
|
79c9191dd2 | ||
|
stanandClaude Opus 5
|
e65260fc28 | ||
|
stanandClaude Opus 5
|
5e9cac84d3 | ||
|
stanandClaude Opus 5
|
6057af29f5 | ||
|
stanandClaude Opus 5
|
9affd1ba8f | ||
|
stanandClaude Opus 5
|
5807f2bca8 | ||
|
stanandClaude Opus 5
|
738bb40634 | ||
|
stanandClaude Opus 5
|
c0dcc8209d |
No files matched your search
@@ -0,0 +1,275 @@
|
||||
# Fix for ASP Bug 1 — solutions could violate a placeholder's upper bounds
|
||||
|
||||
Fixes the bug logged as **Bug 1** in `../ASP_BUGS.md`. One rule was added to
|
||||
`src/main/asp/unifyDiss.lp`; nothing else in the repository was changed.
|
||||
|
||||
---
|
||||
|
||||
## The bug
|
||||
|
||||
`unifyDiss.lp` could solve a placeholder with a type that violates that placeholder's own upper
|
||||
bounds — most visibly `java.lang.Object`, which the S-Object rules add as an upper bound for
|
||||
*every* placeholder.
|
||||
|
||||
Minimal reproduction, self-contained (no `gen-facts` run needed — this is exactly what
|
||||
`gen-facts` emits for `_a <. java.lang.Boolean,` plus the one relevant `jdkHierarchy.lp` fact):
|
||||
|
||||
```prolog
|
||||
% repro_bug1.lp
|
||||
orCons(undCons(subcons(tph("_a"),type("java.lang.Boolean",null)), null), null).
|
||||
subtype(type("java.lang.Boolean",null), type("java.lang.Object",null)).
|
||||
```
|
||||
|
||||
```sh
|
||||
clingo -n 0 repro_bug1.lp src/main/asp/unifyDiss.lp src/main/asp/show.lp
|
||||
```
|
||||
|
||||
Before the fix — three answer sets, two of them wrong:
|
||||
|
||||
```
|
||||
Answer: 1 sigma(tph("_a"),type("java.lang.Object",null))
|
||||
Answer: 2 sigma(tph("_a"),type("java.lang.Boolean",null))
|
||||
Answer: 3 sigma(tph("_a"),type("java.lang.Boolean",null)) sigma(tph("_a"),type("java.lang.Object",null))
|
||||
```
|
||||
|
||||
`java.lang.Object` is not a subtype of `java.lang.Boolean`, so Answer 1 violates the only input
|
||||
constraint — and since `pipeline.sh` runs `clingo -n 1`, that was the answer the pipeline used.
|
||||
|
||||
The or-constraint variant, where two placeholders must land on the *same* alternative:
|
||||
|
||||
```prolog
|
||||
% repro_bug1b.lp
|
||||
% { _a <. java.lang.Byte, _b <. java.lang.Byte | _a <. java.lang.Integer, _b <. java.lang.Integer }
|
||||
orCons(undCons(subcons(tph("_b"),type("java.lang.Byte",null)),undCons(subcons(tph("_a"),type("java.lang.Byte",null)), null)),orCons(undCons(subcons(tph("_b"),type("java.lang.Integer",null)),undCons(subcons(tph("_a"),type("java.lang.Integer",null)), null)), null)).
|
||||
subtype(type("java.lang.Byte",null), type("java.lang.Number",null)).
|
||||
subtype(type("java.lang.Integer",null), type("java.lang.Number",null)).
|
||||
subtype(type("java.lang.Number",null), type("java.lang.Object",null)).
|
||||
```
|
||||
|
||||
Before the fix, 18 answer sets; the first was
|
||||
`sigma(tph("_a"),…Integer) sigma(tph("_b"),…Object)` — `_b` outside both alternatives.
|
||||
|
||||
---
|
||||
|
||||
## Root cause
|
||||
|
||||
Not a missing check on the *solution*, but a missing check on the *constraints*.
|
||||
|
||||
Once `Solution-Gen` assigns a type to a placeholder, `subst` and the `subst-L` / `subst-R` rules
|
||||
rewrite every constraint mentioning that placeholder into a constraint over the substituted
|
||||
types. Inspecting the bad model shows the violated constraint is already sitting in it:
|
||||
|
||||
```
|
||||
subst(tph("_a"), type("java.lang.Object",null)) % the chosen solution
|
||||
subcons(tph("_a"), type("java.lang.Boolean",null)) % the input constraint
|
||||
subcons(type("java.lang.Object",null), type("java.lang.Boolean",null)) % <- derived by subst-L
|
||||
```
|
||||
|
||||
That last atom says `Object <. Boolean`. It contains no placeholders, so it is decidable against
|
||||
the class hierarchy, and it is plainly false — but `unifyDiss.lp` had **no fail conditions at
|
||||
all**, so nothing ever looked at it. The sibling encodings do have this check
|
||||
(`unify.lp:118`, `unifyOrCons.lp:124`, `unifyPaper.lp:126`, all `% fail for adapt`);
|
||||
`unifyDiss.lp` was missing that whole section.
|
||||
|
||||
### Matches the dissertation
|
||||
|
||||
`../dissertation/chapters/unifyWithASP.tex:723` defines the rule:
|
||||
|
||||
> **Fail-Subtype**: `G₁ <. G₂`, `G₁ ≮: G₂` ⟹ ∅
|
||||
|
||||
and line 867 states the ground-only restriction explicitly:
|
||||
|
||||
> *"**Fail-Subtype** rejects any stable model containing a ground subtype constraint `G₁ <. G₂`
|
||||
> where `G₁ ≮: G₂` in the Java class hierarchy […] Crucially, both rules only apply to*
|
||||
> ground *types `G` — types containing no placeholders. This is intentional: a constraint such as
|
||||
> `Box<a> ≐ Box<b>` cannot be validated until `a` and `b` are assigned concrete types."*
|
||||
|
||||
Line 946 adds that this restriction is what `Solution-Requirement` exists for: every placeholder
|
||||
must be assigned a type, otherwise a constraint could stay non-ground and dodge the check.
|
||||
|
||||
---
|
||||
|
||||
## The fix
|
||||
|
||||
Added to `src/main/asp/unifyDiss.lp`, directly after `Solution-Requirement`:
|
||||
|
||||
```prolog
|
||||
:- subcons(S, T), groundType(S), groundType(T), not subtype(S, T).
|
||||
|
||||
groundType(T) :- typeTerm(T), not containsTph(T).
|
||||
% + containsTph/1 (recursive over params/1..3) and typeTerm/1 (every type term occurring in a
|
||||
% constraint, including those nested in type parameters)
|
||||
```
|
||||
|
||||
Notes on the shape of the rule:
|
||||
|
||||
- **Ground-only is required for soundness, not an optimisation.** A constraint still containing a
|
||||
placeholder is not yet decided and must remain satisfiable by a later substitution.
|
||||
- **The subtype relation is not weakened.** The check uses `subtype/2` as-is, on whole type terms,
|
||||
so a parameterized type still only conforms to a bound with the very same parameters. An
|
||||
erasure-level variant (comparing class names only, as `unifyPaper.lp`'s `namedSubtype/2` does)
|
||||
was deliberately *not* used, since it would let `Box<Integer>` satisfy a `Box<String>` bound.
|
||||
- **The hierarchy must now be complete enough.** Because the check is only as good as `subtype/2`,
|
||||
a type mentioned in no `subtype/2` fact at all has no derivable `T <: T` and its constraints
|
||||
become unsatisfiable. Running `repro_bug1.lp` *without* `jdkHierarchy.lp` is UNSAT, where it
|
||||
previously returned (wrong) answers. `pipeline.sh` always passes `jdkHierarchy.lp`, so this only
|
||||
affects callers that invoke clingo directly — and failing loudly beats answering wrongly.
|
||||
|
||||
---
|
||||
|
||||
## Verification
|
||||
|
||||
### The reported cases
|
||||
|
||||
| Input | Before | After |
|
||||
|---|---|---|
|
||||
| `repro_bug1.lp` | 3 models, incl. `Object` and a double-`sigma` one | **1 model**, `java.lang.Boolean` |
|
||||
| `repro_bug1b.lp` | 18 models, first one invalid | **2 models**: both `Byte`, or both `Integer` |
|
||||
|
||||
Both match the "Expected" in `../ASP_BUGS.md` exactly.
|
||||
|
||||
### Regression suite
|
||||
|
||||
All 37 `.java` files under
|
||||
`../JavaConstraintGenerator/src/test/resources/java-samples/testinput/`, each run through
|
||||
`gen-facts` and then `clingo -n 1 … unifyDiss.lp jdkHierarchy.lp show.lp`:
|
||||
|
||||
| | Before | After |
|
||||
|---|---|---|
|
||||
| SAT | 33 | 32 |
|
||||
| UNSAT | 4 | 5 |
|
||||
|
||||
The 4 pre-existing UNSATs (3× `MethodReference`, 1× `TypeParameter`) are Bug 3 and are unchanged.
|
||||
The one new UNSAT is `WholeProject/Matrix.java` — see below.
|
||||
|
||||
Seven samples (excluding Matrix) produce a different model. The real-world effects named in
|
||||
`../ASP_BUGS.md` are fixed:
|
||||
|
||||
| Sample | Before | After |
|
||||
|---|---|---|
|
||||
| `ControlFlow/IfExample` | `_0 = Object` (javac rejects as `if` condition) | `_0 = Boolean` |
|
||||
| `ControlFlow/WhileExample` | `_0 = Object` | `_0 = Boolean` |
|
||||
| `EqualityExpression/EqualityIntInt` | `_0 = Byte`, `_1 = Object` (mixed alternatives) | both `Object` — one alternative |
|
||||
| `EqualityExpression/EqualityBoolean` | `_0` had **two** sigmas (`Byte` *and* `Object`) | single sigma per placeholder |
|
||||
| `RelationalExpression/RelationalIntInt` | `_0 = Double`, `_1 = Object` | both `Double` |
|
||||
|
||||
Note the fix constrains *validity*, not *minimality* — it removes invalid models but does not
|
||||
make clingo prefer the tightest type. In `MethodCall/StringResultAsParameter` the first model
|
||||
changed from `_0 = String` to `_0 = Object`; both are valid for that constraint set and the
|
||||
solved file still compiles. The total number of `Object`-typed placeholders across the suite
|
||||
barely moves (41 → 40, excluding Matrix); what changes is that the remaining ones are now
|
||||
constraint-satisfying.
|
||||
|
||||
### End-to-end (`pipeline.sh`, javac before vs. after)
|
||||
|
||||
34 single-file samples: 25 compile after solving, 5 UNSAT, 3 negative fixtures that do not
|
||||
compile before *or* after (`UnresolvableMethodReference`, `StaticImportUser`,
|
||||
`UnresolvableQualifiedChain` — the latter two need their sibling files), and 1 regression
|
||||
(`SimpleReturn`, below).
|
||||
|
||||
---
|
||||
|
||||
## Known fallout — two pre-existing defects the missing check was hiding
|
||||
|
||||
Both are outside Bug 1 and are **not** fixed here.
|
||||
|
||||
### 1. `WholeProject/Matrix.java` is now UNSAT
|
||||
|
||||
Its previous "solution" *was* the bug: nearly every placeholder solved as `java.lang.Object`,
|
||||
including `_Matrix_7 <. java.lang.Boolean` solved as `Object`, plus a contradictory double-`sigma`
|
||||
for `_Matrix_22`. It only ever looked like a success because the solution applier refuses to write
|
||||
`java.lang.Object` into a source file.
|
||||
|
||||
The reason no valid solution exists: `Matrix extends Vector<Vector<Integer>>`, but the generator
|
||||
emits the extends-relation **raw**, as `Matrix < java.util.Vector` (line 1 of its `.cons`). The
|
||||
type argument is lost, so no `subtype(type("Matrix",null), type("java.util.Vector",params(…)))`
|
||||
fact exists and the ground constraint `Matrix <. Vector<Object>` cannot be confirmed. Minimizing
|
||||
the number of violated ground constraints gives an irreducible core of 3, all against the same
|
||||
bound `java.util.Vector<java.lang.Object>`.
|
||||
|
||||
This is a `JavaConstraintGenerator` issue — the type argument never reaches the `.cons` file — and
|
||||
is unaffected by how `JavaTypeUnifyASP` encodes extends relations (verified: the result is
|
||||
identical either way).
|
||||
|
||||
### 2. `Return/SimpleReturn.java` — solved output no longer compiles
|
||||
|
||||
The new model is *valid for the constraint set given*: it selects the string-concatenation
|
||||
alternative of the `+` or-constraint (`_0 <. String, Integer <. Integer, String <. _3`), yielding
|
||||
`Integer compute(java.lang.String x)`, which javac rejects at `return y;`.
|
||||
|
||||
The constraint set is incomplete: `_SimpleReturn_3` has **no** upper bound at all. The method's
|
||||
declared return type `Integer` stays literal rather than becoming a placeholder, and the generator
|
||||
emits no `_SimpleReturn_3 <. java.lang.Integer` for `return y;`. (Contrast `Return/MultipleReturns`
|
||||
and `Return/StringLiteralReturn`, where the return type *is* a placeholder and the returned value
|
||||
flows in as a lower bound.) Previously the solver's invalid all-`Object` model happened to compile;
|
||||
now a valid model exposes the missing constraint. Fixing this belongs in
|
||||
`JavaConstraintGenerator`.
|
||||
|
||||
### Not a gap: `subtype/2` and parameterized types
|
||||
|
||||
While measuring the above, `_a <. java.util.Vector<java.lang.Integer>` appeared to go UNSAT under
|
||||
Fail-Subtype, suggesting `subtype/2` could not relate parameterized types at all. That was an
|
||||
artifact of an **uncommitted local change** to `ASPGenerator.generateExtendsRelations`, which
|
||||
emitted each extends relation as a bare fact
|
||||
|
||||
```prolog
|
||||
subtype(type("Box",params(XX)),type("java.lang.Object",null)). % unsafe variable XX
|
||||
```
|
||||
|
||||
instead of the guarded rule the method originally produced:
|
||||
|
||||
```prolog
|
||||
subtype(type("Box",params(XX)),type("java.lang.Object",null)) :- subtype(type("Box",params(XX))).
|
||||
```
|
||||
|
||||
The guard is **not** self-referential: its head is `subtype/2` while its body is `subtype/**1**`,
|
||||
a distinct predicate that `unifyDiss.lp:77` derives (`subtype(type(A, P)) :- subcons(type(A, P), _).`)
|
||||
to mark "this type actually occurs in the constraints". The body is what *binds* `XX`, so the
|
||||
guarded form is safe and instantiates the relation for the type arguments that really occur.
|
||||
|
||||
That local change has been reverted, restoring the committed behaviour. With the guarded form:
|
||||
|
||||
- `_a <. java.util.Vector<java.lang.Integer>` → exactly one model, `Vector<Integer>`. No
|
||||
reflexivity rule is needed; `subtype(A,A) :- subtype(A,B).` fires once the guarded rule
|
||||
instantiates `subtype(Vector<Integer>, Object)`.
|
||||
- **Bug 4** of `../ASP_BUGS.md` (parameterized extends-relations producing `error: unsafe
|
||||
variables`) no longer reproduces — it was caused by that local change.
|
||||
- **Bug 3**'s input in the parameterized-extends form (`Box<X> < java.lang.Object`) now solves to
|
||||
`sigma(tph("_a"), type("Box",params(type("java.lang.Integer",null))))`.
|
||||
|
||||
A reflexivity rule (`subtype(type(C,P), type(C,P)) :- typeTerm(type(C,P)).`) was prototyped
|
||||
against the broken fact form and has been **reverted** — it is unnecessary.
|
||||
|
||||
Bug 3 as written in `../ASP_BUGS.md` (a *raw* `Box < java.lang.Object` declaration combined with a
|
||||
parameterized `Box<java.lang.Integer>` use) is still UNSAT and remains open: the guard
|
||||
`subtype(type("Box",null))` never holds, because the constraints only ever mention `Box<Integer>`.
|
||||
`dissertation/chapters/unifyWithASP.tex:516` notes the intended relation coincides with
|
||||
Featherweight Generic Java's.
|
||||
|
||||
---
|
||||
|
||||
## Reproducing this
|
||||
|
||||
```sh
|
||||
cd JavaTypeUnifyASP
|
||||
|
||||
# the two minimal cases (paste the two .lp blocks above into files first)
|
||||
clingo -n 0 repro_bug1.lp src/main/asp/unifyDiss.lp src/main/asp/show.lp
|
||||
clingo -n 0 repro_bug1b.lp src/main/asp/unifyDiss.lp src/main/asp/show.lp
|
||||
|
||||
# a full sample, end to end
|
||||
cd .. && ./pipeline.sh JavaConstraintGenerator/src/test/resources/java-samples/testinput/ControlFlow/IfExample.java
|
||||
```
|
||||
|
||||
To see *which* ground constraints a model violates, turn the integrity constraint into an
|
||||
observable atom:
|
||||
|
||||
```sh
|
||||
sed 's/^ :- subcons(S, T), groundType(S), groundType(T), not subtype(S, T)\./violation(S,T) :- subcons(S, T), groundType(S), groundType(T), not subtype(S, T)./' \
|
||||
src/main/asp/unifyDiss.lp > debug.lp
|
||||
echo '#show violation/2.' > showv.lp
|
||||
clingo -n 1 facts.lp debug.lp src/main/asp/jdkHierarchy.lp showv.lp
|
||||
```
|
||||
|
||||
Adding `#minimize { 1, S, T : violation(S, T) }.` and `--opt-mode=optN` gives the irreducible set
|
||||
of unsatisfiable ground constraints — that is how the `Matrix` core above was found.
|
||||
@@ -0,0 +1,83 @@
|
||||
# JavaTypeUnifyASP
|
||||
|
||||
Step ② of the pipeline: **typing constraints → a type assignment.** Takes the `.cons` file
|
||||
[JavaConstraintGenerator](../ConstraintGeneration.md) produces, turns it into ASP facts, solves
|
||||
them with [clingo](https://potassco.org/clingo/), and turns the answer set back into JSON.
|
||||
|
||||
See [../README.md](../README.md) for the whole flow and
|
||||
[`src/main/asp/unifyFinal.lp`](src/main/asp/unifyFinal.lp) for the encoding, whose comments map
|
||||
every rule to its counterpart in the dissertation.
|
||||
|
||||
## CLI
|
||||
|
||||
```sh
|
||||
java -jar target/JavaTXcompiler-0.1-jar-with-dependencies.jar <subcommand> [args]
|
||||
```
|
||||
|
||||
| Subcommand | Purpose |
|
||||
| --- | --- |
|
||||
| `gen-facts <in.cons> <out.lp>` | constraints → ASP facts |
|
||||
| `cycle-check-facts <in.cons> <out.lp>` | facts for the cycle pre-check (below) |
|
||||
| `gen-facts-pruned <in.cons> <brave-atoms.txt> <out.lp>` | as `gen-facts`, minus the alternatives the pre-check ruled out |
|
||||
| `parse-solution <atoms.txt> <out.json>` | answer set → placeholder-name → type JSON |
|
||||
|
||||
## The cycle pre-check
|
||||
|
||||
A constraint set can force a type placeholder to equal a type that properly *contains* it — for
|
||||
example `_r <. C<_p>` together with `_p <. _res <. _r`, which makes `_p =. C<_p>`. No finite type
|
||||
satisfies that.
|
||||
|
||||
The encoding already says so: the *Anti Cycle Conditions* (Build / Connect / Fail-Cycle) exist for
|
||||
exactly this case. But they are **integrity constraints**, and clingo evaluates those only once
|
||||
grounding has finished — while on a cyclic set grounding is precisely what does not terminate.
|
||||
Each *Subst-Param* firing nests a type one level deeper, and `maxdepth(5)` bounds the depth but
|
||||
not the branching, so the ground program grows out of reach. The symptom is a hang with
|
||||
`Rules: 0`, never an UNSAT. See [../ASP_BUGS.md](../ASP_BUGS.md), Bug 5.
|
||||
|
||||
So the check runs **before** the solve, in [`src/main/asp/cycleCheck.lp`](src/main/asp/cycleCheck.lp).
|
||||
It builds no type terms at all — only a graph over placeholder identities — and therefore grounds
|
||||
in milliseconds however deep the types in the constraint set are.
|
||||
|
||||
Two kinds of edge, and the distinction is the whole point:
|
||||
|
||||
| Edge | From | Meaning |
|
||||
| --- | --- | --- |
|
||||
| `containsEdge` | `_r <. C<_p>`, `_r =. C<_p>`, `C<_p> =. _r` | solving `_r` means solving `_p` *inside* it |
|
||||
| `flowEdge` | `_p <. _res`, `_p =. _res` | `_p`'s type flows into `_res`'s |
|
||||
|
||||
A selection of or-constraint alternatives is **cyclic** iff its graph has a cycle through at least
|
||||
one `containsEdge`. A cycle of flow edges alone (`_a <. _b <. _a`) is harmless — it just means the
|
||||
two are the same type.
|
||||
|
||||
Because a cycle usually needs a particular *combination* of alternatives from *different*
|
||||
or-constraints, the question is combinatorial, so clingo answers it — in one call:
|
||||
|
||||
```sh
|
||||
clingo --enum-mode=brave cycle_facts.lp src/main/asp/cycleCheck.lp
|
||||
```
|
||||
|
||||
- **UNSATISFIABLE** → no acyclic selection exists → the constraint set has no finite solution.
|
||||
Report it and stop, instead of hanging.
|
||||
- otherwise → the brave consequences (the *last* answer clingo prints, not the first) are exactly
|
||||
the alternatives occurring in at least one acyclic selection. Anything absent belongs to no
|
||||
solution, and `gen-facts-pruned` drops it.
|
||||
|
||||
Dropping is sound because every satisfiable selection is acyclic. Measured on a set with four
|
||||
cyclic alternatives and one acyclic one:
|
||||
|
||||
| | outcome | ground rules | time |
|
||||
| --- | --- | --- | --- |
|
||||
| unpruned | never finishes grounding | 0 | > 65 s |
|
||||
| pruned | SATISFIABLE | 265 | 4 ms |
|
||||
|
||||
`../pipeline.sh` runs this automatically as part of step 2.
|
||||
|
||||
**Caveat.** Sound only because F-bounded definitions (`class X extends C<X>`) are out of scope —
|
||||
the dissertation excludes them where it argues that restricting substitution to placeholder-free
|
||||
types preserves completeness. With an F-bounded class in the table, a type containing itself can
|
||||
be legitimate and this check would reject a satisfiable set.
|
||||
|
||||
**Limitation.** Pruning removes an alternative only when it is cyclic in *every* selection. Where
|
||||
cyclic and acyclic selections coexist and both remain reachable, grounding still explores the
|
||||
cyclic ones. The corrected `connect` rule in `unifyFinal.lp` is the in-solver backstop for what
|
||||
the pre-check cannot see.
|
||||
@@ -76,7 +76,7 @@ http://maven.apache.org/maven-v4_0_0.xsd">
|
||||
<configuration>
|
||||
<archive>
|
||||
<manifest>
|
||||
<mainClass>de.dhbwstuttgart.core.ConsoleInterface</mainClass>
|
||||
<mainClass>de.dhbwstuttgart.Main</mainClass>
|
||||
</manifest>
|
||||
</archive>
|
||||
</configuration>
|
||||
@@ -94,7 +94,7 @@ http://maven.apache.org/maven-v4_0_0.xsd">
|
||||
<configuration>
|
||||
<archive>
|
||||
<manifest>
|
||||
<mainClass>de.dhbwstuttgart.core.ConsoleInterface</mainClass>
|
||||
<mainClass>de.dhbwstuttgart.Main</mainClass>
|
||||
</manifest>
|
||||
</archive>
|
||||
<descriptorRefs>
|
||||
@@ -113,7 +113,7 @@ http://maven.apache.org/maven-v4_0_0.xsd">
|
||||
<properties>
|
||||
<maven.compiler.source>19</maven.compiler.source>
|
||||
<maven.compiler.target>19</maven.compiler.target>
|
||||
<mainClass>de.dhbwstuttgart.core.ConsoleInterface</mainClass>
|
||||
<mainClass>de.dhbwstuttgart.Main</mainClass>
|
||||
</properties>
|
||||
<distributionManagement>
|
||||
<repository>
|
||||
|
||||
@@ -6,6 +6,6 @@ tph : 'tph("_' IDENTIFIER '")';
|
||||
type : 'type("' IDENTIFIER '",' params ')';
|
||||
params : 'null' | 'params(' type (',' type)* ')';
|
||||
|
||||
IDENTIFIER: [0-9A-Za-z.]+;
|
||||
IDENTIFIER: [0-9A-Za-z.$[;][0-9A-Za-z.$[;_]*;
|
||||
NEWLINE : [\r\n]+ -> skip;
|
||||
WS: [ \t] -> skip ;
|
||||
@@ -0,0 +1,51 @@
|
||||
%==============================================================================================
|
||||
% cycleCheck.lp - find or-constraint alternatives that can never be part of a solution because
|
||||
% they force a type placeholder to equal a type properly containing itself.
|
||||
%
|
||||
% Run BEFORE the real solve, over facts from `gen-facts --cycle-check`:
|
||||
%
|
||||
% clingo --enum-mode=brave cycle-facts.lp cycleCheck.lp
|
||||
%
|
||||
% Brave enumeration returns the union of all answer sets, so the reported chosen/2 atoms are
|
||||
% exactly the alternatives that appear in at least one ACYCLIC selection. Anything absent from
|
||||
% that set is in no solution and can be dropped from the constraint set before solving.
|
||||
% UNSATISFIABLE means no acyclic selection exists at all - the constraint set has no finite
|
||||
% solution, and saying so here takes milliseconds.
|
||||
%
|
||||
% Why this is a separate program: the Anti Cycle Conditions in unifyFinal.lp express the same
|
||||
% idea, but they are integrity constraints, and clingo evaluates those only once grounding has
|
||||
% finished. On a cyclic set grounding never finishes (ASP_BUGS.md, Bug 5), so they never run.
|
||||
% This program builds no type terms at all - only placeholder identities - so it grounds
|
||||
% instantly no matter how deep the types in the constraint set are.
|
||||
%
|
||||
% CAVEAT: sound only because F-bounded definitions (class X extends C<X>) are out of scope. The
|
||||
% dissertation excludes them explicitly where it argues that restricting substitution to
|
||||
% placeholder-free types preserves completeness. With an F-bounded class in the table, a type
|
||||
% that contains itself can be legitimate and this check would reject a satisfiable set.
|
||||
%==============================================================================================
|
||||
|
||||
% --- Input, emitted by ASPGenerator.generateCycleCheckFacts ------------------------------------
|
||||
% alt(O, A). or-constraint O has an alternative A
|
||||
% containsEdge(O, A, P, Q). in alternative (O,A): P's own type must contain Q's
|
||||
% e.g. "_r <. C1<_p1>" - solving _r means solving _p1 inside it
|
||||
% flowEdge(O, A, P, Q). in alternative (O,A): P's type flows into Q's ("_p <. _res")
|
||||
%
|
||||
% A constraint that is not part of any or-constraint is emitted as an or-constraint with a
|
||||
% single alternative, so it needs no special case: its edges are always present.
|
||||
|
||||
% Exactly one alternative per or-constraint - the same choice the real encoding makes.
|
||||
{ chosen(O,A) : alt(O,A) } == 1 :- alt(O,_).
|
||||
|
||||
contains(P,Q) :- containsEdge(O,A,P,Q), chosen(O,A).
|
||||
edge(P,Q) :- contains(P,Q).
|
||||
edge(P,Q) :- flowEdge(O,A,P,Q), chosen(O,A).
|
||||
|
||||
reach(X,Y) :- edge(X,Y).
|
||||
reach(X,Z) :- reach(X,Y), edge(Y,Z).
|
||||
|
||||
% A cycle is only fatal if it passes through at least one containment edge: that is what forces
|
||||
% a placeholder to sit strictly inside its own type. A cycle of flow edges alone
|
||||
% ("_a <. _b, _b <. _a") is harmless - it just means the two are the same type.
|
||||
:- contains(X,Y), reach(Y,X).
|
||||
|
||||
#show chosen/2.
|
||||
@@ -0,0 +1,29 @@
|
||||
% Base subtype/2 facts for a small, common subset of java.lang.
|
||||
%
|
||||
% unifyDiss.lp's reflexive/transitive rules (subtype(B,B), subtype(A,A), subtype(A,C) :-
|
||||
% subtype(A,B), subtype(B,C)) only propagate subtype/2 facts that already exist - they never
|
||||
% originate one. ASPGenerator only emits subtype facts for user-defined `extends` relations
|
||||
% found in the .cons input (see ConstraintSet.g4's extendsRelation rule), not for built-in JDK
|
||||
% types. Without *some* subtype/2 base facts, any "concreteType <. placeholder" constraint (a
|
||||
% concrete type flowing in as a lower bound) is unsatisfiable: unifyDiss.lp's "super" choice rule
|
||||
% (line 88, "{ equalcons(tph(A), type(D, DP)) : subtype(type(C, CP), type(D, DP)) } == 1") must
|
||||
% pick exactly one candidate supertype D for the placeholder, and with zero subtype facts that
|
||||
% choice set is always empty.
|
||||
%
|
||||
% This is NOT a reflection of the full JDK class hierarchy - just the boxed numeric types, their
|
||||
% common ancestor Number, and Object/Boolean/Character/String - enough to make ordinary literals,
|
||||
% operators (`+`, comparisons, ...), and string concatenation resolvable. Extend as needed for
|
||||
% other library types your input code touches; a fuller version of this would enumerate the real
|
||||
% classpath (e.g. via reflection) rather than being hand-written.
|
||||
|
||||
subtype(type("java.lang.Byte",null), type("java.lang.Number",null)).
|
||||
subtype(type("java.lang.Short",null), type("java.lang.Number",null)).
|
||||
subtype(type("java.lang.Integer",null), type("java.lang.Number",null)).
|
||||
subtype(type("java.lang.Long",null), type("java.lang.Number",null)).
|
||||
subtype(type("java.lang.Float",null), type("java.lang.Number",null)).
|
||||
subtype(type("java.lang.Double",null), type("java.lang.Number",null)).
|
||||
|
||||
subtype(type("java.lang.Number",null), type("java.lang.Object",null)).
|
||||
subtype(type("java.lang.Boolean",null), type("java.lang.Object",null)).
|
||||
subtype(type("java.lang.Character",null), type("java.lang.Object",null)).
|
||||
subtype(type("java.lang.String",null), type("java.lang.Object",null)).
|
||||
@@ -0,0 +1 @@
|
||||
#show sigma/2.
|
||||
@@ -100,6 +100,42 @@ equalcons(tph(A), type(C, CP)) ; nothingFor(tph(A), type(C, CP)) :- subcons(tph(
|
||||
%Solution-Requirement:
|
||||
:- nothingFor(tph(A), _), not equalcons(tph(A), _).
|
||||
|
||||
% Fail-Subtype:
|
||||
% G1 <. G2, G1 </: G2 ==> fail (G1, G2 ground, i.e. free of type placeholders)
|
||||
% Once Solution-Gen has assigned a type to a placeholder, subst-L/subst-R rewrite every
|
||||
% constraint mentioning it into one over the substituted types, so a wrong assignment surfaces as
|
||||
% a subcons/2 between two ground types: solving `_a <. java.lang.Boolean` with java.lang.Object
|
||||
% derives `subcons(type("java.lang.Object",null), type("java.lang.Boolean",null))`. A ground
|
||||
% constraint is decidable - it holds iff the class hierarchy says so - and nothing checked it so
|
||||
% far, which is what let a placeholder be solved with a type violating its own upper bounds.
|
||||
% The restriction to ground terms is required for soundness, not an optimisation: a constraint
|
||||
% still containing a placeholder, such as Box<_a> <. Box<_b>, cannot be validated before those
|
||||
% placeholders are substituted.
|
||||
:- subcons(S, T), groundType(S), groundType(T), not subtype(S, T).
|
||||
|
||||
% groundType(T): type term T occurs in the constraint set and contains no type placeholder.
|
||||
groundType(T) :- typeTerm(T), not containsTph(T).
|
||||
|
||||
containsTph(tph(A)) :- typeTerm(tph(A)).
|
||||
containsTph(type(C, params(P1))) :- typeTerm(type(C, params(P1))), containsTph(P1).
|
||||
containsTph(type(C, params(P1, P2))) :- typeTerm(type(C, params(P1, P2))), containsTph(P1).
|
||||
containsTph(type(C, params(P1, P2))) :- typeTerm(type(C, params(P1, P2))), containsTph(P2).
|
||||
containsTph(type(C, params(P1, P2, P3))) :- typeTerm(type(C, params(P1, P2, P3))), containsTph(P1).
|
||||
containsTph(type(C, params(P1, P2, P3))) :- typeTerm(type(C, params(P1, P2, P3))), containsTph(P2).
|
||||
containsTph(type(C, params(P1, P2, P3))) :- typeTerm(type(C, params(P1, P2, P3))), containsTph(P3).
|
||||
|
||||
% Every type term occurring in a constraint, including the ones nested in type parameters.
|
||||
typeTerm(S) :- subcons(S, _).
|
||||
typeTerm(T) :- subcons(_, T).
|
||||
typeTerm(S) :- equalcons(S, _).
|
||||
typeTerm(T) :- equalcons(_, T).
|
||||
typeTerm(P1) :- typeTerm(type(_, params(P1))).
|
||||
typeTerm(P1) :- typeTerm(type(_, params(P1, _))).
|
||||
typeTerm(P2) :- typeTerm(type(_, params(_, P2))).
|
||||
typeTerm(P1) :- typeTerm(type(_, params(P1, _, _))).
|
||||
typeTerm(P2) :- typeTerm(type(_, params(_, P2, _))).
|
||||
typeTerm(P3) :- typeTerm(type(_, params(_, _, P3))).
|
||||
|
||||
% S-Object
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(tph(A), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(_, tph(A)).
|
||||
|
||||
@@ -0,0 +1,426 @@
|
||||
%==============================================================================================
|
||||
% unifyFinal.lp - global type inference for Java by unification, as an Answer Set Program.
|
||||
%
|
||||
% Source: the program printed in dissertation/chapters/unifyWithASP.tex, section
|
||||
% "ASP Program + Example Input" (\label{appendix:program}), transcribed verbatim except that
|
||||
% its embedded "% TEST INPUT" constraint set and its trailing "#show sigma/2." are left out
|
||||
% (show.lp provides the latter), and one rule is added - see Fail-Equals in PART 2.
|
||||
%
|
||||
% Rule names in CAPITALS refer to the inference rules of
|
||||
% Figure "Unify Algorithm" (\label{fig:aspUnifyAlgorithm}) and
|
||||
% Figure "Subtyping" (\label{fig:aspSubtyping}).
|
||||
%
|
||||
% Notation used in the paper and mirrored here:
|
||||
% a, b type placeholders tph("_a")
|
||||
% G a *ground* type - one containing no placeholder anywhere
|
||||
% N, C<...> a class type type("java.util.List", params(...))
|
||||
% T <. T' subtype constraint subcons(T, T')
|
||||
% T =. T' equality constraint equalcons(T, T')
|
||||
% T <: T' the Java subtype relation subtype(T, T')
|
||||
% sigma(a) the computed unifier sigma(tph("_a"), type(...))
|
||||
%
|
||||
% File layout:
|
||||
% PART 1 Input: constraint set, or-constraints, extends relations, subtyping
|
||||
% PART 2 The algorithm: one section per rule of the paper
|
||||
% PART 3 Helpers: depth, groundness, placeholder occurrence
|
||||
%==============================================================================================
|
||||
|
||||
|
||||
%==============================================================================================
|
||||
% PART 1 - INPUT
|
||||
%==============================================================================================
|
||||
%
|
||||
% Everything in this part turns the facts emitted by JavaTypeUnifyASP's `gen-facts` command into
|
||||
% the two constraint predicates the algorithm works on (subcons/2, equalcons/2) plus the Java
|
||||
% subtype relation (subtype/2).
|
||||
%
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% What the input looks like
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% JavaConstraintGenerator writes a textual .cons file; `gen-facts` parses it (grammar:
|
||||
% src/main/antlr4/.../ConstraintSet.g4) and emits ASP facts. A .cons file has three kinds of line:
|
||||
%
|
||||
% Sub < Super an extends/implements edge, type arguments included
|
||||
% T <. T' a subtype constraint
|
||||
% { a, b | c, d } an or-constraint: at least one alternative, all of its parts
|
||||
%
|
||||
% Types are written `java.util.List<java.lang.Integer>` and placeholders `_Foo_3`. These become:
|
||||
%
|
||||
% type("java.util.List", params(type("java.lang.Integer", null))) a class type
|
||||
% type("java.lang.Integer", null) no type arguments
|
||||
% tph("_Foo_3") a type placeholder
|
||||
%
|
||||
% A simple constraint `_Foo_3 <. java.lang.Number` is emitted as a one-element or-constraint:
|
||||
%
|
||||
% orCons(undCons(subcons(tph("_Foo_3"), type("java.lang.Number",null)), null), null).
|
||||
%
|
||||
% so there is exactly one shape to unpack, whether or not the constraint had alternatives.
|
||||
% An or-constraint nests: orCons(<alternative>, orCons(<alternative>, ... null)), and each
|
||||
% alternative is a chain undCons(<constraint>, undCons(<constraint>, ... null)).
|
||||
%
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% Where the extends relations come from
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% They are not facts of this program; they are supplied per run, exactly like the constraint set.
|
||||
% JavaConstraintGenerator reads them off the analysed Java sources (`class C extends D`,
|
||||
% `implements E`) and off the JDK/library classes it reflects, walking up until every ancestor is
|
||||
% covered. Each edge keeps its type arguments, and ASPGenerator emits it as a *guarded rule*, not
|
||||
% a fact - realizing S-CLASS of Figure "Subtyping":
|
||||
%
|
||||
% class C<X> extends D<X>
|
||||
% ==> subtype(type("C", params(XX)), type("D", params(XX)))
|
||||
% :- subtype(type("C", params(XX))).
|
||||
%
|
||||
% Two things make the guard necessary rather than decorative:
|
||||
% - it *binds* XX. A bare fact with a free variable is not safe and clingo rejects it.
|
||||
% - it instantiates the edge lazily, only for the type arguments a given run actually mentions.
|
||||
% Note the head is subtype/2 and the body subtype/1 - different predicates, so this is not a
|
||||
% self-referential rule. subtype/1 is derived below from the constraints.
|
||||
%
|
||||
% Because the edges arrive as rules, `Matrix < java.util.Vector<java.util.Vector<java.lang.Integer>>`
|
||||
% is what lets ADAPT resolve `Matrix <. java.util.Vector<X>` to X = Vector<Integer>. An *erased*
|
||||
% edge would give a subtype/2 fact that no parameterized occurrence can ever match.
|
||||
%==============================================================================================
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% Or-constraints: choose exactly one alternative, then take all of its conjuncts.
|
||||
% This is the ASP encoding of the constraint set's disjunctive structure; the paper treats a
|
||||
% constraint set as already-chosen and does not name a rule for it.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% One alternative left in the chain: it is forced.
|
||||
undCons(A,B) :- orCons(undCons(A,B), null).
|
||||
% More than one: pick this alternative, or move on to the rest. Exactly one is chosen.
|
||||
{ undCons(A,B); orCons(C,D) } == 1 :- orCons(undCons(A,B), orCons(C,D)).
|
||||
|
||||
% Unpack the chosen alternative's conjunct chain into plain constraints.
|
||||
subcons(A,B) :- undCons(subcons(A,B), _).
|
||||
equalcons(A,B) :- undCons(equalcons(A,B), _).
|
||||
undCons(C,D) :- undCons(_, undCons(C,D)).
|
||||
undCons(B,C) :- undCons(A, undCons(B, C)).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% Subtyping - Figure "Subtyping" (\label{fig:aspSubtyping}).
|
||||
% S-CLASS arrives as the generated rules described above; the closure is here.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% Java: every reference type is a subtype of Object. Stated directly so that the last hop of any
|
||||
% chain is always one step from a type the constraints actually mention.
|
||||
subtype(A, type("java.lang.Object", null)):- subtype(A).
|
||||
|
||||
% S-REFL: T <: T
|
||||
subtype(A, A) :- subtype(A).
|
||||
subtype(A, A) :- subtype(A, B).
|
||||
% S-TRANS: T1 <: T2, T2 <: T3 ==> T1 <: T3
|
||||
subtype(B) :- subtype(A, B).
|
||||
subtype(A, C) :- subtype(A, B), subtype(B, C).
|
||||
|
||||
% Erasure-level subtyping: the same relation with type arguments dropped. Used by Fail-Subtype
|
||||
% below, which is the one place the appendix compares class names only.
|
||||
namedSubtype(A,B) :- subtype(type(A, AP), type(B, BP)).
|
||||
|
||||
% subtype/1 - "this type occurs in the constraint set", the guard that activates the generated
|
||||
% S-CLASS rules. Seeded from both sides of every subtype constraint.
|
||||
subtype(type(A, P)) :- subcons(_, type(A, P)).
|
||||
subtype(type(A, P)) :- subcons(type(A, P), _).
|
||||
|
||||
|
||||
%==============================================================================================
|
||||
% PART 2 - THE ALGORITHM
|
||||
% One section per inference rule of Figure "Unify Algorithm" (\label{fig:aspUnifyAlgorithm}).
|
||||
%==============================================================================================
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% SUBST - the substitution relation the four Subst-* rules below are phrased against.
|
||||
%
|
||||
% The paper writes every Subst rule with a *ground* type G on the right: `a =. G`. That
|
||||
% restriction is what keeps grounding finite - substituting a type that still contains a
|
||||
% placeholder can feed a placeholder's own solution back into itself and build ever-deeper terms
|
||||
% (see "Grounding bottleneck" in the chapter). It is enforced here by deriving subst from
|
||||
% sigma/2 rather than from equalcons/2: SOLUTION below only produces sigma for a type that
|
||||
% contains no placeholder.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
subst(tph(A), type(N,P)) :- sigma(tph(A), type(N, P)).
|
||||
|
||||
% SUBST-L: a =. G, a <. T ==> G <. T
|
||||
subcons(B,C) :- subst(A, B), subcons(A, C).
|
||||
% SUBST-R: a =. G, T <. a ==> T <. G
|
||||
subcons(C,B) :- subst(A, B), subcons(C, A).
|
||||
% SUBST-EQUAL: a =. G, a =. T ==> T =. G
|
||||
equalcons(B,C) :- subst(A, B), equalcons(A, C).
|
||||
|
||||
% SWAP: T1 =. T2 ==> T2 =. T1
|
||||
equalcons(A,B) :- equalcons(B,A).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% S-OBJECT: a <. Object for every placeholder a
|
||||
%
|
||||
% One rule per position a placeholder can occupy in a constraint - either side of <. and =., and
|
||||
% nested inside a type argument at any of the three supported arities. Giving every placeholder
|
||||
% at least one upper bound is what makes SOLUTION-GEN able to answer for it at all.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(tph(A), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(_, tph(A)).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(_, type(_, params(tph(A)))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(_, type(_, params(tph(A), _))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(_, type(_, params(_, tph(A)))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(_, type(_, params(tph(A), _, _))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(_, type(_, params(_, tph(A), _))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(_, type(_, params(_, _, tph(A)))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(type(_, params(tph(A))), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(type(_, params(tph(A), _)), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(type(_, params(_, tph(A))), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(type(_, params(tph(A), _, _)), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(type(_, params(tph(A), _, _)), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(type(_, params(_, tph(A), _)), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- subcons(type(_, params(_, _, tph(A))), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(tph(A), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(_, tph(A)).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(_, type(_, params(tph(A)))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(_, type(_, params(tph(A), _))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(_, type(_, params(_, tph(A)))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(_, type(_, params(tph(A), _, _))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(_, type(_, params(_, tph(A), _))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(_, type(_, params(_, _, tph(A)))).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(type(_, params(tph(A))), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(type(_, params(tph(A), _)), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(type(_, params(_, tph(A))), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(type(_, params(tph(A), _, _)), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(type(_, params(tph(A), _, _)), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(type(_, params(_, tph(A), _)), _).
|
||||
subcons(tph(A), type("java.lang.Object", null)) :- equalcons(type(_, params(_, _, tph(A))), _).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% SUBST-PARAM: a =. G, T =. C<P1..a..Pn> ==> T =. C<P1..G..Pn>
|
||||
% SUBST-PARAM-RIGHT: a =. G, b <. C<T1..a..Tn> ==> b <. C<P1..G..Pn>
|
||||
%
|
||||
% Substitution *inside* a type argument, one rule per parameter position (arities one to three -
|
||||
% see "Fixed Arity for Parameter Lists"). SUBST-PARAM-LEFT of the figure, which rewrites the left
|
||||
% operand of a <., has no counterpart here.
|
||||
%
|
||||
% Each firing makes a type one level deeper, so a cyclic assignment such as a =. List<a> would
|
||||
% nest without bound. FAIL-CYCLE below rules such cycles out, but clingo grounds before it
|
||||
% evaluates any integrity constraint, so the grounder would diverge first. The maxdepth guard is
|
||||
% what keeps grounding finite; depth/2 is defined in PART 3.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
maxdepth(5).
|
||||
|
||||
equalcons(A, type(C, params(T2))) :- equalcons(A, type(C, params(T))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
equalcons(A, type(C, params(T2, P2))) :- equalcons(A, type(C, params(T, P2))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
equalcons(A, type(C, params(P1, T2))) :- equalcons(A, type(C, params(P1, T))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
equalcons(A, type(C, params(T2, P2, P3))) :- equalcons(A, type(C, params(T, P2, P3))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
equalcons(A, type(C, params(P1, T2, P3))) :- equalcons(A, type(C, params(P1, T, P3))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
equalcons(A, type(C, params( P1, P2, T2))) :- equalcons(A, type(C, params(P1, P2, T))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
|
||||
subcons(A, type(C, params(T2))) :- subcons(A, type(C, params(T))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
subcons(A, type(C, params(T2, P2))) :- subcons(A, type(C, params(T, P2))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
subcons(A, type(C, params(P1, T2))) :- subcons(A, type(C, params(P1, T))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
subcons(A, type(C, params(T2, P2, P3))) :- subcons(A, type(C, params(T, P2, P3))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
subcons(A, type(C, params(P1, T2, P3))) :- subcons(A, type(C, params(P1, T, P3))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
subcons(A, type(C, params( P1, P2, T2))) :- subcons(A, type(C, params(P1, P2, T))), subst(T, T2), depth(T2, D), maxdepth(Dmax), D < Dmax.
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% ADAPT: N <. C<P1..Pn>, N <: C<P'1..P'n> ==> P1 =. P'1, ..., Pn =. P'n
|
||||
%
|
||||
% A class type constrained below a parameterized type must agree with that type argument for
|
||||
% argument, read off its position in the hierarchy. This is where an extends relation's type
|
||||
% arguments do their work: `Matrix <. Vector<X>` together with
|
||||
% `Matrix <: Vector<Vector<Integer>>` forces X = Vector<Integer>. The parameter equalities
|
||||
% themselves are extracted by REDUCE.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
equalcons(type(D,P3), type(D,P2)) :- subcons(type(C,P), type(D, P2)), subtype(type(C, P), type(D, P3)).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% REDUCE: C<P1..Pn> =. C<P'1..P'n> ==> Pi =. P'i
|
||||
% Same class on both sides: equate the arguments pairwise. One rule per position per arity.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
equalcons(P1, PP1) :- equalcons(type(C, params(P1)), type(C, params(PP1))).
|
||||
equalcons(P1, PP1) :- equalcons(type(C, params(P1, P2)), type(C, params(PP1, PP2))).
|
||||
equalcons(P2, PP2) :- equalcons(type(C, params(P1, P2)), type(C, params(PP1, PP2))).
|
||||
equalcons(P1, PP1) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))).
|
||||
equalcons(P2, PP2) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))).
|
||||
equalcons(P3, PP3) :- equalcons(type(C, params(P1, P2, P3)), type(C, params(PP1, PP2, PP3))).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% SUPER: N <. a, N <: N1..Nn ==> for one m: a =. Nm
|
||||
%
|
||||
% A placeholder with a class type as a *lower* bound must be one of that type's supertypes - the
|
||||
% solver picks which. Written as a cardinality constraint over the candidates, the ASP form of
|
||||
% the figure's "for one m" conclusion. If no subtype/2 fact matches N, the candidate set is empty
|
||||
% and "== 1" makes the program unsatisfiable - which is why the extends relations must cover
|
||||
% every type that appears as a lower bound.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
{ equalcons(tph(A), type(D, DP)): subtype(type(C, CP), type(D, DP)) } == 1 :- subcons(type(C, CP), tph(A)).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% SOLUTION-GEN: a <. N, ... ==> for one m: a =. Nm
|
||||
% Offer each upper bound of a placeholder as a candidate assignment. A choice rule rather than a
|
||||
% cardinality one: the solver may take it or leave it here, and SOLUTION-REQUIREMENT below is
|
||||
% what insists that something is eventually chosen.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
{ equalcons(tph(A), type(T,P)) } :- subcons(tph(A), type(T,P)).
|
||||
|
||||
% SOLUTION-REQUIREMENT: every placeholder that occurs in a constraint must end up with a unifier.
|
||||
% Commented out in the figure - see the surrounding text, which discusses this formulation.
|
||||
:- subcons(tph(A), _), not sigma(tph(A), _).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% SOLUTION: a =. G ==> sigma(a) = G
|
||||
%
|
||||
% Only for a *ground* G: "not tphs(_, P)" rejects a type whose arguments still contain a
|
||||
% placeholder (tphs/2 is defined in PART 3). This single guard is also what restricts SUBST, and
|
||||
% with it every Subst-* rule, to placeholder-free types.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
tphs( P ) :- equalcons(tph(A), type(C, P)).
|
||||
sigma(tph(A), type(C,P)) :- equalcons(tph(A), type(C, P)), not tphs(_, P).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% FAIL-SUBTYPE: G1 <. G2, G1 not<: G2 ==> fail
|
||||
%
|
||||
% Compares class *names* (namedSubtype), where the figure compares whole types. That reads like a
|
||||
% gap but is not one in practice, because ADAPT covers the arguments: given
|
||||
% Vector<String> <. Vector<Integer>, ADAPT plus S-REFL derive
|
||||
% Vector<String> =. Vector<Integer>, REDUCE splits that into String =. Integer, and FAIL-EQUALS
|
||||
% below rejects it on the differing head names. Verified - that constraint set is UNSATISFIABLE
|
||||
% with or without the added rule. No counterexample to the name-only form has been constructed;
|
||||
% if one exists it needs a ground pair that ADAPT cannot fire on.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
:- subcons(type(C, CP), type(D, DP)), not namedSubtype(C, D).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% FAIL-EQUALS: G1 =. G2, G1 != G2 ==> fail
|
||||
%
|
||||
% The appendix implements this by comparing head class names only:
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
:- equalcons(type(C, CP), type(D, DP)), C != D.
|
||||
|
||||
% THIS RULE IS THE ONE ADDITION TO THE APPENDIX PROGRAM: on ground terms the whole type can be
|
||||
% compared, type arguments included, which is what the figure's rule actually says.
|
||||
%
|
||||
% Where it earns its keep is *arity*, not argument values. Two types with the same class name but
|
||||
% different parameter counts are paired by neither rule above: the name-only rule sees C == C, and
|
||||
% REDUCE has no rule matching null against params(...), or params(P1) against params(P1,P2). So
|
||||
% java.util.Vector =. java.util.Vector<java.lang.Integer>
|
||||
% is accepted by the appendix program and rejected here - see ../../../../test_input3/arity-mismatch.cons.
|
||||
% This is exactly the raw-versus-parameterized confusion that arises if extends relations are ever
|
||||
% emitted in both erased and parameterized form.
|
||||
%
|
||||
% Argument *values* are already handled without this rule, via ADAPT + REDUCE + the name-only
|
||||
% FAIL-EQUALS - see the note on FAIL-SUBTYPE above.
|
||||
%
|
||||
% The restriction to ground terms is required for soundness, not an optimisation - Box<a> =. Box<b>
|
||||
% is perfectly satisfiable and must not be rejected before a and b have been substituted.
|
||||
% groundType/1 is defined in PART 3.
|
||||
:- equalcons(S, T), groundType(S), groundType(T), S != T.
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% Anti Cycle Conditions - BUILD, CONNECT, FAIL-CYCLE.
|
||||
%
|
||||
% BUILD: a =. C<..b..> ==> a -> b
|
||||
% CONNECT: a -> b, b -> c ==> a -> c
|
||||
% FAIL-CYCLE: a -> a ==> fail
|
||||
%
|
||||
% An assignment whose right-hand side contains the placeholder being assigned has no finite
|
||||
% solution. Note these are integrity constraints, so they are only evaluated *after* grounding -
|
||||
% the maxdepth guard on SUBST-PARAM is what gets the program that far.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
connected(A,B) :- equalcons(tph(A), type(_,params(tph(B)))).
|
||||
connected(A,B) :- equalcons(tph(A), type(_,params(tph(B),_))).
|
||||
connected(A,B) :- equalcons(tph(A), type(_,params(_,tph(B)))).
|
||||
connected(A,B) :- equalcons(tph(A), type(_,params(tph(B),_,_))).
|
||||
connected(A,B) :- equalcons(tph(A), type(_,params(_,tph(B),_))).
|
||||
connected(A,B) :- equalcons(tph(A), type(_,params(_,_,tph(B)))).
|
||||
|
||||
% CONNECT. The appendix prints this as `connected(A,C) :- connected(A,B), connected(A,C).`, whose
|
||||
% second body literal repeats the head instead of chaining through B - as printed it derives
|
||||
% nothing, leaving FAIL-CYCLE able to catch only *direct* self-reference (a =. C<..a..>) and not
|
||||
% a -> b -> a. Corrected here to the figure's rule, `a -> b, b -> c ==> a -> c`.
|
||||
%
|
||||
% Note this is a correctness backstop only. FAIL-CYCLE is an integrity constraint, so it runs
|
||||
% after grounding - and on a cyclic constraint set grounding is exactly what does not terminate.
|
||||
% cycleCheck.lp is what catches those, before the solve.
|
||||
connected(A,C) :- connected(A,B), connected(B,C).
|
||||
|
||||
% FAIL-CYCLE.
|
||||
:- connected(A,A).
|
||||
|
||||
|
||||
%==============================================================================================
|
||||
% PART 3 - HELPERS
|
||||
% No counterpart in the paper; these compute the side conditions its rules are stated with.
|
||||
%==============================================================================================
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% depth/1 and depth/2 - the nesting depth of a type, used only by SUBST-PARAM's maxdepth guard.
|
||||
%
|
||||
% depth/1 marks a term as one whose depth is worth computing; it is seeded from the substituted
|
||||
% types and pushed down into type arguments, so the measurement is confined to terms that can
|
||||
% actually reach a Subst-Param rule. depth/2 then reports a depth for each such term: 0 for a
|
||||
% type with no arguments, and for a parameterized type the sum of its arguments' depths plus one.
|
||||
% (A sum rather than a maximum, so a wide type counts as deeper than a narrow one of the same
|
||||
% nesting - a coarser bound than the name "depth" suggests, but a finite one, which is the point.)
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
depth(T2) :- subst(T, T2).
|
||||
depth(T2) :- subst(_, T2).
|
||||
depth(T) :- depth(type(A, params(T))).
|
||||
depth(T) :- depth(type(A, params(T, T1))).
|
||||
depth(T1) :- depth(type(A, params(T, T1))).
|
||||
depth(T) :- depth(type(A, params(T, T1, T2))).
|
||||
depth(T1) :- depth(type(A, params(T, T1, T2))).
|
||||
depth(T2) :- depth(type(A, params(T, T1, T2))).
|
||||
|
||||
depth(type(A, null), 0) :- depth(type(A, null)).
|
||||
depth(type(A, params(T)), D+1) :- depth(type(A, params(T))), depth(T, D).
|
||||
depth(type(A, params(T, T1)), D+D1+1) :- depth(type(A, params(T, T1))), depth(T, D), depth(T1, D1).
|
||||
depth(type(A, params(T, T1, T2)), D+D1+D2+1) :- depth(type(A, params(T, T1, T2))), depth(T, D), depth(T1, D1), depth(T2, D2).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% groundType/1 - the paper's G: a type term occurring in the constraint set that contains no
|
||||
% placeholder at any depth. Used by the added Fail-Equals rule.
|
||||
%
|
||||
% Defined positively - built up from argument-free types rather than as
|
||||
% "typeTerm(T), not containsTph(T)" - so the grounder can evaluate it bottom-up. Phrased with
|
||||
% negation it would sit in a negative cycle through subcons/2 and the grounder would have to
|
||||
% assume it might hold for every term, which makes it useless as a guard.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
groundType(type(C, null)) :- typeTerm(type(C, null)).
|
||||
groundType(type(C, params(P1))) :- typeTerm(type(C, params(P1))), groundType(P1).
|
||||
groundType(type(C, params(P1, P2))) :- typeTerm(type(C, params(P1, P2))), groundType(P1), groundType(P2).
|
||||
groundType(type(C, params(P1, P2, P3))) :- typeTerm(type(C, params(P1, P2, P3))), groundType(P1), groundType(P2), groundType(P3).
|
||||
|
||||
% typeTerm/1 - every type term occurring anywhere in a constraint, including nested arguments.
|
||||
typeTerm(S) :- subcons(S, _).
|
||||
typeTerm(T) :- subcons(_, T).
|
||||
typeTerm(S) :- equalcons(S, _).
|
||||
typeTerm(T) :- equalcons(_, T).
|
||||
typeTerm(P1) :- typeTerm(type(_, params(P1))).
|
||||
typeTerm(P1) :- typeTerm(type(_, params(P1, _))).
|
||||
typeTerm(P2) :- typeTerm(type(_, params(_, P2))).
|
||||
typeTerm(P1) :- typeTerm(type(_, params(P1, _, _))).
|
||||
typeTerm(P2) :- typeTerm(type(_, params(_, P2, _))).
|
||||
typeTerm(P3) :- typeTerm(type(_, params(_, _, P3))).
|
||||
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
% tphs/1 and tphs/2 - "this parameter list contains a placeholder", the side condition SOLUTION
|
||||
% uses to accept only ground types. tphs(P) marks a parameter list under inspection; tphs(A, P)
|
||||
% says placeholder A occurs somewhere in P. One rule per position per arity, recursing through
|
||||
% nested class types.
|
||||
% ---------------------------------------------------------------------------------------------
|
||||
tphs(tph(P), params(tph(P))) :- tphs( params(tph(P))).
|
||||
tphs(P) :- tphs( params(type(C, P))).
|
||||
tphs(tph(A), params(type(C, P))) :- tphs( params(type(C, P))), tphs(tph(A), P).
|
||||
|
||||
tphs(tph(P), params(X, tph(P))) :- tphs( params(X, tph(P))).
|
||||
tphs(tph(P), params(tph(P), X)) :- tphs( params(tph(P), X)).
|
||||
tphs(P) :- tphs( params(X, type(C, P))).
|
||||
tphs(P) :- tphs( params(type(C, P), X)).
|
||||
tphs(tph(A), params(X, type(C, P))) :- tphs( params(X, type(C, P))), tphs(tph(A), P).
|
||||
tphs(tph(A), params(type(C, P), X)) :- tphs( params(type(C, P), X)), tphs(tph(A), P).
|
||||
|
||||
tphs(tph(P), params(tph(P), X, Y)) :- tphs( params(tph(P), X, Y)).
|
||||
tphs(tph(P), params(X, tph(P), Y)) :- tphs( params(X, tph(P), Y)).
|
||||
tphs(tph(P), params(X,Y,tph(P))) :- tphs( params(X, Y, tph(P))).
|
||||
tphs(P) :- tphs( params(type(C, P), X, Y)).
|
||||
tphs(P) :- tphs( params(X, type(C, P),Y)).
|
||||
tphs(P) :- tphs( params(X,Y,type(C, P))).
|
||||
tphs(tph(A), params(type(C, P), X, Y)) :- tphs( params(type(C, P), X, Y)), tphs(tph(A), P).
|
||||
tphs(tph(A), params(X, type(C, P), Y)) :- tphs( params(X, type(C, P), Y)), tphs(tph(A), P).
|
||||
tphs(tph(A), params(X, Y, type(C, P))) :- tphs( params(X, Y, type(C, P))), tphs(tph(A), P).
|
||||
@@ -0,0 +1,234 @@
|
||||
package de.dhbwstuttgart;
|
||||
|
||||
import de.dhbwstuttgart.input.ConstraintParser;
|
||||
import de.dhbwstuttgart.output.SolutionParser;
|
||||
import de.dhbwstuttgart.sat.asp.ASPGenerator;
|
||||
|
||||
import java.io.IOException;
|
||||
import java.nio.file.Files;
|
||||
import java.nio.file.Path;
|
||||
import de.dhbwstuttgart.sat.asp.Pair;
|
||||
|
||||
import java.util.ArrayList;
|
||||
import java.util.LinkedHashSet;
|
||||
import java.util.List;
|
||||
import java.util.Map;
|
||||
import java.util.Set;
|
||||
import java.util.regex.Matcher;
|
||||
import java.util.regex.Pattern;
|
||||
|
||||
/**
|
||||
* Small CLI over this project's two translation entry points, so a shell pipeline can call into
|
||||
* it without embedding a JVM: turning a {@code .cons} constraint file into ASP facts for clingo,
|
||||
* and turning clingo's answer-set text back into a placeholder-name-to-type JSON map.
|
||||
*/
|
||||
public class Main {
|
||||
|
||||
public static void main(String[] args) {
|
||||
if (args.length < 1) {
|
||||
printUsage();
|
||||
System.exit(1);
|
||||
}
|
||||
|
||||
try {
|
||||
switch (args[0]) {
|
||||
case "gen-facts" -> {
|
||||
if (args.length != 3) {
|
||||
System.err.println("gen-facts requires exactly 2 arguments: <constraints.cons> <out-facts.lp>");
|
||||
System.exit(1);
|
||||
}
|
||||
genFacts(args[1], args[2]);
|
||||
}
|
||||
case "cycle-check-facts" -> {
|
||||
if (args.length != 3) {
|
||||
System.err.println("cycle-check-facts requires exactly 2 arguments: <constraints.cons> <out-facts.lp>");
|
||||
System.exit(1);
|
||||
}
|
||||
cycleCheckFacts(args[1], args[2]);
|
||||
}
|
||||
case "gen-facts-pruned" -> {
|
||||
if (args.length != 4) {
|
||||
System.err.println("gen-facts-pruned requires exactly 3 arguments: "
|
||||
+ "<constraints.cons> <brave-atoms.txt> <out-facts.lp>");
|
||||
System.exit(1);
|
||||
}
|
||||
genFactsPruned(args[1], args[2], args[3]);
|
||||
}
|
||||
case "parse-solution" -> {
|
||||
if (args.length != 3) {
|
||||
System.err.println("parse-solution requires exactly 2 arguments: <clingo-atoms.txt> <out-solution.json>");
|
||||
System.exit(1);
|
||||
}
|
||||
parseSolution(args[1], args[2]);
|
||||
}
|
||||
default -> {
|
||||
System.err.println("Unknown subcommand: " + args[0]);
|
||||
printUsage();
|
||||
System.exit(1);
|
||||
}
|
||||
}
|
||||
} catch (IOException e) {
|
||||
System.err.println("I/O error: " + e.getMessage());
|
||||
System.exit(1);
|
||||
}
|
||||
}
|
||||
|
||||
private static void genFacts(String consFile, String outFactsFile) throws IOException {
|
||||
String cons = Files.readString(Path.of(consFile));
|
||||
// Both ANTLR grammars require at least one entry ("(x)+"), so a blank/empty input -
|
||||
// e.g. a Java file with no constraint-generating constructs yet supported by
|
||||
// JavaConstraintGenerator - would otherwise crash instead of producing an empty result.
|
||||
if (cons.isBlank()) {
|
||||
Files.writeString(Path.of(outFactsFile), "");
|
||||
return;
|
||||
}
|
||||
var orCons = ConstraintParser.parse(cons);
|
||||
String asp = ASPGenerator.generateASP(orCons);
|
||||
// extendsRelation entries (e.g. "Matrix < java.util.Vector", from JavaConstraintGenerator
|
||||
// gathering the analysed classes' own extends/implements clauses) are a separate grammar
|
||||
// production parsed separately from the constraints/or-constraints ConstraintParser.parse
|
||||
// already handled above - both read the same .cons text, just looking at different parts
|
||||
// of its parse tree.
|
||||
var extendsRelations = ConstraintParser.parseExtendsRelations(cons);
|
||||
String extendsAsp = ASPGenerator.generateExtendsRelations(extendsRelations);
|
||||
Files.writeString(Path.of(outFactsFile), asp + extendsAsp);
|
||||
}
|
||||
|
||||
/**
|
||||
* Writes the facts {@code cycleCheck.lp} consumes - see that file's header. Run before the
|
||||
* real solve to find or-constraint alternatives that force a placeholder to equal a type
|
||||
* containing itself; those can never be part of a solution and make clingo's grounder
|
||||
* diverge if left in (see ../../ASP_BUGS.md, Bug 5).
|
||||
*/
|
||||
private static void cycleCheckFacts(String consFile, String outFactsFile) throws IOException {
|
||||
String cons = Files.readString(Path.of(consFile));
|
||||
if (cons.isBlank()) {
|
||||
Files.writeString(Path.of(outFactsFile), "");
|
||||
return;
|
||||
}
|
||||
Files.writeString(Path.of(outFactsFile),
|
||||
ASPGenerator.generateCycleCheckFacts(ConstraintParser.parse(cons)));
|
||||
}
|
||||
|
||||
/**
|
||||
* Like {@code gen-facts}, but keeps only the or-constraint alternatives named in
|
||||
* {@code braveAtomsFile} - clingo's brave consequences from the {@code cycleCheck.lp} run,
|
||||
* i.e. every alternative that occurs in at least one acyclic selection. An alternative
|
||||
* outside that set belongs to no solution.
|
||||
*
|
||||
* <p>An or-constraint that loses every alternative would be unsatisfiable, but that cannot
|
||||
* happen here: were it so, the cycle check itself would have been UNSATISFIABLE and the
|
||||
* caller would have stopped before reaching this point.
|
||||
*/
|
||||
private static void genFactsPruned(String consFile, String braveAtomsFile, String outFactsFile)
|
||||
throws IOException {
|
||||
String cons = Files.readString(Path.of(consFile));
|
||||
if (cons.isBlank()) {
|
||||
Files.writeString(Path.of(outFactsFile), "");
|
||||
return;
|
||||
}
|
||||
Set<String> keep = parseChosenAtoms(Files.readString(Path.of(braveAtomsFile)));
|
||||
var orCons = ConstraintParser.parse(cons);
|
||||
var pruned = new ArrayList<List<Set<Pair>>>(orCons.size());
|
||||
for (int o = 0; o < orCons.size(); o++) {
|
||||
var alternatives = orCons.get(o);
|
||||
var surviving = new ArrayList<Set<Pair>>(alternatives.size());
|
||||
for (int a = 0; a < alternatives.size(); a++) {
|
||||
if (keep.contains(o + "," + a)) surviving.add(alternatives.get(a));
|
||||
}
|
||||
// Defensive: an empty list would render as a malformed orCons(...) term. If the
|
||||
// brave-consequence file was empty or unreadable, fall back to the full set rather
|
||||
// than emit something the grammar cannot express.
|
||||
pruned.add(surviving.isEmpty() ? alternatives : surviving);
|
||||
}
|
||||
String asp = ASPGenerator.generateASP(pruned);
|
||||
var extendsRelations = ConstraintParser.parseExtendsRelations(cons);
|
||||
Files.writeString(Path.of(outFactsFile), asp + ASPGenerator.generateExtendsRelations(extendsRelations));
|
||||
}
|
||||
|
||||
/** Extracts "O,A" keys from clingo's {@code chosen(O,A)} brave-consequence atoms. */
|
||||
private static Set<String> parseChosenAtoms(String atoms) {
|
||||
Set<String> keys = new LinkedHashSet<>();
|
||||
Matcher m = Pattern.compile("chosen\\((\\d+),(\\d+)\\)").matcher(atoms);
|
||||
while (m.find()) keys.add(m.group(1) + "," + m.group(2));
|
||||
return keys;
|
||||
}
|
||||
|
||||
private static void parseSolution(String atomsFile, String outSolutionFile) throws IOException {
|
||||
String atoms = Files.readString(Path.of(atomsFile));
|
||||
if (atoms.isBlank()) {
|
||||
Files.writeString(Path.of(outSolutionFile), "{\n}\n");
|
||||
return;
|
||||
}
|
||||
Map<String, String> solution = SolutionParser.parse(atoms);
|
||||
Files.writeString(Path.of(outSolutionFile), toJson(solution));
|
||||
}
|
||||
|
||||
/**
|
||||
* {@link SolutionParser#parse} strips the leading underscore off every placeholder name
|
||||
* (its grammar folds it into the literal that precedes the identifier token), but every
|
||||
* other artifact in this pipeline - the {@code .cons} format, the type-placeholder-position
|
||||
* JSON from JavaConstraintGenerator - uses the full name including the leading underscore
|
||||
* (e.g. {@code "_Foo_3"}). Restore it here so downstream consumers can match placeholder
|
||||
* names directly with no reformatting of their own.
|
||||
*/
|
||||
private static String toJson(Map<String, String> solution) {
|
||||
StringBuilder sb = new StringBuilder();
|
||||
sb.append("{\n");
|
||||
int i = 0;
|
||||
for (var entry : solution.entrySet()) {
|
||||
sb.append(" ").append(quote("_" + entry.getKey())).append(": ").append(quote(entry.getValue()));
|
||||
if (++i < solution.size()) sb.append(',');
|
||||
sb.append('\n');
|
||||
}
|
||||
sb.append("}\n");
|
||||
return sb.toString();
|
||||
}
|
||||
|
||||
private static String quote(String s) {
|
||||
StringBuilder sb = new StringBuilder(s.length() + 2);
|
||||
sb.append('"');
|
||||
for (int i = 0; i < s.length(); i++) {
|
||||
char c = s.charAt(i);
|
||||
switch (c) {
|
||||
case '"' -> sb.append("\\\"");
|
||||
case '\\' -> sb.append("\\\\");
|
||||
case '\n' -> sb.append("\\n");
|
||||
case '\r' -> sb.append("\\r");
|
||||
case '\t' -> sb.append("\\t");
|
||||
default -> {
|
||||
if (c < 0x20) {
|
||||
sb.append(String.format("\\u%04x", (int) c));
|
||||
} else {
|
||||
sb.append(c);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
sb.append('"');
|
||||
return sb.toString();
|
||||
}
|
||||
|
||||
private static void printUsage() {
|
||||
System.err.println("Usage: Main <subcommand> [args]");
|
||||
System.err.println();
|
||||
System.err.println(" gen-facts <constraints.cons> <out-facts.lp>");
|
||||
System.err.println(" Parse a .cons constraint file and write the equivalent ASP");
|
||||
System.err.println(" facts, ready to run through clingo together with unifyDiss.lp.");
|
||||
System.err.println();
|
||||
System.err.println(" cycle-check-facts <constraints.cons> <out-facts.lp>");
|
||||
System.err.println(" Write the facts for cycleCheck.lp. Run that first, with");
|
||||
System.err.println(" --enum-mode=brave: UNSATISFIABLE means the constraint set has no");
|
||||
System.err.println(" finite solution; otherwise its chosen(O,A) atoms say which");
|
||||
System.err.println(" or-constraint alternatives are still worth solving.");
|
||||
System.err.println();
|
||||
System.err.println(" gen-facts-pruned <constraints.cons> <brave-atoms.txt> <out-facts.lp>");
|
||||
System.err.println(" Like gen-facts, but drops every or-constraint alternative absent");
|
||||
System.err.println(" from the cycle check's brave consequences.");
|
||||
System.err.println();
|
||||
System.err.println(" parse-solution <clingo-atoms.txt> <out-solution.json>");
|
||||
System.err.println(" Parse clingo's answer-set atoms (only sigma(tph(...), type(...))");
|
||||
System.err.println(" atoms - filter clingo's output with show.lp first) and write a");
|
||||
System.err.println(" flat JSON object mapping each placeholder name to its solved type.");
|
||||
}
|
||||
}
|
||||
@@ -51,6 +51,92 @@ public class ASPGenerator {
|
||||
}
|
||||
}
|
||||
|
||||
/**
|
||||
* Emits the facts {@code cycleCheck.lp} consumes: one {@code alt/2} per or-constraint
|
||||
* alternative, plus the placeholder-level edges that alternative contributes.
|
||||
*
|
||||
* <p>Two edge kinds, and the distinction is the whole point of the check:
|
||||
* <ul>
|
||||
* <li>{@code containsEdge(O,A,P,Q)} - solving P means solving Q <em>inside</em> P's own
|
||||
* type, as in {@code _r <. C1<_p1>}. Only these can make a type contain itself.</li>
|
||||
* <li>{@code flowEdge(O,A,P,Q)} - P's type flows into Q's, as in {@code _p <. _res}.
|
||||
* A cycle of these alone is harmless: it means the two are the same type.</li>
|
||||
* </ul>
|
||||
*
|
||||
* <p>Deliberately conservative. An edge is emitted only where the constraint genuinely
|
||||
* forces containment, so {@code C<_q> <. _p} contributes nothing - being a supertype of
|
||||
* {@code C<_q>} does not oblige {@code _p} to contain {@code _q}. Missing an edge only
|
||||
* costs detection (the encoding's own Fail-Cycle remains as a backstop); inventing one
|
||||
* would reject a satisfiable constraint set.
|
||||
*
|
||||
* <p>Constraints outside any or-constraint arrive here as an or-constraint with a single
|
||||
* alternative, so they need no special handling - their edges are simply always chosen.
|
||||
*/
|
||||
public static String generateCycleCheckFacts(List<List<Set<Pair>>> orCons) {
|
||||
StringBuilder ret = new StringBuilder();
|
||||
for (int o = 0; o < orCons.size(); o++) {
|
||||
List<Set<Pair>> alternatives = orCons.get(o);
|
||||
for (int a = 0; a < alternatives.size(); a++) {
|
||||
ret.append("alt(").append(o).append(',').append(a).append(").\n");
|
||||
for (Pair pair : alternatives.get(a)) {
|
||||
appendEdges(ret, o, a, pair);
|
||||
}
|
||||
}
|
||||
}
|
||||
return ret.toString();
|
||||
}
|
||||
|
||||
private static void appendEdges(StringBuilder ret, int o, int a, Pair pair) {
|
||||
Type left;
|
||||
Type right;
|
||||
boolean symmetric;
|
||||
if (pair instanceof LessDot ld) {
|
||||
left = ld.left();
|
||||
right = ld.right();
|
||||
symmetric = false;
|
||||
} else if (pair instanceof EqualsDot ed) {
|
||||
left = ed.left();
|
||||
right = ed.right();
|
||||
symmetric = true;
|
||||
} else {
|
||||
return;
|
||||
}
|
||||
|
||||
if (left instanceof TypePlaceholder p && right instanceof TypePlaceholder q) {
|
||||
edge(ret, "flowEdge", o, a, p.name(), q.name());
|
||||
if (symmetric) edge(ret, "flowEdge", o, a, q.name(), p.name());
|
||||
return;
|
||||
}
|
||||
// P <. C<..Q..> / P =. C<..Q..> : P's type has to contain Q's.
|
||||
if (left instanceof TypePlaceholder p && right instanceof NamedType n) {
|
||||
for (String q : placeholdersIn(n)) edge(ret, "containsEdge", o, a, p.name(), q);
|
||||
}
|
||||
// C<..Q..> =. P : same obligation, equality being symmetric. The <. form is NOT included.
|
||||
if (symmetric && left instanceof NamedType n && right instanceof TypePlaceholder p) {
|
||||
for (String q : placeholdersIn(n)) edge(ret, "containsEdge", o, a, p.name(), q);
|
||||
}
|
||||
}
|
||||
|
||||
private static void edge(StringBuilder ret, String pred, int o, int a, String from, String to) {
|
||||
ret.append(pred).append('(').append(o).append(',').append(a)
|
||||
.append(",\"").append(from).append("\",\"").append(to).append("\").\n");
|
||||
}
|
||||
|
||||
/** Every type-placeholder name occurring anywhere inside {@code type}, at any depth. */
|
||||
private static Set<String> placeholdersIn(Type type) {
|
||||
Set<String> found = new java.util.LinkedHashSet<>();
|
||||
collectPlaceholders(type, found);
|
||||
return found;
|
||||
}
|
||||
|
||||
private static void collectPlaceholders(Type type, Set<String> found) {
|
||||
if (type instanceof TypePlaceholder p) {
|
||||
found.add(p.name());
|
||||
} else if (type instanceof NamedType n) {
|
||||
for (Type param : n.params()) collectPlaceholders(param, found);
|
||||
}
|
||||
}
|
||||
|
||||
public static String generateExtendsRelations(List<ExtendsRelation> extendsRelations) {
|
||||
String ret = "";
|
||||
for(var x : extendsRelations){
|
||||
|
||||
@@ -0,0 +1,97 @@
|
||||
import de.dhbwstuttgart.input.ConstraintParser;
|
||||
import de.dhbwstuttgart.sat.asp.ASPGenerator;
|
||||
import org.junit.Test;
|
||||
|
||||
import static org.junit.Assert.assertEquals;
|
||||
import static org.junit.Assert.assertTrue;
|
||||
|
||||
/**
|
||||
* The facts behind {@code src/main/asp/cycleCheck.lp}. A constraint set that forces a placeholder
|
||||
* to equal a type properly containing itself has no finite solution, and clingo's grounder
|
||||
* diverges on it rather than reporting UNSAT (see ../../ASP_BUGS.md, Bug 5). The check runs before
|
||||
* the solve, on placeholder identities alone, so it costs nothing however deep the types are.
|
||||
*
|
||||
* <p>What matters here is the containment/flow distinction: only a containment edge can put a
|
||||
* placeholder inside its own type, so only a cycle through one of those is fatal.
|
||||
*/
|
||||
public class CycleCheckTest {
|
||||
|
||||
private static String facts(String cons) {
|
||||
return ASPGenerator.generateCycleCheckFacts(ConstraintParser.parse(cons));
|
||||
}
|
||||
|
||||
// "_r <. C1<_p1>" - solving _r means solving _p1 inside it.
|
||||
@Test
|
||||
public void aPlaceholderBoundedByAParameterizedTypeYieldsAContainsEdge() {
|
||||
String f = facts("_r <. C1<_p1>,");
|
||||
assertTrue(f, f.contains("containsEdge(0,0,\"_r\",\"_p1\")"));
|
||||
assertTrue("no flow edge expected: " + f, !f.contains("flowEdge"));
|
||||
}
|
||||
|
||||
// "_p <. _res" between two placeholders is a plain flow: harmless on its own, and harmless
|
||||
// even in a cycle, because it never nests one type inside another.
|
||||
@Test
|
||||
public void aPlaceholderToPlaceholderConstraintYieldsAFlowEdge() {
|
||||
String f = facts("_p <. _res,");
|
||||
assertTrue(f, f.contains("flowEdge(0,0,\"_p\",\"_res\")"));
|
||||
assertTrue("no contains edge expected: " + f, !f.contains("containsEdge"));
|
||||
}
|
||||
|
||||
// Equality is symmetric, so it constrains in both directions.
|
||||
@Test
|
||||
public void equalityBetweenPlaceholdersYieldsBothFlowDirections() {
|
||||
String f = facts("_a =. _b,");
|
||||
assertTrue(f, f.contains("flowEdge(0,0,\"_a\",\"_b\")"));
|
||||
assertTrue(f, f.contains("flowEdge(0,0,\"_b\",\"_a\")"));
|
||||
}
|
||||
|
||||
// "C<_q> =. _p" says _p IS that type, so it must contain _q.
|
||||
@Test
|
||||
public void equalityWithAParameterizedTypeOnTheLeftStillYieldsAContainsEdge() {
|
||||
String f = facts("C1<_q> =. _p,");
|
||||
assertTrue(f, f.contains("containsEdge(0,0,\"_p\",\"_q\")"));
|
||||
}
|
||||
|
||||
// ...but "C<_q> <. _p" does not: being a supertype of C<_q> does not oblige _p to contain _q.
|
||||
// Deliberately conservative - a missing edge only costs detection, an invented one would
|
||||
// reject a satisfiable constraint set.
|
||||
@Test
|
||||
public void aParameterizedLowerBoundYieldsNoContainsEdge() {
|
||||
String f = facts("C1<_q> <. _p,");
|
||||
assertTrue("expected no containment obligation: " + f, !f.contains("containsEdge"));
|
||||
}
|
||||
|
||||
@Test
|
||||
public void nestedTypeArgumentsAreReachedAtEveryDepth() {
|
||||
String f = facts("_r <. C1<C2<_deep>>,");
|
||||
assertTrue(f, f.contains("containsEdge(0,0,\"_r\",\"_deep\")"));
|
||||
}
|
||||
|
||||
// Every alternative of an or-constraint is indexed separately, so the solver-side check can
|
||||
// pick alternatives independently - which is the whole point, since a cycle usually needs a
|
||||
// particular combination of them.
|
||||
@Test
|
||||
public void eachOrConstraintAlternativeIsIndexedSeparately() {
|
||||
String f = facts("{ _r <. C1<_p1>, _p1 <. _res | _r <. C2<_p2>, _p2 <. _res }");
|
||||
assertTrue(f, f.contains("alt(0,0)"));
|
||||
assertTrue(f, f.contains("alt(0,1)"));
|
||||
assertTrue(f, f.contains("containsEdge(0,0,\"_r\",\"_p1\")"));
|
||||
assertTrue(f, f.contains("containsEdge(0,1,\"_r\",\"_p2\")"));
|
||||
}
|
||||
|
||||
// A constraint outside any or-constraint becomes an or-constraint with one alternative, so
|
||||
// its edges are always chosen - no special case needed in the .lp.
|
||||
@Test
|
||||
public void mandatoryConstraintsBecomeASingleAlternativeOrConstraint() {
|
||||
String f = facts("_res <. _r,\n{ _r <. C1<_p1> | _r <. C2<_p1> }");
|
||||
long alts = f.lines().filter(l -> l.startsWith("alt(0,")).count();
|
||||
assertEquals("the mandatory conjunction should be one alternative: " + f, 1, alts);
|
||||
}
|
||||
|
||||
@Test
|
||||
public void groundConstraintsContributeNoEdgesAtAll() {
|
||||
String f = facts("java.lang.Integer <. java.lang.Number,");
|
||||
assertTrue("ground constraint should add no edges: " + f,
|
||||
!f.contains("containsEdge") && !f.contains("flowEdge"));
|
||||
}
|
||||
}
|
||||
@@ -0,0 +1,101 @@
|
||||
import de.dhbwstuttgart.Main;
|
||||
import org.junit.Test;
|
||||
|
||||
import java.io.IOException;
|
||||
import java.nio.file.Files;
|
||||
import java.nio.file.Path;
|
||||
|
||||
import static org.junit.Assert.assertEquals;
|
||||
import static org.junit.Assert.assertFalse;
|
||||
import static org.junit.Assert.assertTrue;
|
||||
|
||||
public class MainTest {
|
||||
|
||||
@Test
|
||||
public void genFactsWritesAspFacts() throws IOException {
|
||||
Path cons = Files.createTempFile("constraints", ".cons");
|
||||
Path facts = Files.createTempFile("facts", ".lp");
|
||||
try {
|
||||
Files.writeString(cons, "_Foo_3 <. java.lang.Number,\n");
|
||||
Main.main(new String[]{"gen-facts", cons.toString(), facts.toString()});
|
||||
String written = Files.readString(facts);
|
||||
assertTrue(written.contains("orCons("));
|
||||
assertTrue(written.contains("subcons(tph(\"_Foo_3\")"));
|
||||
assertTrue(written.contains("type(\"java.lang.Number\",null)"));
|
||||
} finally {
|
||||
Files.deleteIfExists(cons);
|
||||
Files.deleteIfExists(facts);
|
||||
}
|
||||
}
|
||||
|
||||
@Test
|
||||
public void genFactsAlsoIncludesExtendsRelations() throws IOException {
|
||||
// "Matrix < java.util.Vector" is exactly the extendsRelation text JavaConstraintGenerator
|
||||
// now emits (see JavaProjectExtractor#getExtendsRelations), mixed into the same .cons
|
||||
// file as ordinary constraints.
|
||||
Path cons = Files.createTempFile("constraints", ".cons");
|
||||
Path facts = Files.createTempFile("facts", ".lp");
|
||||
try {
|
||||
Files.writeString(cons, "Matrix < java.util.Vector\n_Foo_3 <. java.lang.Number,\n");
|
||||
Main.main(new String[]{"gen-facts", cons.toString(), facts.toString()});
|
||||
String written = Files.readString(facts);
|
||||
assertTrue(written.contains("orCons("));
|
||||
// A guarded rule, not a bare fact. Head and body are different predicates -
|
||||
// subtype/2 vs. subtype/1, the latter derived by unifyDiss.lp from subcons - so the
|
||||
// rule is not self-referential. The body is what binds the type parameters of a
|
||||
// generic extends relation, which is what keeps the rule safe for clingo.
|
||||
assertTrue("actual: " + written, written.contains(
|
||||
"subtype(type(\"Matrix\",null),type(\"java.util.Vector\",null))"
|
||||
+ ":-subtype(type(\"Matrix\",null))."));
|
||||
} finally {
|
||||
Files.deleteIfExists(cons);
|
||||
Files.deleteIfExists(facts);
|
||||
}
|
||||
}
|
||||
|
||||
@Test
|
||||
public void parseSolutionWritesJsonWithLeadingUnderscoreRestored() throws IOException {
|
||||
Path atoms = Files.createTempFile("atoms", ".txt");
|
||||
Path solution = Files.createTempFile("solution", ".json");
|
||||
try {
|
||||
Files.writeString(atoms, "sigma(tph(\"_Foo_3\"),type(\"java.lang.Integer\",null))");
|
||||
Main.main(new String[]{"parse-solution", atoms.toString(), solution.toString()});
|
||||
String json = Files.readString(solution);
|
||||
assertTrue(json.contains("\"_Foo_3\""));
|
||||
assertTrue(json.contains("\"java.lang.Integer\""));
|
||||
} finally {
|
||||
Files.deleteIfExists(atoms);
|
||||
Files.deleteIfExists(solution);
|
||||
}
|
||||
}
|
||||
|
||||
@Test
|
||||
public void genFactsHandlesAnEmptyConstraintFileWithoutCrashing() throws IOException {
|
||||
// Both ANTLR grammars require at least one entry, so a blank .cons file - e.g. from a
|
||||
// Java file with no constraint-generating constructs yet supported - must not crash.
|
||||
Path cons = Files.createTempFile("constraints", ".cons");
|
||||
Path facts = Files.createTempFile("facts", ".lp");
|
||||
try {
|
||||
Files.writeString(cons, "");
|
||||
Main.main(new String[]{"gen-facts", cons.toString(), facts.toString()});
|
||||
assertEquals("", Files.readString(facts));
|
||||
} finally {
|
||||
Files.deleteIfExists(cons);
|
||||
Files.deleteIfExists(facts);
|
||||
}
|
||||
}
|
||||
|
||||
@Test
|
||||
public void parseSolutionHandlesEmptyAtomsWithoutCrashing() throws IOException {
|
||||
Path atoms = Files.createTempFile("atoms", ".txt");
|
||||
Path solution = Files.createTempFile("solution", ".json");
|
||||
try {
|
||||
Files.writeString(atoms, "");
|
||||
Main.main(new String[]{"parse-solution", atoms.toString(), solution.toString()});
|
||||
assertEquals("{\n}\n", Files.readString(solution));
|
||||
} finally {
|
||||
Files.deleteIfExists(atoms);
|
||||
Files.deleteIfExists(solution);
|
||||
}
|
||||
}
|
||||
}
|
||||
@@ -3,7 +3,18 @@ import org.junit.Test;
|
||||
|
||||
import java.util.Map;
|
||||
|
||||
import static org.junit.Assert.assertEquals;
|
||||
|
||||
public class SolutionParserTest {
|
||||
@Test
|
||||
public void parsePlaceholderNameWithInternalUnderscore(){
|
||||
// JavaConstraintGenerator always names placeholders "_<basename>_<counter>", e.g.
|
||||
// "_Foo_3" - the tph rule's IDENTIFIER token must accept the internal underscore.
|
||||
String solution = "sigma(tph(\"_Foo_3\"),type(\"java.lang.Integer\",null))";
|
||||
Map<String,String> sigmas = SolutionParser.parse(solution);
|
||||
assertEquals("java.lang.Integer", sigmas.get("Foo_3"));
|
||||
}
|
||||
|
||||
@Test
|
||||
public void parseMatrixSolution(){
|
||||
String solution = "sigma(tph(\"_AMY\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AK\"),type(\"java.lang.Number\",null)) sigma(tph(\"_AY\"),type(\"java.lang.Number\",null)) sigma(tph(\"_J\"),type(\"java.lang.Number\",null)) sigma(tph(\"_V\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_G\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BK\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BA\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_U\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BU\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BO\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BG\"),type(\"java.lang.Number\",null)) sigma(tph(\"_BB\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BV\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AU\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AF\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_BC\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AS\"),type(\"java.util.Vector\",params(type(\"java.lang.Integer\",null)))) sigma(tph(\"_BD\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AG\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AV\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_ANN\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_ANH\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AD\"),type(\"Matrix\",null)) sigma(tph(\"_AP\"),type(\"java.util.Vector\",params(type(\"java.lang.Integer\",null)))) sigma(tph(\"_R\"),type(\"java.lang.Boolean\",null)) sigma(tph(\"_BR\"),type(\"Object\",null)) sigma(tph(\"_ANO\"),type(\"java.lang.Integer\",null)) sigma(tph(\"_AB\"),type(\"Matrix\",null)) sigma(tph(\"_AM\"),type(\"java.util.Vector\",params(type(\"java.lang.Integer\",null))))\n";
|
||||
|
||||
Reference in new issue
Block a user