Merge remote-tracking branch 'origin/master' into release

Author: rv-auditor

.gitignore

@@ -3,3 +3,4 @@ __pycache__/
 .coverage
 /deps/.stable-mir-json
 /.vscode/
+kmir/src/tests/integration/data/**/target

kmir/src/kmir/cargo.py

@@ -90,6 +90,12 @@ def smir_for_project(self, clean: bool = False) -> SMIRInfo:
 
         messages = [json.loads(line) for line in command_result.stdout.splitlines()]
 
+        if command_result.returncode != 0:
+            _LOGGER.error('Cargo compilation failed!')
+            for msg in [m['message'] for m in messages if m.get('reason') == 'compiler-message']:
+                _LOGGER.error(msg['level'] + '\n' + msg['rendered'])
+            raise Exception('Cargo compilation failed')
+
         artifacts = [
             (Path(message['filenames'][0]), message['target']['kind'][0])
             for message in messages
@@ -100,7 +106,6 @@ def smir_for_project(self, clean: bool = False) -> SMIRInfo:
         exe = None
         for file, kind in artifacts:
             _LOGGER.debug(f'Artifact ({kind}) at ../{file.parent.name}/{file.name}')
-            in_deps = file.parent.name == 'deps'
             if kind == 'bin':
                 # we can only support a single executable at the moment
                 if exe is not None:
@@ -109,14 +114,22 @@ def smir_for_project(self, clean: bool = False) -> SMIRInfo:
                         'Several execuatbles not supported at the moment.'
                     )
                 exe = file.name
-                # executables are in the target directory and do not have a suffix as in `deps`
-                related_files = list((file.parent / 'deps').glob(f'{file.name}*.smir.json'))
-                targets.append(related_files[0])
+                glob = exe.replace('-', '_') + '-*.smir.json'
+                # executables are in the target directory with the crate name and have a hex ID suffix in `deps`
+                location = file.parent / 'deps'
             else:
-                # lib, rlib, dylib, cdylib may be in `deps` or in target and have consistent names
-                name = file.stem.removeprefix('lib') + '.smir.json'
+                # lib, rlib, dylib, cdylib may be in `deps` or in target and have prefix 'lib'
+                in_deps = file.parent.name == 'deps'
                 location = file.parent if in_deps else file.parent / 'deps'
-                targets.append(location / name)
+                # files for lib and rlib require a hex ID suffix unless in `deps`, *.dylib (or *.so) ones don't
+                is_rlib = file.suffix == '.rlib'
+                glob = file.stem.removeprefix('lib') + ('' if in_deps or not is_rlib else '-*') + '.smir.json'
+
+            related_files = list(location.glob(glob))
+            if not related_files:
+                _LOGGER.error('SMIR JSON files not found after building, you must run `cargo clean` and rebuild.')
+                raise FileNotFoundError(f'{location}/{glob}')
+            targets.append(related_files[0])
 
         _LOGGER.debug(f'Files: {targets}')
 

kmir/src/tests/integration/data/crate-tests/single-bin/a_module::twice.expected

@@ -0,0 +1,39 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (42 steps)
+├─ 3 (split)
+│   #expect ( typedValue ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 1
+┃
+┃ (branch)
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     notBool notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 18446744073709551615 ==Int ARG_UINT1:Int +Int ARG_UINT1:Int ==Bool false
+┃  │
+┃  ├─ 4
+┃  │   #expect ( typedValue ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 1
+┃  │
+┃  │  (2 steps)
+┃  └─ 6 (stuck, leaf)
+┃      #ProgramError ( AssertError ( assertMessageOverflow ( binOpAdd , operandCopy ( p
+┃
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 18446744073709551615 ==Int ARG_UINT1:Int +Int ARG_UINT1:Int ==Bool false
+   │
+   ├─ 5
+   │   #expect ( typedValue ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT1:Int &Int 1
+   │
+   │  (21 steps)
+   ├─ 7 (terminal)
+   │   #EndProgram ~> .K
+   │
+   ┊  constraint: true
+   ┊  subst: ...
+   └─ 2 (leaf, target, terminal)
+       #EndProgram ~> .K
+
+
+

kmir/src/tests/integration/data/crate-tests/single-bin/main-crate/Cargo.lock

@@ -0,0 +1,6 @@
+[package]
+name = "single-exe"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

kmir/src/tests/integration/data/crate-tests/single-bin/main-crate/Cargo.toml

@@ -0,0 +1,16 @@
+pub fn add(left: u64, right: u64) -> u64 {
+    left + right
+}
+
+pub mod a_module {
+    use super::add;
+
+    pub fn twice(x: u64) -> u64{
+        add(x, x)
+    }
+}
+
+pub fn main() {
+    let x = 42;
+    assert_eq!(a_module::twice(x), 2 * x);
+}

kmir/src/tests/integration/data/crate-tests/single-bin/main-crate/src/main.rs

@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (219 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│   function: main
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+

kmir/src/tests/integration/data/crate-tests/single-bin/main.expected

@@ -0,0 +1,39 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (34 steps)
+├─ 3 (split)
+│   #expect ( typedValue ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 1
+┃
+┃ (branch)
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     notBool notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709551615 ==Int ARG_UINT1:Int +Int ARG_UINT2:Int ==Bool false
+┃  │
+┃  ├─ 4
+┃  │   #expect ( typedValue ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 1
+┃  │
+┃  │  (2 steps)
+┃  └─ 6 (stuck, leaf)
+┃      #ProgramError ( AssertError ( assertMessageOverflow ( binOpAdd , operandCopy ( p
+┃
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 18446744073709551615 ==Int ARG_UINT1:Int +Int ARG_UINT2:Int ==Bool false
+   │
+   ├─ 5
+   │   #expect ( typedValue ( BoolVal ( notBool ARG_UINT1:Int +Int ARG_UINT2:Int &Int 1
+   │
+   │  (16 steps)
+   ├─ 7 (terminal)
+   │   #EndProgram ~> .K
+   │
+   ┊  constraint: true
+   ┊  subst: ...
+   └─ 2 (leaf, target, terminal)
+       #EndProgram ~> .K
+
+
+

kmir/src/tests/integration/data/crate-tests/single-dylib/add.expected

@@ -0,0 +1,15 @@
+[package]
+name = "small-test-dylib"
+version = "0.1.0"
+edition = "2021"
+
+[lib]
+name = "small_test_dylib"
+path = "src/lib.rs"    # The source file of the target.
+test = false           # Is tested by default.
+doctest = false        # Documentation examples are tested by default.
+bench = false          # Is benchmarked by default.
+doc = false            # Is documented by default.
+crate-type = ["dylib"] # The crate types to generate.
+
+[dependencies]

kmir/src/tests/integration/data/crate-tests/single-dylib/main-crate/Cargo.lock

@@ -0,0 +1,28 @@
+use std::process::exit;
+
+pub fn add(left: u64, right: u64) -> u64 {
+    left + right
+}
+
+fn assume(cond: bool) {
+    if !cond { exit(0); }
+}
+
+// must call test_add_in_range for it to be discovered by linker
+pub fn expose_test() {
+    testing::test_add_in_range(0, 0);
+}
+
+
+
+pub mod testing {
+    use super::*;
+
+    pub fn test_add_in_range(left: u64, right: u64) {
+        let sum = left as u128 + right as u128;
+        assume(sum <= u64::MAX as u128);
+        let result = add(left, right);
+
+        assert_eq!(result as u128, sum)
+    }
+}

kmir/src/tests/integration/data/crate-tests/single-dylib/main-crate/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "small-test-lib"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

kmir/src/tests/integration/data/crate-tests/single-dylib/main-crate/src/lib.rs

@@ -0,0 +1,28 @@
+use std::process::exit;
+
+pub fn add(left: u64, right: u64) -> u64 {
+    left + right
+}
+
+fn assume(cond: bool) {
+    if !cond { exit(0); }
+}
+
+// must call test_add_in_range for it to be discovered by linker
+pub fn expose_test() {
+    testing::test_add_in_range(0, 0);
+}
+
+
+
+pub mod testing {
+    use super::*;
+
+    pub fn test_add_in_range(left: u64, right: u64) {
+        let sum = left as u128 + right as u128;
+        assume(sum <= u64::MAX as u128);
+        let result = add(left, right);
+
+        assert_eq!(result as u128, sum)
+    }
+}

kmir/src/tests/integration/data/crate-tests/single-lib/main-crate/Cargo.lock

@@ -0,0 +1,40 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (112 steps)
+├─ 3 (split)
+│   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
+┃
+┃ (branch)
+┣━━┓ subst: .Subst
+┃  ┃ constraint:
+┃  ┃     notBool ARG_UINT1:Int +Int 340282366920938463463374607431768211456 %Int 340282366920938463463374607431768211456 +Int ARG_UINT2:Int +Int 340282366920938463463374607431768211456 %Int 340282366920938463463374607431768211456 <=Int 18446744073709551615
+┃  │
+┃  ├─ 4
+┃  │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
+┃  │
+┃  │  (4 steps)
+┃  └─ 6 (stuck, leaf)
+┃      #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+┃      span: 72
+┃
+┗━━┓ subst: .Subst
+   ┃ constraint:
+   ┃     ARG_UINT1:Int +Int 340282366920938463463374607431768211456 %Int 340282366920938463463374607431768211456 +Int ARG_UINT2:Int +Int 340282366920938463463374607431768211456 %Int 340282366920938463463374607431768211456 <=Int 18446744073709551615
+   │
+   ├─ 5
+   │   #selectBlock ( switchTargets ( ... branches: branch ( 0 , basicBlockIdx ( 1 ) )
+   │
+   │  (175 steps)
+   ├─ 7 (terminal)
+   │   #EndProgram ~> .K
+   │
+   ┊  constraint: true
+   ┊  subst: ...
+   └─ 2 (leaf, target, terminal)
+       #EndProgram ~> .K
+
+
+

kmir/src/tests/integration/data/crate-tests/single-lib/main-crate/Cargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "crate1"
+version = "0.1.0"
+edition = "2021"
+
+[dependencies]

kmir/src/tests/integration/data/crate-tests/single-lib/main-crate/src/lib.rs

@@ -0,0 +1,38 @@
+pub fn add(left: isize, right: isize) -> isize {
+    left + right
+}
+
+#[derive(Clone, Copy)]
+pub struct MyStruct {
+    pub int_field: isize,
+    pub enum_field: MyEnum,
+    pub option_field: Option<MyEnum> 
+}
+
+impl MyStruct {
+    pub fn new(i: isize, e: Option<MyEnum>) -> Self {
+        let enum_field = e.unwrap_or(MyEnum::Foo);
+        MyStruct { int_field: add(i, 0), enum_field, option_field: e }
+    }
+}
+
+#[derive(Clone, Copy)]
+pub enum MyEnum {
+    Foo,
+    Bar(isize)
+}
+
+impl MyEnum {
+    pub fn default() -> Self { Self::Bar(42) }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn it_works() {
+        let result = add(2, 2);
+        assert_eq!(result, 4);
+    }
+}