Abstract Core

.github/workflows/general.yml

@@ -0,0 +1,28 @@
+on: pull_request
+
+name: Tests
+
+jobs:
+  tests:
+    name: Check
+    runs-on: ubuntu-latest
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@v2
+
+      - name: Install stable toolchain
+        uses: actions-rs/toolchain@v1
+        with:
+          profile: minimal
+          toolchain: stable
+          override: true
+          components: rustfmt, clippy
+
+      - name: cargo test
+        run: cargo test
+
+      - name: cargo fmt
+        run: cargo fmt --all -- --check
+
+      - name: cargo clippy
+        run: cargo clippy -- -D warnings

Cargo.toml

@@ -7,7 +7,12 @@ authors = ["Tannr Allard <tannr@hey.com>"]
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
-byteorder = "1.4.3"
-hex = "0.4.3"
-thiserror = "1.0.30"
-z3 = "0.11.2"
+symbolic-stack-machines-core = {path = "./core", optional = true}
+symbolic-stack-machines-contrib = {path = "./contrib", optional = true}
+
+[workspace]
+members = ["core", "contrib"]
+
+[features]
+core = ["symbolic-stack-machines-core"]
+full = ["symbolic-stack-machines-core", "symbolic-stack-machines-contrib"]

contrib/Cargo.toml

@@ -0,0 +1,10 @@
+[package]
+name = "symbolic-stack-machines-contrib"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+symbolic-stack-machines-core = {path = "../core"}
+z3 = "0.11.2"

contrib/src/constraints/mod.rs

@@ -0,0 +1 @@
+pub mod z3;

contrib/src/constraints/z3.rs

@@ -0,0 +1,228 @@
+use symbolic_stack_machines_core::constraint::*;
+use symbolic_stack_machines_core::value::Number as AbstractInt;
+use z3::ast::Int;
+use z3::{Config, Context, Model, Solver as Z3InnerSolver};
+
+pub type ValInt = AbstractInt;
+
+pub struct Z3SolverBuilder {
+    ctx: Option<Context>,
+}
+
+impl<'a> Z3SolverBuilder {
+    pub fn new() -> Self {
+        Self { ctx: None }
+    }
+
+    pub fn ctx(mut self, cfg: Option<Config>) -> Self {
+        self.ctx = Some(Context::new(&cfg.unwrap_or_default()));
+        self
+    }
+
+    pub fn build(self) -> Z3Solver<'a> {
+        Z3Solver {
+            inner: None,
+            constraints: vec![],
+            ctx: self.ctx.unwrap(),
+        }
+    }
+}
+pub struct Z3Solver<'a> {
+    inner: Option<Z3InnerSolver<'a>>,
+    constraints: Vec<Constraint>,
+    ctx: Context,
+}
+
+impl<'a> Z3Solver<'a> {
+    pub fn inner(&self) -> &Z3InnerSolver<'a> {
+        assert!(self.inner.is_some());
+        self.inner.as_ref().unwrap()
+    }
+    pub fn get_ctx(&self) -> &'a Context {
+        self.inner().get_context()
+    }
+
+    pub fn get_constraints(&self) -> &Vec<Constraint> {
+        &self.constraints
+    }
+
+    pub fn set_solver(&'a mut self) {
+        self.inner = Some(Z3InnerSolver::new(&self.ctx));
+    }
+}
+
+pub fn z3_int<'a>(i: u64, ctxt: &'a Context) -> z3::ast::Int<'a> {
+    Int::from_u64(ctxt, i)
+}
+
+pub fn z3_int_var<'a>(i: &str, ctxt: &'a Context) -> z3::ast::Int<'a> {
+    Int::new_const(ctxt, i)
+}
+
+impl<'a> Constrained for Z3Solver<'a> {
+    type Model = Model<'a>;
+
+    fn check(&self) -> SatResult<Self::Model> {
+        todo!()
+    }
+}
+
+// impl<'a> Solver<ValInt, Int<'a>> for Z3Solver<'a> {
+//     fn solve(&self) -> SatResult<Self::Model> {
+//         match self.inner().check() {
+//             Z3SatResult::Sat => SatResult::Sat(self.inner().get_model().unwrap()),
+//             Z3SatResult::Unsat => SatResult::Unsat,
+//             Z3SatResult::Unknown => SatResult::Unknown,
+//         }
+//     }
+
+//     fn generic_assert(&mut self, constraint: &Constraint) {
+//         self.inner().assert(&self.transpile(constraint));
+//     }
+// }
+
+// impl<'a> Solver<u64, Int<'a>> for Z3Solver<'a> {
+//     fn solve(&self) -> SatResult<Self::Model> {
+//         match self.inner().check() {
+//             Z3SatResult::Sat => SatResult::Sat(self.inner().get_model().unwrap()),
+//             Z3SatResult::Unsat => SatResult::Unsat,
+//             Z3SatResult::Unknown => SatResult::Unknown,
+//         }
+//     }
+
+//     fn generic_assert(&mut self, constraint: &Constraint) {
+//         self.inner().assert(&self.transpile(constraint));
+//     }
+// }
+
+// TO DO: Generic impl
+
+// impl<'a, T, A> Transpile<T, Bool<'a>, A> for Z3Solver<'a, T>
+// where A: From<T> + Ast<'a>
+// {
+
+// }
+
+// TODO(tannr): Impl Transpile from
+
+// impl<'a> Transpile<u64, Int<'a>> for Z3Solver<'a> {
+//     fn val_to_ground_type(&self, v: u64) -> Int<'a> {
+//         z3_int(v, self.get_ctx())
+//     }
+
+//     fn ground_type_to_val(&self, g: Int<'a>) -> u64 {
+//         g.as_u64().unwrap()
+//     }
+
+//     fn assert(&self, c: Bool<'a>) -> Bool<'a> {
+//         self.inner().assert(&c);
+//         c
+//     }
+
+//     fn and(&self, l: Bool<'a>, r: Bool<'a>) -> Bool<'a> {
+//         z3::ast::Bool::and(l.get_ctx(), &vec![&l, &r])
+//     }
+
+//     fn not(&self, c: Bool<'a>) -> Bool<'a> {
+//         z3::ast::Bool::not(&c)
+//     }
+
+//     fn or(&self, l: Bool<'a>, r: Bool<'a>) -> Bool<'a> {
+//         z3::ast::Bool::or(l.get_ctx(), &vec![&l, &r])
+//     }
+
+//     fn gt(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l.gt(&r)
+//     }
+
+//     fn lt(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l.lt(&r)
+//     }
+
+//     fn lte(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l.le(&r)
+//     }
+
+//     fn gte(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l.ge(&r)
+//     }
+
+//     fn eq(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l._eq(&r)
+//     }
+
+//     fn neq(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         self.not(self.eq(l, r))
+//     }
+
+//     fn true_(&self) -> Bool<'a> {
+//         Bool::from_bool(&self.get_ctx(), true)
+//     }
+
+//     fn false_(&self) -> Bool<'a> {
+//         Bool::from_bool(&self.get_ctx(), false)
+//     }
+// }
+
+// impl<'a> Transpile<Bool<'a>, Int<'a>> for Z3Solver<'a> {
+//     fn val_to_ground_type(&self, v: ValInt) -> Int<'a> {
+//         if let Some(val) = v.inner() {
+//             z3_int(val, self.get_ctx())
+//         } else {
+//             z3_int_var(v.id(), self.get_ctx())
+//         }
+//     }
+
+//     fn ground_type_to_val(&self, g: Int<'a>) -> ValInt {
+//         ValInt::new(g.as_u64().unwrap(), Some(g.to_string()))
+//     }
+
+//     fn assert(&self, c: Bool<'a>) -> Bool<'a> {
+//         self.inner().assert(&c);
+//         c
+//     }
+
+//     fn and(&self, l: Bool<'a>, r: Bool<'a>) -> Bool<'a> {
+//         z3::ast::Bool::and(l.get_ctx(), &vec![&l, &r])
+//     }
+
+//     fn not(&self, c: Bool<'a>) -> Bool<'a> {
+//         z3::ast::Bool::not(&c)
+//     }
+
+//     fn or(&self, l: Bool<'a>, r: Bool<'a>) -> Bool<'a> {
+//         z3::ast::Bool::or(l.get_ctx(), &vec![&l, &r])
+//     }
+
+//     fn gt(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l.gt(&r)
+//     }
+
+//     fn lt(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l.lt(&r)
+//     }
+
+//     fn lte(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l.le(&r)
+//     }
+
+//     fn gte(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l.ge(&r)
+//     }
+
+//     fn eq(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         l._eq(&r)
+//     }
+
+//     fn neq(&self, l: Int<'a>, r: Int<'a>) -> Bool<'a> {
+//         self.not(self.eq(l, r))
+//     }
+
+//     fn true_(&self) -> Bool<'a> {
+//         Bool::from_bool(&self.get_ctx(), true)
+//     }
+
+//     fn false_(&self) -> Bool<'a> {
+//         Bool::from_bool(&self.get_ctx(), false)
+//     }
+// }

contrib/src/instructions/arith.rs

@@ -0,0 +1,60 @@
+use symbolic_stack_machines_core::{
+    environment::Env,
+    instructions::{AbstractExecRecord, AbstractInstruction, InstructionResult},
+    memory::Memory,
+    stack::{Stack, StackOpRecord, StackRecord},
+};
+
+pub struct ADD;
+
+impl AbstractInstruction<AbstractExecRecord> for ADD {
+    fn exec(
+        &self,
+        stack: &Stack,
+        _mem: &Memory,
+        _ext: &Env,
+    ) -> InstructionResult<AbstractExecRecord> {
+        let mut change_log = AbstractExecRecord::default();
+
+        let op_1 = stack.peek(0).unwrap();
+        let op_2 = stack.peek(1).unwrap();
+        let res = *op_1 + *op_2;
+
+        change_log.stack_diff = Some(StackRecord {
+            changed: vec![
+                StackOpRecord::Pop,
+                StackOpRecord::Pop,
+                StackOpRecord::Push(res),
+            ],
+        });
+
+        Ok(change_log)
+    }
+}
+
+pub struct SUB;
+
+impl AbstractInstruction<AbstractExecRecord> for SUB {
+    fn exec(
+        &self,
+        stack: &Stack,
+        _mem: &Memory,
+        _ext: &Env,
+    ) -> InstructionResult<AbstractExecRecord> {
+        let mut change_log = AbstractExecRecord::default();
+
+        let op_1 = stack.peek(0).unwrap();
+        let op_2 = stack.peek(1).unwrap();
+        let res = *op_1 - *op_2;
+
+        change_log.stack_diff = Some(StackRecord {
+            changed: vec![
+                StackOpRecord::Pop,
+                StackOpRecord::Pop,
+                StackOpRecord::Push(res),
+            ],
+        });
+
+        Ok(change_log)
+    }
+}

contrib/src/instructions/bitwise.rs

@@ -0,0 +1,29 @@
+use symbolic_stack_machines_core::{
+    environment::Env,
+    instructions::{AbstractExecRecord, AbstractInstruction, InstructionResult},
+    memory::Memory,
+    stack::{Stack, StackOpRecord, StackRecord, ONE, ZERO},
+};
+
+pub struct ISZERO;
+
+impl AbstractInstruction<AbstractExecRecord> for ISZERO {
+    fn exec(
+        &self,
+        stack: &Stack,
+        _memory: &Memory,
+        _ext: &Env,
+    ) -> InstructionResult<AbstractExecRecord> {
+        let mut change_log = AbstractExecRecord::default();
+
+        let op = stack.peek(0).unwrap();
+
+        let rv = op._eq(&ZERO).ite(ONE, ZERO);
+
+        change_log.stack_diff = Some(StackRecord {
+            changed: vec![StackOpRecord::Pop, StackOpRecord::Push(rv)],
+        });
+
+        Ok(change_log)
+    }
+}