From 9fa61d0517580124c8c32a21899aa067cc4994bc Mon Sep 17 00:00:00 2001 From: alexanderlackner <43965864+alexanderlackner@users.noreply.github.com> Date: Thu, 3 Sep 2020 17:08:07 +0200 Subject: [PATCH] fix: constraints are now properly displayed in data-flow graphs --- src/formula_graph.rs | 86 ++++++++++++++++++++++--- symbolic/simple-if-else-symbolic-exit.c | 34 ++++++++++ 2 files changed, 110 insertions(+), 10 deletions(-) create mode 100644 symbolic/simple-if-else-symbolic-exit.c diff --git a/src/formula_graph.rs b/src/formula_graph.rs index 6e20bee8..69ce513f 100644 --- a/src/formula_graph.rs +++ b/src/formula_graph.rs @@ -117,10 +117,21 @@ impl fmt::Debug for Input { #[derive(Clone, Eq, Hash, PartialEq)] pub enum BooleanFunction { - // Equals, + NotEqual, + Equals, GreaterThan, } +impl fmt::Display for BooleanFunction { + fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result { + match *self { + BooleanFunction::GreaterThan => write!(f, "Greater Than"), + BooleanFunction::Equals => write!(f, "Equal"), + BooleanFunction::NotEqual => write!(f, "Not Equal"), + } + } +} + #[derive(Clone, Eq, Hash, PartialEq)] pub struct Constrain { // has 1 input edge only and 0 output edges @@ -136,7 +147,7 @@ impl Constrain { impl fmt::Debug for Constrain { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - write!(f, "{}", self.name) + write!(f, "{}, {}", self.name, self.op) } } @@ -161,15 +172,17 @@ struct DataFlowGraphBuilder<'a> { program_break: u64, regs: [Value; 32], memory: Vec, + branch_decisions: Vec, } impl<'a> DataFlowGraphBuilder<'a> { - // creates a machine state with a specifc memory size + // creates a machine state with a specific memory size fn new( memory_size: usize, path: &'a [Instruction], data_segment: &[u8], elf_metadata: ElfMetadata, + branch_decisions: Vec, ) -> Self { let mut regs = [Value::Concrete(0); 32]; let mut memory = vec![Value::Uninitialized; memory_size / 8]; @@ -197,6 +210,7 @@ impl<'a> DataFlowGraphBuilder<'a> { path, regs, memory, + branch_decisions, } } @@ -389,6 +403,51 @@ impl<'a> DataFlowGraphBuilder<'a> { None } + fn execute_beq(&mut self, btype: BType) -> Option { + let node; + if self.branch_decisions.remove(0) { + node = Node::Constrain(Constrain::new(String::from("beq"), BooleanFunction::Equals)); + } else { + node = Node::Constrain(Constrain::new( + String::from("beq"), + BooleanFunction::NotEqual, + )); + } + let node_idx = self.graph.add_node(node); + let lhs = self.regs[btype.rs1() as usize]; + let rhs = self.regs[btype.rs2() as usize]; + + println!("{:?}", lhs); + println!("{:?}", rhs); + + match (lhs, rhs) { + (Value::Concrete(v1), Value::Concrete(v2)) => { + let const_node1 = self.create_const_node(v1); + let const_node2 = self.create_const_node(v2); + self.graph + .add_edge(const_node1, node_idx, ArgumentSide::Lhs); + self.graph + .add_edge(const_node2, node_idx, ArgumentSide::Rhs); + } + (Value::Symbolic(v1), Value::Concrete(v2)) => { + let const_node = self.create_const_node(v2); + self.graph.add_edge(v1, node_idx, ArgumentSide::Lhs); + self.graph.add_edge(const_node, node_idx, ArgumentSide::Rhs); + } + (Value::Concrete(v1), Value::Symbolic(v2)) => { + let const_node = self.create_const_node(v1); + self.graph.add_edge(const_node, node_idx, ArgumentSide::Lhs); + self.graph.add_edge(v2, node_idx, ArgumentSide::Rhs); + } + (Value::Symbolic(v1), Value::Symbolic(v2)) => { + self.graph.add_edge(v1, node_idx, ArgumentSide::Lhs); + self.graph.add_edge(v2, node_idx, ArgumentSide::Rhs); + } + _ => panic!("access to uninitialized memory"), + } + None + } + fn execute_exit(&mut self) -> Option { if let Value::Symbolic(exit_code) = self.regs[REG_A0] { let const_node = Node::Constant(Const::new(0)); @@ -505,7 +564,7 @@ impl<'a> DataFlowGraphBuilder<'a> { } None } - Instruction::Beq(_btype) => None, + Instruction::Beq(btype) => self.execute_beq(btype), _ => unimplemented!("can not handle this instruction"), } } @@ -535,8 +594,10 @@ fn build_dataflow_graph( path: &[Instruction], data_segment: &[u8], elf_metadata: ElfMetadata, + branch_decision: Vec, ) -> Option<(Formula, NodeIndex)> { - DataFlowGraphBuilder::new(1000000, path, data_segment, elf_metadata).generate_graph() + DataFlowGraphBuilder::new(1000000, path, data_segment, elf_metadata, branch_decision) + .generate_graph() } // TODO: need to load data segment => then write test @@ -611,12 +672,12 @@ mod tests { .arg("cksystemsteaching/selfie") .arg("/opt/selfie/selfie") .arg("-c") - .arg("/opt/monster/symbolic/symbolic-exit.c") + .arg("/opt/monster/symbolic/simple-if-else-symbolic-exit.c") .arg("-o") - .arg("/opt/monster/symbolic/symbolic-exit.riscu.o") + .arg("/opt/monster/symbolic/simple-if-else-symbolic-exit.riscu.o") .output(); - let test_file = Path::new("symbolic/symbolic-exit.riscu.o"); + let test_file = Path::new("symbolic/simple-if-else-symbolic-exit.riscu.o"); let (graph, data_segment, elf_metadata) = cfg::build_from_file(test_file).unwrap(); @@ -626,8 +687,13 @@ mod tests { println!("{:?}", path); - let (formula, _root) = - build_dataflow_graph(&path, data_segment.as_slice(), elf_metadata).unwrap(); + let (formula, _root) = build_dataflow_graph( + &path, + data_segment.as_slice(), + elf_metadata, + _branch_decisions, + ) + .unwrap(); let graph_wo_dc = eliminate_dead_code(&formula, _root); diff --git a/symbolic/simple-if-else-symbolic-exit.c b/symbolic/simple-if-else-symbolic-exit.c new file mode 100644 index 00000000..37c761b7 --- /dev/null +++ b/symbolic/simple-if-else-symbolic-exit.c @@ -0,0 +1,34 @@ +/* +The purpose of this code is to demonstrate the capabilities +of the monster model generator of selfie. Monster translates +the code to an SMT-LIB or BTOR2 formula that is satisfiable +if and only if the code exits with a non-zero exit code, or +performs division by zero or invalid/unsafe memory accesses. + +This code is exactly the same as simple-if-else-1-35.c but with symbolic exit codes. +This is necessary since we only support symbolic exit codes so far. + +Input == #b00110001 (== 49 == '1') +*/ + +uint64_t main() { + uint64_t a; + uint64_t* x; + + a = 40; + x = malloc(8); + + read(0, x, 1); + + *x = *x - 47; + + if (*x == 2) + a = a + *x; + else + a = a + (*x * 0); + + if (a == 42) + return a; + else + return *x; +} \ No newline at end of file