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.

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

Fix windows CI builds #1476

Merged
merged 19 commits into from
Dec 5, 2023
Merged
Show file tree
Hide file tree
Changes from 14 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
12 changes: 8 additions & 4 deletions .github/workflows/test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -217,6 +217,7 @@ jobs:
runs-on: ${{ matrix.os }}
env:
PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
COMPILATION_TARGET_PRUSTI: ${{ matrix.os == 'windows-latest' && 'x86_64-pc-windows-msvc' || '' }}
Copy link
Member

Choose a reason for hiding this comment

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

Suggested change
COMPILATION_TARGET_PRUSTI: ${{ matrix.os == 'windows-latest' && 'x86_64-pc-windows-msvc' || '' }}
# Avoid file conflicts when compiling on Windows
# See: https://github.com/viperproject/prusti-dev/pull/1476
COMPILATION_TARGET_PRUSTI: ${{ matrix.os == 'windows-latest' && 'x86_64-pc-windows-msvc' || '' }}

steps:
- name: Check out the repo
uses: actions/checkout@v3
Expand Down Expand Up @@ -249,13 +250,16 @@ jobs:
key: ${{ env.VER_CACHE_KEY_UNIQUE }}
# Restore from the most recent cache that matches a shared prefix of the key
restore-keys: ${{ env.VER_CACHE_KEY_SHARED }}

- name: Build with cargo
run: python x.py build --all --jobs 1
run: python x.py build --all --jobs 1 ${{ matrix.os == 'windows-latest' && '--target x86_64-pc-windows-msvc' || '' }}

- name: Run cargo tests
run: python x.py test --all
run: python x.py test --all ${{ matrix.os == 'windows-latest' && '--target x86_64-pc-windows-msvc' || '' }}

- name: Run a subset of tests with Carbon
run: |
python x.py test pass/no-annotation --all --verbose
python x.py test pass/no-annotation --all --verbose ${{ matrix.os == 'windows-latest' && '--target x86_64-pc-windows-msvc' || '' }}
env:
PRUSTI_VIPER_BACKEND: carbon
- name: Check prusti-contracts
Expand Down Expand Up @@ -296,7 +300,7 @@ jobs:
run: python x.py setup

- name: Build with cargo --release
run: python x.py build --release
run: python x.py build --release ${{ matrix.os == 'windows-latest' && '--target x86_64-pc-windows-msvc' || '' }}

# Run Prusti on itself.
# Disabled because of a bug when compiling jni-gen
Expand Down
1 change: 1 addition & 0 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

1 change: 1 addition & 0 deletions analysis/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ syn = { version = "1.0", features = [ "full", "parsing" ] }
derive_more = "0.99"
prusti-rustc-interface = { path = "../prusti-rustc-interface" }
tracing = { path = "../tracing" }
prusti-utils = { path = "../prusti-utils" }

[dev-dependencies]
compiletest_rs = "0.10"
Expand Down
1 change: 1 addition & 0 deletions analysis/tests/test_accessibility.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
mod utils;

use glob::glob;
use prusti_utils::utils::find_compiled_executable;
use std::{
env,
ffi::OsStr,
Expand Down
1 change: 1 addition & 0 deletions analysis/tests/test_analysis.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ mod utils;

/// Source: https://github.com/rust-lang/miri/blob/master/tests/compiletest.rs
use compiletest_rs as compiletest;
use prusti_utils::utils::find_compiled_executable;
use std::{env, path::PathBuf};
use utils::*;

Expand Down
32 changes: 0 additions & 32 deletions analysis/tests/utils.rs
Original file line number Diff line number Diff line change
@@ -1,35 +1,3 @@
use std::path::PathBuf;

pub fn find_compiled_executable(name: &str) -> PathBuf {
let target_directory = if cfg!(debug_assertions) {
"debug"
} else {
"release"
};
let executable_name = if cfg!(windows) {
format!("{name}.exe")
} else {
name.to_string()
};
let local_driver_path: PathBuf = ["target", target_directory, executable_name.as_str()]
.iter()
.collect();
if local_driver_path.exists() {
return local_driver_path;
}
let workspace_driver_path: PathBuf =
["..", "target", target_directory, executable_name.as_str()]
.iter()
.collect();
if workspace_driver_path.exists() {
return workspace_driver_path;
}
panic!(
"Could not find the {target_directory:?} {executable_name:?} binary to be used in tests. \
It might be that the project has not been compiled correctly."
);
}

pub fn find_sysroot() -> String {
// Taken from https://github.com/Manishearth/rust-clippy/pull/911.
let home = option_env!("RUSTUP_HOME").or(option_env!("MULTIRUST_HOME"));
Expand Down
40 changes: 6 additions & 34 deletions prusti-launch/tests/test_binaries.rs
Original file line number Diff line number Diff line change
Expand Up @@ -5,41 +5,13 @@
// file, You can obtain one at http://mozilla.org/MPL/2.0/.

use glob::glob;
use prusti_utils::utils::find_compiled_executable;
use std::{
io::{BufRead, BufReader},
path::PathBuf,
process::{Child, Command, Stdio},
};

fn find_executable_path(base_name: &str) -> PathBuf {
let target_directory = if cfg!(debug_assertions) {
"debug"
} else {
"release"
};
let executable_name = if cfg!(windows) {
format!("{base_name}.exe")
} else {
base_name.to_string()
};
let local_prusti_rustc_path: PathBuf = ["target", target_directory, &executable_name]
.iter()
.collect();
if local_prusti_rustc_path.exists() {
return local_prusti_rustc_path;
}
let workspace_prusti_rustc_path: PathBuf = ["..", "target", target_directory, &executable_name]
.iter()
.collect();
if workspace_prusti_rustc_path.exists() {
return workspace_prusti_rustc_path;
}
panic!(
"Could not find the {target_directory:?} prusti-rustc binary to be used in tests. \
It might be that Prusti has not been compiled correctly."
);
}

fn run_on_test_files<F: Fn(&PathBuf) -> Command>(run: F) {
let mut num_pass_tests = 0;
let pass_entries = glob("tests/pass/**/*.rs").expect("failed to read glob pattern");
Expand Down Expand Up @@ -107,7 +79,7 @@ impl Drop for ChildGuard {

#[test]
fn test_prusti_rustc() {
let prusti_rustc = find_executable_path("prusti-rustc");
let prusti_rustc = find_compiled_executable("prusti-rustc");

run_on_test_files(|program: &PathBuf| {
let mut cmd = Command::new(&prusti_rustc);
Expand All @@ -121,7 +93,7 @@ fn test_prusti_rustc() {

#[test]
fn test_prusti_rustc_dump() {
let prusti_rustc = find_executable_path("prusti-rustc");
let prusti_rustc = find_compiled_executable("prusti-rustc");

run_on_test_files(|program: &PathBuf| {
let mut cmd = Command::new(&prusti_rustc);
Expand All @@ -146,7 +118,7 @@ fn test_prusti_rustc_dump() {
// so this test fails.
#[test]
fn test_prusti_be_rustc() {
let prusti_rustc = find_executable_path("prusti-rustc");
let prusti_rustc = find_compiled_executable("prusti-rustc");

run_on_test_files(|program: &PathBuf| {
let mut cmd = Command::new(&prusti_rustc);
Expand All @@ -162,8 +134,8 @@ fn test_prusti_be_rustc() {

#[test]
fn test_prusti_rustc_with_server() {
let prusti_rustc = find_executable_path("prusti-rustc");
let prusti_server = find_executable_path("prusti-server");
let prusti_rustc = find_compiled_executable("prusti-rustc");
let prusti_server = find_compiled_executable("prusti-server");

// Preserve SYSTEMROOT on Windows.
// See: https://travis-ci.community/t/socket-the-requested-service-provider-could-not-be-loaded-or-initialized/1127
Expand Down
2 changes: 1 addition & 1 deletion prusti-utils/src/config.rs
Original file line number Diff line number Diff line change
Expand Up @@ -350,7 +350,7 @@ pub fn viper_home() -> String {
if let Some(path) = find_viper_home(&current_executable_dir) {
path.to_str().unwrap().to_owned()
} else {
panic!("Failed to detect Vipe home, please set viper_home configuration flag")
panic!("Failed to detect Viper home, please set viper_home configuration flag")
}
}
}
Expand Down
64 changes: 33 additions & 31 deletions prusti-utils/src/launch/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -26,25 +26,31 @@ pub fn get_current_executable_dir() -> PathBuf {
.to_path_buf()
}

/// Finds the closest `target` directory in the current path.
/// This should be the target directory at the root of the repository,
/// i.e. `prusti-dev/target`.
pub fn get_target_dir(exe_dir: &Path) -> PathBuf {
let mut root_dir = exe_dir;
while root_dir.file_name().unwrap() != "target" {
root_dir = root_dir.parent().unwrap();
}
root_dir.to_path_buf()
}

pub fn get_prusti_contracts_dir(exe_dir: &Path) -> Option<PathBuf> {
let a_prusti_contracts_file = format!("lib{}.rlib", PRUSTI_LIBS[0].replace('-', "_"));
let target_dir = if cfg!(debug_assertions) {
let build_mode = if cfg!(debug_assertions) {
"debug"
} else {
"release"
};

let target_dir = get_target_dir(exe_dir);
let candidates = [
// Libraries in the Prusti artifact will show up here
exe_dir.to_path_buf(),
// Libraries when building Prusti will show up here
exe_dir
.parent()
.unwrap()
.parent()
.unwrap()
.join("target")
.join("verify")
.join(target_dir),
target_dir.join("verify").join(build_mode),
];
candidates
.into_iter()
Expand Down Expand Up @@ -178,28 +184,24 @@ fn get_sysroot_from_rustup() -> Option<PathBuf> {

/// Find Viper home
pub fn find_viper_home(base_dir: &Path) -> Option<PathBuf> {
let candidates = vec![
base_dir.join("viper_tools").join("server"),
base_dir
.join("..")
.join("..")
.join("viper_tools")
.join("server"),
base_dir.join("viper_tools").join("backends"),
base_dir
.join("..")
.join("..")
.join("viper_tools")
.join("backends"),
base_dir
.join("..")
.join("..")
.join("..")
.join("viper_tools")
.join("backends"),
];

candidates.into_iter().find(|candidate| candidate.is_dir())
let mut dir = base_dir;
loop {
if dir.join("viper_tools").is_dir() {
let viper_tools_dir = dir.join("viper_tools");
let backends_dir = viper_tools_dir.join("backends");
if backends_dir.is_dir() {
return Some(backends_dir);
}
let server_dir = viper_tools_dir.join("server");
if server_dir.is_dir() {
return Some(server_dir);
}
}
match dir.parent() {
Some(parent) => dir = parent,
None => return None,
}
}
}

/// Find Z3 executable
Expand Down
52 changes: 52 additions & 0 deletions prusti-utils/src/utils/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,3 +6,55 @@

pub mod identifiers;
pub mod to_string;
use std::{env, path::PathBuf};

pub fn find_compiled_executable(name: &str) -> PathBuf {
let target_directory = if cfg!(debug_assertions) {
"debug"
} else {
"release"
};

let mut target_path = PathBuf::from("target");

// If prusti was compiled for a custom target, e.g. via x.py build --target
// <triple>, then the executables will be placed in /target/<triple>/debug
// rather than /target/debug.

// The environment variable COMPILATION_TARGET_PRUSTI should be set to the
// appropriate triple when running the tests, so that the appropriate
// directory is used.
if let Ok(triple) = env::var("COMPILATION_TARGET_PRUSTI") {
if !triple.is_empty() {
target_path.push(triple);
}
}

target_path.push(target_directory);

let executable_name = if cfg!(windows) {
format!("{name}.exe")
} else {
name.to_string()
};

let mut local_driver_path = target_path.clone();
local_driver_path.push(&executable_name);

if local_driver_path.exists() {
return local_driver_path;
}

let mut workspace_driver_path = PathBuf::from("..");
workspace_driver_path.push(target_path);
workspace_driver_path.push(&executable_name);

if workspace_driver_path.exists() {
return workspace_driver_path;
}

panic!(
"Could not find the {target_directory:?} {executable_name:?} binary to be used in tests. \
It might be that the project has not been compiled correctly."
);
}
Loading