feat: implemented sltu in boolector and z3 (#75) (#80)

- created an integration test for SLTU

examples/test-sltu.c

@@ -0,0 +1,18 @@
+uint64_t main() {
+  uint64_t  a;
+  uint64_t* x;
+
+  a = 40;
+  x = malloc(8);
+
+  read(0, x, 1);
+
+  *x = *x - 47;
+
+  a = *x < a;
+
+  if (a == 1)
+    return 1;
+  else
+    return 0;
+}

src/boolector.rs

@@ -78,6 +78,8 @@ fn traverse<'a>(
                             .and(&traverse(graph, rhs, solver, bvs)),
                         BVOperator::Divu => traverse(graph, lhs, solver, bvs)
                             .udiv(&traverse(graph, rhs, solver, bvs)),
+                        BVOperator::Sltu => traverse(graph, lhs, solver, bvs)
+                            .slt(&traverse(graph, rhs, solver, bvs)),
                         i => unimplemented!("binary operator: {:?}", i),
                     }
                 }

src/z3.rs

@@ -94,6 +94,7 @@ fn traverse<'ctx>(
                 BVOperator::Divu => traverse_binary!(lhs, bvudiv, rhs, graph, ctx, bvs),
                 BVOperator::Equals => traverse_binary!(lhs, _eq, rhs, graph, ctx, bvs),
                 BVOperator::BitwiseAnd => traverse_binary!(lhs, bvand, rhs, graph, ctx, bvs),
+                BVOperator::Sltu => traverse_binary!(lhs, bvslt, rhs, graph, ctx, bvs),
                 i => unimplemented!("binary operator: {:?}", i),
             },
             (lhs, None) => match op {

tests/engine.rs

@@ -4,7 +4,7 @@ use common::{compile_all_riscu, init};
 use monster::engine;
 use rayon::prelude::*;
 
-const TEST_FILES: [&str; 2] = ["/arithmetic.c", "/if-else.c"];
+const TEST_FILES: [&str; 3] = ["/arithmetic.c", "/if-else.c", "/test-sltu.c"];
 
 fn execute_riscu(names: &[&str], solver: engine::Backend) {
     init();