Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

path constraint check #2

Merged
merged 1 commit into from
Jan 21, 2021
Merged

path constraint check #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
80 changes: 70 additions & 10 deletions packages/pytea/src/backend/context.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,9 @@ interface ContextMethods<T> {
// immediate linear SMT : generates conservative range.
getCachedRange(num: number | ExpNum): NumRange | undefined; // return conservative range
checkImmediate(constraint: Constraint): boolean | undefined; // return true if always true, false if always false, undefined if don't know

// Check if this ctx has path constraints.
hasPathCtr(): boolean;
}

export interface ContextSet<T> {
Expand All @@ -224,6 +227,7 @@ export interface ContextSet<T> {

getList(): List<Context<T>>;
getFailed(): List<Context<SVError>>;
getStopped(): List<Context<SVError>>;

isEmpty(): boolean;
addLog(message: string, source?: ParseNode): ContextSet<T>;
Expand Down Expand Up @@ -741,6 +745,11 @@ export class Context<T> extends Record(contextDefaults) implements ContextProps<
checkImmediate(constraint: Constraint): boolean | undefined {
return this.ctrSet.checkImmediate(constraint);
}

// Check if this ctx has path constraints.
hasPathCtr(): boolean {
return !this.ctrSet.pathCtr.isEmpty();
}
}

export class ContextSetImpl<T> implements ContextSet<T> {
Expand All @@ -749,11 +758,15 @@ export class ContextSetImpl<T> implements ContextSet<T> {
private _ctxList: List<Context<T>>;
// failed path
private _failed: List<Context<SVError>>;
// stopped path: failed but possibly unreachable path
// TODO: path constraint resolution
private _stopped: List<Context<SVError>>;

constructor(ctxList: List<Context<T>>, failed?: List<Context<SVError>>) {
constructor(ctxList: List<Context<T>>, failed?: List<Context<SVError>>, stopped?: List<Context<SVError>>) {
this.env = false;
this._ctxList = ctxList;
this._failed = failed ? failed : List();
this._stopped = stopped ? stopped : List();
}

static fromCtx<A>(ctx: Context<A>): ContextSet<A> {
Expand All @@ -762,9 +775,13 @@ export class ContextSetImpl<T> implements ContextSet<T> {
if (failedCtx.failId === -1) {
failedCtx = failedCtx.set('failId', getFailedId());
}
return new ContextSetImpl(List(), List([failedCtx]));
if (failedCtx.hasPathCtr()) {
return new ContextSetImpl(List(), List(), List([failedCtx]));
} else {
return new ContextSetImpl(List(), List([failedCtx]), List());
}
} else {
return new ContextSetImpl(List([ctx]), List());
return new ContextSetImpl(List([ctx]), List(), List());
}
}

Expand All @@ -776,20 +793,33 @@ export class ContextSetImpl<T> implements ContextSet<T> {
return this._failed;
}

getStopped(): List<Context<SVError>> {
return this._stopped;
}

filter(tester: (ctx: Context<T>) => boolean): ContextSet<T> {
return new ContextSetImpl(this._ctxList.filter(tester), this._failed);
return new ContextSetImpl(this._ctxList.filter(tester), this._failed, this._stopped);
}

setCtxList<A>(ctxList: List<Context<A>>): ContextSet<A> {
const succeed = ctxList.filter((ctx) => ctx.failed === undefined);
const failed = ctxList
.filter((ctx) => ctx.failed !== undefined)
.filter((ctx) => !ctx.hasPathCtr())
.map((ctx) => {
let failed = ctx.setRetVal(ctx.failed!);
if (ctx.failId === -1) failed = failed.set('failId', getFailedId());
return failed;
});
return new ContextSetImpl(succeed, this._failed.concat(failed));
const stopped = ctxList
.filter((ctx) => ctx.failed !== undefined)
.filter((ctx) => ctx.hasPathCtr())
.map((ctx) => {
let stopped = ctx.setRetVal(ctx.failed!);
if (ctx.failId === -1) stopped = stopped.set('failId', getFailedId());
return stopped;
});
return new ContextSetImpl(succeed, this._failed.concat(failed), this._stopped.concat(stopped));
}

map<A>(mapper: (ctx: Context<T>) => Context<A>): ContextSet<A> {
Expand All @@ -800,26 +830,44 @@ export class ContextSetImpl<T> implements ContextSet<T> {
const mapped = this._ctxList.map(mapper);
const succeed = mapped.toArray().flatMap((cs) => cs.getList().toArray());
const failed = mapped.toArray().flatMap((cs) => cs.getFailed().toArray());
const stopped = mapped.toArray().flatMap((cs) => cs.getStopped().toArray());

return new ContextSetImpl(List(succeed), List(failed).concat(this._failed));
return new ContextSetImpl(
List(succeed),
List(failed).concat(this._failed),
List(stopped).concat(this._stopped)
);
}

return<A>(retVal: A): ContextSet<A> {
return new ContextSetImpl(
this._ctxList.map((ctx) => ctx.setRetVal(retVal)),
this._failed
this._failed,
this._stopped
);
}

fail(errMsg: string, source?: ParseNode): ContextSet<SVError> {
return new ContextSetImpl(
List(),
this._ctxList
.filter((ctx) => {
!ctx.hasPathCtr();
})
.map((ctx) => {
const err = SVError.create(errMsg, source);
return ctx.fail(err);
})
.concat(this._failed)
.concat(this._failed),
this._ctxList
.filter((ctx) => {
ctx.hasPathCtr();
})
.map((ctx) => {
const err = SVError.create(errMsg, source);
return ctx.fail(err);
})
.concat(this._stopped)
);
}

Expand All @@ -833,7 +881,16 @@ export class ContextSetImpl<T> implements ContextSet<T> {
this._failed.forEach((ctx) => (failedSet[ctx.failId] = ctx));
thatFailed.forEach((ctx) => (failedSet[ctx.failId] = ctx));

return new ContextSetImpl(thisList.concat(thatList), List(Object.values(failedSet)));
const stoppedSet: { [id: number]: Context<SVError> } = {};
const thatStopped = ctxSet.getStopped();
this._stopped.forEach((ctx) => (stoppedSet[ctx.failId] = ctx));
thatStopped.forEach((ctx) => (stoppedSet[ctx.failId] = ctx));

return new ContextSetImpl(
thisList.concat(thatList),
List(Object.values(failedSet)),
List(Object.values(stoppedSet))
);
}

require(ctr: Constraint | Constraint[], failMsg?: string, source?: ParseNode): ContextSet<T | SVError> {
Expand Down Expand Up @@ -879,7 +936,10 @@ export class ContextSetImpl<T> implements ContextSet<T> {
}
});

return [new ContextSetImpl(List(ifPath), this._failed), new ContextSetImpl(List(elsePath), this._failed)];
return [
new ContextSetImpl(List(ifPath), this._failed, this._stopped),
new ContextSetImpl(List(elsePath), this._failed, this._stopped),
];
}

isEmpty(): boolean {
Expand Down
46 changes: 46 additions & 0 deletions packages/pytea/src/service/pyteaService.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -368,6 +368,7 @@ export class PyteaService {
private _resultOnlyLog(result: ContextSet<ShValue | ShContFlag>): void {
const success = result.getList();
const failed = result.getFailed();
const stopped = result.getStopped();

failed.forEach((ctx, i) => {
const source = ctx.retVal.source;
Expand All @@ -381,6 +382,7 @@ export class PyteaService {

this._console.log(
chalk.green(`potential success path #: ${success.count()}\n`) +
chalk.yellow(`potential unreachable path #: ${stopped.count()}\n`) +
chalk.red(`immediate failed path #: ${failed.count()}\n\n`) +
'RUNNING TIMES:\n' +
this._timeLog.map(([name, interval]) => ` ${name}: ${(interval / 1000).toFixed(4)}s`).join('\n')
Expand All @@ -390,6 +392,7 @@ export class PyteaService {
private _reducedLog(result: ContextSet<ShValue | ShContFlag>): void {
const success = result.getList();
const failed = result.getFailed();
const stopped = result.getStopped();

const jsonList: string[] = [];

Expand Down Expand Up @@ -422,6 +425,30 @@ export class PyteaService {
);
});

stopped.forEach((ctx, i) => {
jsonList.push(ctx.ctrSet.getConstraintJSON());

const source = ctx.retVal.source;

const heapLog = ctx.env.addrMap
.filter((v) => v.addr >= 0)
.map((addr, key) => {
return ` ${key} => ${this._reducedToString(addr, ctx.heap)}`;
})
.join('\n');

this._console.log(
chalk.yellow(`stopped path #${i + 1}`) +
`: ${ctx.retVal.reason} - ${PyteaUtils.formatParseNode(source)}\n\n` +
`LOGS:\n${ctx.logsToString()}\n\n` +
'CONSTRAINTS:\n' +
ctx.ctrSet.toString() +
'\n\nCALL STACK:\n' +
ctx.callStackToString() +
`\n\nREDUCED HEAP (${ctx.heap.valMap.count()}):\n${heapLog}`
);
});

failed.forEach((ctx, i) => {
const source = ctx.retVal.source;

Expand All @@ -448,6 +475,7 @@ export class PyteaService {

this._console.log(
chalk.green(`potential success path #: ${success.count()}\n`) +
chalk.yellow(`potential unreachable path #: ${stopped.count()}\n`) +
chalk.red(`immediate failed path #: ${failed.count()}\n\n`) +
'RUNNING TIMES:\n' +
this._timeLog.map(([name, interval]) => ` ${name}: ${(interval / 1000).toFixed(4)}s`).join('\n')
Expand All @@ -457,6 +485,7 @@ export class PyteaService {
private _fullLog(result: ContextSet<ShValue | ShContFlag>): void {
const success = result.getList();
const failed = result.getFailed();
const stopped = result.getStopped();

if (this._mainStmt) {
this._console.log(
Expand All @@ -474,6 +503,22 @@ export class PyteaService {
);
});

stopped.forEach((ctx, i) => {
const source = ctx.retVal.source;

this._console.log(
chalk.yellow(`stopped path #${i + 1}`) +
`: ${ctx.retVal.reason} / at ${ctx.relPath} ${PyteaUtils.formatParseNode(source)}\n` +
`LOGS:\n${ctx.logsToString()}\n` +
'CONSTRAINTS:\n' +
ctx.ctrSet.toString() +
'\n\nCALL STACK:\n' +
ctx.callStackToString() +
`\nENV:\n${ctx.env.toString()}\n` +
`\nHEAP (${ctx.heap.valMap.count()}):\n${ctx.heap.filter((_, key) => key >= 0).toString()}`
);
});

failed.forEach((ctx, i) => {
const source = ctx.retVal.source;

Expand All @@ -494,6 +539,7 @@ export class PyteaService {

this._console.log(
chalk.green(`potential success path #: ${success.count()}\n`) +
chalk.yellow(`potential unreachable path #: ${stopped.count()}\n`) +
chalk.red(`immediate failed path #: ${failed.count()}\n\n`) +
'RUNNING TIMES:\n' +
this._timeLog.map(([name, interval]) => ` ${name}: ${(interval / 1000).toFixed(4)}s`).join('\n')
Expand Down
6 changes: 6 additions & 0 deletions packages/pytea/src/service/pyteaUtils.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -286,6 +286,9 @@ export function runZ3Py<T>(result: ContextSet<T>): void {
result.getList().forEach((ctx) => {
jsonList.push(ctx.ctrSet.getConstraintJSON());
});
result.getStopped().forEach((ctx) => {
jsonList.push(ctx.ctrSet.getConstraintJSON());
});

if (jsonList.length === 0) {
return;
Expand All @@ -307,6 +310,9 @@ export function exportConstraintSet<T>(result: ContextSet<T>, path: string): voi
result.getList().forEach((ctx) => {
jsonList.push(ctx.ctrSet.getConstraintJSON());
});
result.getStopped().forEach((ctx) => {
jsonList.push(ctx.ctrSet.getConstraintJSON());
});

const jsonStr = `[\n${jsonList.join(',\n')}\n]`;
fs.writeFileSync(path, jsonStr);
Expand Down