Unverified Commit 3e1ac8bc authored by Ethan Carter Edwards's avatar Ethan Carter Edwards
Browse files

nixos/tests/owi: init

parent 827846a2
Loading
Loading
Loading
Loading
+1 −0
Original line number Diff line number Diff line
@@ -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;

nixos/tests/owi.nix

0 → 100644
+61 −0
Original line number Diff line number Diff line
{
  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")
    '';
}
+5 −1
Original line number Diff line number Diff line
@@ -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";