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

Deprecate standalone kani, add support for cargo-kani for every call #46

Merged
merged 5 commits into from
Mar 16, 2023
Merged

Deprecate standalone kani, add support for cargo-kani for every call #46

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
cfb3eb6
Switch to cargo-kani for all commands, and deprecate usage of standal…
jaisnan Mar 10, 2023
f5329e4
Remove execution paths for standalone Kani
jaisnan Mar 10, 2023
5b755c5
Revert Es version change
jaisnan Mar 16, 2023
fff4681
Clean up redundant variables
jaisnan Mar 16, 2023
54dc5f7
Correct NaN check for args variable
jaisnan Mar 16, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
46 changes: 5 additions & 41 deletions src/model/kaniCommandCreate.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,30 +29,6 @@ export async function runKaniHarnessInterface(
return kaniOutput;
}

/**
* Run Kani as a command line binary
*
* @param rsFile - Path to the file that is to be verified
* @param harnessName - name of the harness that is to be verified
* @param args - arguments to Kani if provided
* @returns verification status (i.e success or failure)
*/
export async function runKaniHarness(
rsFile: string,
harnessName: string,
args?: number,
): Promise<any> {
let harnessCommand = '';
if (args !== undefined || NaN) {
harnessCommand = `${KaniConstants.KaniExecutableName} ${rsFile} ${KaniArguments.harnessFlag} ${harnessName} ${KaniArguments.unwindFlag} ${args}`;
} else {
harnessCommand = `${KaniConstants.KaniExecutableName} ${rsFile} ${KaniArguments.harnessFlag} ${harnessName}`;
}
// Kani Output
const kaniOutput = await catchOutput(harnessCommand);
return kaniOutput;
}

/**
* Run cargo Kani --tests as a command line binary for harness declared
* under #[test]
Expand Down Expand Up @@ -98,26 +74,14 @@ export async function captureFailedChecks(
args?: number,
): Promise<KaniResponse> {
let harnessCommand = '';
if (args === undefined) {
harnessCommand = `${KaniConstants.KaniExecutableName} ${rsFile} ${KaniArguments.harnessFlag} ${harnessName}`;
} else {
harnessCommand = `${KaniConstants.KaniExecutableName} ${rsFile} ${KaniArguments.harnessFlag} ${harnessName} ${KaniArguments.unwindFlag} ${args}`;
}
const kaniOutput = await createFailedDiffMessage(harnessCommand);
if (kaniOutput.failedProperty == 'error') {
const crateURI = getRootDir();
let harnessCommand = '';

if (args === undefined || NaN) {
harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.harnessFlag} ${harnessName} --output-format terse`;
} else {
harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.harnessFlag} ${harnessName} ${KaniArguments.unwindFlag} ${args} --output-format terse`;
}
const kaniOutput = await createFailedDiffMessage(harnessCommand);
return kaniOutput;
if (args === undefined || NaN) {
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.harnessFlag} ${harnessName}`;
} else {
return kaniOutput;
harnessCommand = `${KaniConstants.CargoKaniExecutableName} ${KaniArguments.harnessFlag} ${harnessName} ${KaniArguments.unwindFlag} ${args}`;
}
const kaniOutput = await createFailedDiffMessage(harnessCommand);
return kaniOutput;
}

// Generic function to run a command (Kani | Cargo Kani)
Expand Down
23 changes: 1 addition & 22 deletions src/model/kaniRunner.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,7 @@ export async function runKaniCommand(
// Get cargo command and args for the command to be executed
const command = commmandSplit.commandPath;
const args = commmandSplit.args;
let kaniBinaryPath = '';
const kaniBinaryPath = '';
jaisnan marked this conversation as resolved.
Show resolved Hide resolved

if (command == 'cargo' || command == 'cargo kani') {
const kaniBinaryPath = await getKaniPath('cargo-kani');
Expand All @@ -71,13 +71,6 @@ export async function runKaniCommand(
cwd: directory,
};

return executeKaniProcess(kaniBinaryPath, args, options, cargoKaniMode);
} else if (command == 'kani') {
kaniBinaryPath = await getKaniPath(command);
const options = {
shell: false,
};

return executeKaniProcess(kaniBinaryPath, args, options, cargoKaniMode);
} else {
return false;
Expand Down Expand Up @@ -106,20 +99,6 @@ export async function runKaniCommand(
cwd: directory,
};

return new Promise((resolve, reject) => {
execFile(kaniBinaryPath, args, options, (error, stdout, stderr) => {
if (stdout) {
const responseObject: KaniResponse = responseParserInterface(stdout);
resolve(responseObject);
}
});
});
} else if (commmandSplit.commandPath == 'kani') {
const kaniBinaryPath = await getKaniPath('kani');
const options = {
shell: false,
};

return new Promise((resolve, reject) => {
execFile(kaniBinaryPath, args, options, (error, stdout, stderr) => {
if (stdout) {
Expand Down
4 changes: 2 additions & 2 deletions tsconfig.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
{
"compilerOptions": {
"module": "commonjs",
"target": "ES2020",
"target": "ES2018",
jaisnan marked this conversation as resolved.
Show resolved Hide resolved
"outDir": "out",
"lib": [
"ES2020"
"ES2018"
],
"sourceMap": true,
"rootDir": "src",
Expand Down