diff --git a/src/lib/souffle/ast/declarations/adt.ts b/src/lib/souffle/ast/declarations/adt.ts index 92b00e3..f8b9704 100644 --- a/src/lib/souffle/ast/declarations/adt.ts +++ b/src/lib/souffle/ast/declarations/adt.ts @@ -13,9 +13,9 @@ export class AlgebraicDataType extends Declaration { } pp(indent: string = ""): string { - return `${indent}.type ${this.name} = [${this.branches + return `${indent}.type ${this.name} = ${this.branches .map((b) => `${b[0]} {${b[1].map((f) => `${f[0]}: ${f[1].pp()}`).join(", ")}}`) - .join(" | ")}]`; + .join(" | ")}`; } children(): Iterable { diff --git a/src/lib/souffle/ast/declarations/component.ts b/src/lib/souffle/ast/declarations/component.ts index ea6dee3..c8a83df 100644 --- a/src/lib/souffle/ast/declarations/component.ts +++ b/src/lib/souffle/ast/declarations/component.ts @@ -18,10 +18,12 @@ export class Component extends Declaration { } pp(indent: string = ""): string { + const innerIndent = indent + " "; + return `${indent}.comp ${Component.ppCompInv([this.name, this.typeParams])}${ - this.bases.length ? 0 : this.bases.map(Component.ppCompInv).join(", ") + this.bases.length == 0 ? "" : ":" + this.bases.map(Component.ppCompInv).join(", ") } { - ${this.body.map((x) => x.pp(indent + " ")).join("\n")} + ${this.body.map((x) => x.pp(innerIndent)).join("\n")} }`; } @@ -30,6 +32,6 @@ export class Component extends Declaration { } getStructId(): any { - return [this.name, ...this.typeParams, ...this.bases, ...this.body]; + return [this.name, this.typeParams, this.bases, this.body]; } } diff --git a/src/lib/souffle/ast/declarations/directive.ts b/src/lib/souffle/ast/declarations/directive.ts index 65c90ca..e626c1f 100644 --- a/src/lib/souffle/ast/declarations/directive.ts +++ b/src/lib/souffle/ast/declarations/directive.ts @@ -13,9 +13,11 @@ export class Directive extends Declaration { } pp(indent: string = ""): string { - return `${indent}${this.type} ${this.name}(${this.parameters - .map(([name, val]) => `${name} = ${val}`) - .join(", ")})`; + const paramStr = this.parameters + .map(([name, val]) => `${name} = ${typeof val === "string" ? `"${val}"` : val}`) + .join(", "); + + return `${indent}${this.type} ${this.name}${paramStr.length > 0 ? `(${paramStr})` : ""}`; } children(): Iterable { @@ -23,6 +25,6 @@ export class Directive extends Declaration { } getStructId(): any { - return [this.type, this.name, ...this.parameters]; + return [this.type, this.name, this.parameters]; } } diff --git a/src/lib/souffle/ast/declarations/functor.ts b/src/lib/souffle/ast/declarations/functor.ts index cd89048..f30dbf6 100644 --- a/src/lib/souffle/ast/declarations/functor.ts +++ b/src/lib/souffle/ast/declarations/functor.ts @@ -24,6 +24,6 @@ export class Functor extends Declaration { } getStructId(): any { - return [this.name, ...this.args, this.returnType, this.stateful]; + return [this.name, this.args, this.returnType, this.stateful]; } } diff --git a/src/lib/souffle/ast/declarations/record_type.ts b/src/lib/souffle/ast/declarations/record_type.ts index d4b41a3..1c612b9 100644 --- a/src/lib/souffle/ast/declarations/record_type.ts +++ b/src/lib/souffle/ast/declarations/record_type.ts @@ -22,6 +22,6 @@ export class RecordType extends Declaration { } getStructId(): any { - return [this.name, ...this.fields]; + return [this.name, this.fields]; } } diff --git a/src/lib/souffle/ast/declarations/relation.ts b/src/lib/souffle/ast/declarations/relation.ts index 93c05b4..559cde2 100644 --- a/src/lib/souffle/ast/declarations/relation.ts +++ b/src/lib/souffle/ast/declarations/relation.ts @@ -40,7 +40,7 @@ export class Relation extends Declaration { return `${indent}.decl ${this.name}(${this.args .map((a) => `${a[0]}: ${a[1].pp()}`) - .join(", ")}) ${[...this.tags].join(" ")}${ + .join(", ")}) ${[...this.tags].join(" ") + " "}${ choiceStrs.length > 0 ? `choice-domain ${choiceStrs.join(", ")}` : "" }`; } @@ -50,6 +50,8 @@ export class Relation extends Declaration { } getStructId(): any { - return [this.name, ...this.args, [...this.tags], this.choiceDomains]; + const tags = [...this.tags]; + tags.sort(); + return [this.name, this.args, tags, this.choiceDomains]; } } diff --git a/src/lib/souffle/ast/declarations/rule.ts b/src/lib/souffle/ast/declarations/rule.ts index 9896c0b..45c71be 100644 --- a/src/lib/souffle/ast/declarations/rule.ts +++ b/src/lib/souffle/ast/declarations/rule.ts @@ -19,7 +19,7 @@ export class Rule extends Declaration { let queryPlanStr = ""; if (this.queryPlan.length > 0) { - queryPlanStr += ".plan"; + queryPlanStr += " .plan"; queryPlanStr += this.queryPlan .map(([num, nums]) => `${num}: (${nums.map((x) => `${x}`).join(", ")})`) .join(", "); diff --git a/src/lib/souffle/ast/expressions/binary.ts b/src/lib/souffle/ast/expressions/binary.ts index 16ab7cf..40e8a56 100644 --- a/src/lib/souffle/ast/expressions/binary.ts +++ b/src/lib/souffle/ast/expressions/binary.ts @@ -1,7 +1,22 @@ import { Node, Src } from "../node"; import { Expression } from "./expression"; -export type BinaryOp = "+"; +export type BinaryOp = + | "+" + | "-" + | "*" + | "/" + | "%" + | "^" + | "land" + | "lor" + | "lxor" + | "band" + | "bor" + | "bxor" + | "bshl" + | "bshr" + | "bshru"; export class BinaryOperator extends Expression { constructor( diff --git a/src/lib/souffle/ast/expressions/unary.ts b/src/lib/souffle/ast/expressions/unary.ts index c7bbbff..ad44ca5 100644 --- a/src/lib/souffle/ast/expressions/unary.ts +++ b/src/lib/souffle/ast/expressions/unary.ts @@ -1,7 +1,7 @@ import { Node, Src } from "../node"; import { Expression } from "./expression"; -export type UnaryOp = "-" | "~" | "!"; +export type UnaryOp = "-" | "bnot" | "lnot"; export class UnaryOperator extends Expression { constructor( @@ -13,7 +13,7 @@ export class UnaryOperator extends Expression { } pp(): string { - return `${this.op}(${this.subExpr.pp()})`; + return `(${this.op}${this.subExpr.pp()})`; } children(): Iterable { diff --git a/src/lib/souffle/ast/rules/atom.ts b/src/lib/souffle/ast/rules/atom.ts index 4a46e81..a0a27c4 100644 --- a/src/lib/souffle/ast/rules/atom.ts +++ b/src/lib/souffle/ast/rules/atom.ts @@ -19,6 +19,6 @@ export class Atom extends Node { } getStructId(): any { - return [this.name, ...this.args]; + return [this.name, this.args]; } } diff --git a/src/lib/souffle/ast/rules/constraints/comparison.ts b/src/lib/souffle/ast/rules/constraints/comparison.ts index 6bfc642..4bb209c 100644 --- a/src/lib/souffle/ast/rules/constraints/comparison.ts +++ b/src/lib/souffle/ast/rules/constraints/comparison.ts @@ -15,7 +15,7 @@ export class Comparison extends Constraint { } pp(): string { - return `${this.lhs.pp()} ${this.op} ${this.rhs.pp()}`; + return `(${this.lhs.pp()} ${this.op} ${this.rhs.pp()})`; } children(): Iterable { diff --git a/test/samples/analyses/fcall.json b/test/samples/analyses/fcall.json index fba8b15..caffa8b 100644 --- a/test/samples/analyses/fcall.json +++ b/test/samples/analyses/fcall.json @@ -12,7 +12,9 @@ [52, 15, [52, [15, null]]], [52, 22, [52, [8, [22, null]]]], [52, 29, [52, [15, [29, null]]]], + [52, 29, [52, [8, [22, [29, null]]]]], [52, 40, [52, [15, [29, [40, null]]]]], + [52, 40, [52, [8, [22, [29, [40, null]]]]]], [59, 59, [59, [59, null]]] ] } diff --git a/test/succ.spec.ts b/test/succ.spec.ts index 73e022f..929e974 100644 --- a/test/succ.spec.ts +++ b/test/succ.spec.ts @@ -185,13 +185,13 @@ describe("Test succ relation for all samples", () => { describe(sample, () => { let units: sol.SourceUnit[]; let infer: sol.InferType; - let contents: string; + let contents: Buffer; let succ: Fact[]; let succFirst: NdGraph; let g: NdGraph; before(async () => { - contents = fse.readFileSync(sample, { encoding: "utf-8" }); + contents = fse.readFileSync(sample); const result = await sol.compileSol(sample, "auto"); const data = result.data;