Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
36 changes: 36 additions & 0 deletions scripts/ci/preflight-steps/check-outdated.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
#!/usr/bin/python3
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
import subprocess

def run_cargo_command(command, working_directory):

try:
process = subprocess.Popen(
command,
stdout=subprocess.PIPE,
stderr=subprocess.PIPE,
shell=True,
text=True,
cwd=working_directory)
stdout, stderr = process.communicate()

if process.returncode != 0:
print(f"Command '{command}' executed unsuccesfully, in '{working_directory}'.")
print(stderr)
else:
print(f"Command '{command}' executed succesfully, in '{working_directory}'.")
print(stdout)
except Exception as e:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not sure that there's an need for try-except here. If Popen raises, I think the program should crash out early.

There's also no need to use shell=True here, please pass the command as a list.

More generally I'm not sure that there's any need to buffer the output and then immediately print it. I think this code could be a lot shorter:

cmds = [
  ["cargo", "install", "cargo-outdated"],
  ["cargo", "outdated", "--workspace"],
]
exit_code = 0
for cmd in cmds:
    proc = subprocess.run(cmd, cwd=working_directory)
    exit_code += proc.returncode
sys.exit(exit_code)

print(f"Error: {str(e)}")


def main():

target_directory = "kani"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this be working_directory?

run_cargo_command("cargo install cargo-outdated", working_directory)
run_cargo_command("cargo outdated --workspace", working_directory)


if __name__ == "__main__":
main()
23 changes: 23 additions & 0 deletions scripts/ci/preflight-steps/dependency_links.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
#!/usr/bin/python3
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm going to propose that we don't duplicate this information, see this

# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
dependencies_links = {
'cbmc': {
'dependency_name': 'cbmc',
'dependency_string': 'CBMC_VERSION',
'org_name': 'diffblue',
'link': 'https://github.com/diffblue/cbmc'
},
'cbmc_viewer': {
'dependency_name': 'cbmc-viewer',
'dependency_string': 'CBMC_VIEWER_VERSION',
'org_name': 'model-checking',
'link': 'https://github.com/model-checking/cbmc-viewer'
},
'kissat': {
'dependency_name': 'kissat',
'dependency_string': 'KISSAT_VERSION',
'org_name': 'arminbiere',
'link': 'https://github.com/arminbiere/kissat'
}
}
58 changes: 58 additions & 0 deletions scripts/ci/preflight-steps/dependency_updater.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,58 @@
#!/usr/bin/python3
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
import re
import requests

class VersionUpdater:
def __init__(self, file, dependency):
self.file = file
self.dependency = dependency
self.dependencies = {}

def get_latest_version(self, org_name, crate_name):
url = f"https://github.com/{org_name}/{crate_name}/releases/latest"
response = requests.get(url)
if response.status_code == 404:
raise ValueError(f"Failed to find latest version for crate '{crate_name}' on GitHub.")
else:
return re.search(r"v?(\d+\.\d+(\.\d+)?(-\S+)?)", response.url).group(1)

def read_dependencies(self):
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this method need to exist? It seems that its reading the current version numbers. But those never get used, they immediately get overwritten by the latest version number in update_dependencies?


with open(self.file, 'r') as f:
contents = f.readlines()

for line in contents:
if "CBMC_VERSION" in line:
version_number = line.split("=")[1].replace("\n", "")
self.dependencies["CBMC_VERSION"] = version_number
elif "CBMC_VIEWER_VERSION" in line:
version_number = line.split("=")[1].replace("\n", "")
self.dependencies["CBMC_VIEWER_VERSION"] = version_number
elif "KISSAT_VERSION" in line:
version_number = line.split("=")[1].replace("\n", "")
self.dependencies["KISSAT_VERSION"] = version_number
else:
pass

def update_dependencies(self):
latest_version = self.get_latest_version(self.dependency["org_name"], self.dependency["dependency_name"])
self.dependencies[self.dependency["dependency_string"]] = latest_version

def write_dependencies(self):
with open(self.file, 'r') as f:
lines = f.readlines()
with open(self.file, 'w') as f:
for line in lines:
match = re.search(r'(\w+)="\d+(\.\d+)+"', line.strip())
if match and match.group(1).strip() == self.dependency["dependency_string"]:
f.write(
f'{self.dependency["dependency_string"]}="{self.dependencies[self.dependency["dependency_string"]]}"\n')
else:
f.write(line)

def run_process(self):
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's not clear to me that you need to walk through the file, updating the existing values. It seems much quicker to overwrite the entire file.

If you have a dict like this:

new_versions = {
  "CBMC_VIEWER": 3.9,
  "CBMC": 5.99.0,
  ...
}

then I think it would be much clearer to do this:

with open("kani-dependencies", "w") as handle:
    for tool, version in new_versions.items():
        print(f"{tool}={version}", file=handle)

then you don't need the if-statement on line 27, which hard-codes the tool names and will thus need to be updated whenever we add a new dependency.

so my suggestion is:

  1. Get the list of existing tools by opening kani-dependencies, read each line, split on =, return the first part
  2. Turn that list of tools into the new versions dict, using a variation of your get_latest_version method
  3. Write the dict out using the 3 lines of code above, no need to update the existing file, just overwrite it.

I think this would make the code a lot shorter and clearer, and avoid hardcoding the tool names here. kani-dependencies is the only place those names should be written.

self.read_dependencies()
self.update_dependencies()
self.write_dependencies()
12 changes: 12 additions & 0 deletions scripts/ci/preflight-steps/update-cbmc-viewer.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#!/usr/bin/python3
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure that it makes sense to have three files for CBMC, Viewer, and Kissat, when the files are almost identical.

I like that you've specified the dependencies in a data structure in dependency_links.py. My suggestion is to have a single script that iterates over that dict, instead of manually specifying the key each time.

for dep_name, info in dependency_links.items():
     updater = VersionUpdater(kani_dependencies_path, dependencies_links[dep_name])
    updater.run_process()

This way, we can add more dependencies simply by adding to the dict, without adding any new code, because the logic is the same.

(info is unused in the code above but I think it should be passed to run_process or to the VersionUpdater constructor)

# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
from job_runner import dependencies_links
from dependency_updater import VersionUpdater

# Set the name of the dependency you want to update
kani_dependencies_path = "/Users/jaisnan/kani/kani-dependencies"

if __name__ == "__main__":
updater = VersionUpdater(kani_dependencies_path, dependencies_links["cbmc_viewer"])
updater.run_process()
12 changes: 12 additions & 0 deletions scripts/ci/preflight-steps/update-cbmc.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#!/usr/bin/python3
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
from job_runner import dependencies_links
from dependency_updater import VersionUpdater

# Set the name of the dependency you want to update
kani_dependencies_path = "/Users/jaisnan/kani/kani-dependencies"
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This shouldn't be using the full path, just kani-dependencies should be fine


if __name__ == "__main__":
updater = VersionUpdater(kani_dependencies_path, dependencies_links["cbmc"])
updater.run_process()
45 changes: 45 additions & 0 deletions scripts/ci/preflight-steps/update-kani-version.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
#!/usr/bin/python3
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The correct shebang line for python (and most other interpreters) is #!/usr/bin/env python3

# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
import toml
import sys

def update_version(file_path, new_version):

try:
# load the toml file
with open(file_path, 'r') as f:
data = toml.load(f)

# update the version number
data['package']['version'] = new_version

with open(file_path, 'w') as f:
toml.dump(data, f)

print(f"Version updated succesfully to '{version_number}' in '{file_path}'.")
except Exception as e:
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't see a need to catch Exception here or anywhere else... I suggest removing the try-catch unless there's a specific exception that's likely to be thrown here.

print(f"Error updating kani version to '{version_number}' in '{file_path}'.")


def main():
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This file doesn't appear to do anything because it doesn't actually call update_version

if len(sys.argv) != 2:
print("Usage: python update_versions.py <new_version>")
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggest that instead of asking the user to specify the new version, you should read the version from Cargo.toml, reset the patch number and bump the minor number, and use that. Having to specify a version number manually should be optional.

sys.exit(1)

# The new version number specified by the user
new_version = sys.argv[1]

# The list of Cargo.toml files to update
cargo_toml_files = [
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm not sure that this should be hardcoded. How did you get this list? If new kani subpackages are later added this script will silently fail to update their version numbers.

If this is a list of every TOML file whose package.name value starts with kani, then I suggest that this program search through the whole source tree for such files, and update all of them.

for ct in pathlib.Path().rglob("Cargo.toml"):
    with open(ct) as handle:
        data = toml.load(handle)
    if "package" not in data or "name" not in data["package"]:
        continue
    if not data["package"]["name"].startswith("kani"):
        continue

    data["package"]["version"] = new_version
    with open(ct, "w") as handle:
        toml.dump(data, handle)

"Cargo.toml",
"cprover_bindings/Cargo.toml",
"kani-compiler/Cargo.toml",
"kani-compiler/kani_queries/Cargo.toml",
"kani-driver/Cargo.toml",
"kani_metadata/Cargo.toml",
"library/kani/Cargo.toml",
"library/kani_macros/Cargo.toml",
"library/std/Cargo.toml",
"tools/build-kani/Cargo.toml",
]
12 changes: 12 additions & 0 deletions scripts/ci/preflight-steps/update-kissat.py
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
#!/usr/bin/python3
# Copyright Kani Contributors
# SPDX-License-Identifier: Apache-2.0 OR MIT
from job_runner import dependencies_links
from dependency_updater import VersionUpdater

# Set the name of the dependency you want to update
kani_dependencies_path = "/Users/jaisnan/kani/kani-dependencies"

if __name__ == "__main__":
updater = VersionUpdater(kani_dependencies_path, dependencies_links["kissat"])
updater.run_process()