diff --git a/nixos/tests/all-tests.nix b/nixos/tests/all-tests.nix index 7aa2dbdbdaf5..2a251331675a 100644 --- a/nixos/tests/all-tests.nix +++ b/nixos/tests/all-tests.nix @@ -1073,6 +1073,7 @@ in open-web-calendar = runTest ./web-apps/open-web-calendar.nix; ocsinventory-agent = handleTestOn [ "x86_64-linux" "aarch64-linux" ] ./ocsinventory-agent.nix { }; orthanc = runTest ./orthanc.nix; + owi = runTest ./owi.nix; owncast = runTest ./owncast.nix; outline = runTest ./outline.nix; i18n = runTest ./i18n.nix; diff --git a/nixos/tests/owi.nix b/nixos/tests/owi.nix new file mode 100644 index 000000000000..74e9d2d394fd --- /dev/null +++ b/nixos/tests/owi.nix @@ -0,0 +1,61 @@ +{ + lib, + pkgs, + ... +}: +{ + name = "owi"; + + meta.maintainers = with lib.maintainers; [ ethancedwards8 ]; + + nodes.machine = { + environment.systemPackages = with pkgs; [ owi ]; + + environment.etc."owipass.rs".source = pkgs.writeText "owi.rs" '' + use owi_sym::Symbolic; + + fn mean_one(x: i32, y: i32) -> i32 { + (x + y)/2 + } + + fn mean_two(x: i32, y: i32) -> i32 { + (y + x)/2 + } + + fn main() { + let x = i32::symbol(); + let y = i32::symbol(); + // proving the commutative property of addition! + owi_sym::assert(mean_one(x, y) == mean_two(x, y)) + } + ''; + + environment.etc."owifail.rs".source = pkgs.writeText "owi.rs" '' + use owi_sym::Symbolic; + + fn mean_wrong(x: i32, y: i32) -> i32 { + (x + y) / 2 + } + + fn mean_correct(x: i32, y: i32) -> i32 { + (x & y) + ((x ^ y) >> 1) + } + + fn main() { + let x = i32::symbol(); + let y = i32::symbol(); + owi_sym::assert(mean_wrong(x, y) == mean_correct(x, y)) + } + ''; + }; + + testScript = + { nodes, ... }: + '' + start_all() + + # testing + machine.succeed("owi rust --fail-on-assertion-only /etc/owipass.rs") + machine.fail("owi rust --fail-on-assertion-only /etc/owifail.rs") + ''; +} diff --git a/pkgs/by-name/ow/owi/package.nix b/pkgs/by-name/ow/owi/package.nix index 18ce88812f6e..9462b2fbde61 100644 --- a/pkgs/by-name/ow/owi/package.nix +++ b/pkgs/by-name/ow/owi/package.nix @@ -7,6 +7,7 @@ zig, makeWrapper, unstableGitUpdater, + nixosTests, }: let @@ -75,7 +76,10 @@ ocamlPackages.buildDunePackage rec { doCheck = false; - passthru.updateScript = unstableGitUpdater { }; + passthru = { + updateScript = unstableGitUpdater { }; + tests = { inherit (nixosTests) owi; }; + }; meta = { description = "Symbolic execution for Wasm, C, C++, Rust and Zig";