Skip to content

Commit

Permalink
feat: some stubs for (ternary) bit vectors (#9)
Browse files Browse the repository at this point in the history
  • Loading branch information
ChristianMoesl committed Nov 17, 2020
1 parent f841014 commit b89220d
Show file tree
Hide file tree
Showing 6 changed files with 80 additions and 3 deletions.
3 changes: 1 addition & 2 deletions Cargo.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

2 changes: 1 addition & 1 deletion Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ description = "Monster is a symbolic execution engine for 64-bit RISC-V code"
goblin = "0.2"
byteorder = "1.3.4"
clap = "3.0.0-beta.1"
riscv-decode = "0.2.0"
riscv-decode = { git = "https://github.com/cksystemsgroup/riscv-decode" }
petgraph = "0.5.1"

[dev-dependencies]
Expand Down
11 changes: 11 additions & 0 deletions src/bitvec.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
pub struct BitVector {
pub(crate) value: u64,
}

impl BitVector {
#[allow(dead_code)]
fn new(value: u64) -> Self {
BitVector { value }
}
}
39 changes: 39 additions & 0 deletions src/engine.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
use crate::ternary::TernaryBitVector;

struct Machine {
#[allow(dead_code)]
regs: [TernaryBitVector; 32],
}

impl Machine {
#[allow(dead_code)]
fn new() -> Self {
Machine {
regs: [TernaryBitVector::new(0, u64::max_value()); 32],
}
}
}

// fn has_inv_value_for_addi(raw: IType) -> bool {
// true
// }

#[cfg(test)]
mod tests {
use super::*;
use riscv_decode::types::*;
use riscv_decode::Instruction;

#[test]
fn can_find_input_for_addi() {
let machine = Machine::new();

let raw = IType(0);
let _addi = Instruction::Addi(raw);

let _rd = raw.rd();
let _rs1_value = machine.regs[raw.rs1() as usize];

let _s = raw.imm();
}
}
3 changes: 3 additions & 0 deletions src/main.rs
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,14 @@ use clap::{App, Arg};
use std::fmt::Display;
use std::path::Path;

mod bitvec;
mod cfg;
mod compile;
mod decode;
mod disassemble;
mod elf;
mod engine;
mod ternary;

use compile::compile_example;
use disassemble::disassemble_riscu;
Expand Down
25 changes: 25 additions & 0 deletions src/ternary.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
use crate::bitvec::BitVector;

#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
pub struct TernaryBitVector {
xlo: u64,
xhi: u64,
}

impl TernaryBitVector {
pub fn new(xlo: u64, xhi: u64) -> Self {
assert!(Self::valid(xlo, xhi), "is not a valid ternary bit vector");
Self { xlo, xhi }
}

/// verifies that these two values can form a valid ternary bit vector
pub fn valid(xlo: u64, xhi: u64) -> bool {
!xlo | xhi == u64::max_value()
}

/// verifies that all constant bits of a ternary bit vector match a bit vector
#[allow(dead_code)]
pub fn mcb(&self, other: &BitVector) -> bool {
(self.xhi & other.value == other.value) && (self.xlo | other.value == other.value)
}
}

0 comments on commit b89220d

Please sign in to comment.