Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add support for more Int types & Refactor files #27

Merged
merged 7 commits into from
Feb 23, 2023
Merged

Add support for more Int types & Refactor files #27

Show file tree
Hide file tree
Changes from 6 commits
Commits
Show all changes
7 commits
Select commit Hold shift + click to select a range
0ead1d2
Update module import and declarations
JustinReiter Feb 22, 2023
3c99df8
Add support for all signed integer types 64 bits and below
JustinReiter Feb 22, 2023
d9924dc
Minor suggested refactoring & expand int type constraints
JustinReiter Feb 22, 2023
ea7a42e
Update tests and clean imports
JustinReiter Feb 22, 2023
e8ea6bd
Update tests for various signed integer types
JustinReiter Feb 23, 2023
55dce23
Update rust compatibility with LLVM for rust 1.60-1.64
JustinReiter Feb 23, 2023
b65c317
Check int type via `is_int_type` function
JustinReiter Feb 23, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,5 @@
/tests/*.ll
/tests/*.bc
/.vscode
/.idea
/tests_temp
11 changes: 10 additions & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ Wombat SymX is a symbolic executor that operates on LLVM IR (specifically, `*.bc

## Setup

Note that LLVM 13+ is required for running the program and for creating `*.bc` LLVM binaries. This is packaged with the latest rust compiler (`rustc +1.60.0`).
Note that LLVM 13 is required for running the program and for creating `*.bc` LLVM binaries. This is packaged with the following rust compilers (`rustc 1.60.*-1.64.*`).

For MAC and Linux, run:
```zsh
Expand Down Expand Up @@ -106,3 +106,12 @@ The path looks like the following:

## Time Wombat SymX
`time cargo run -- <rust_file> test`


# Resources

## LLVM Unsigned vs Signed

LLVM lifts all integers to signed. Intrinsic functions still use unsigned operations while taking signed integers as arguments.

https://stackoverflow.com/questions/14723532/llvms-integer-types
32 changes: 16 additions & 16 deletions src/codegen_basic_block.rs → src/codegen/codegen_basic_block.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,8 +9,8 @@ use inkwell::values::{FunctionValue, InstructionOpcode};
use z3::Solver;
use z3::ast::{Ast, Bool, Int};

use crate::codegen_instruction::codegen_instruction;
use crate::get_var_name::get_var_name;
use crate::codegen::codegen_instruction::codegen_instruction;
use crate::utils::var_utils::get_var_name;
use crate::symbolic_execution::{PANIC_VAR_NAME, COMMON_END_NODE};


Expand All @@ -35,57 +35,57 @@ fn get_basic_block_by_name<'a>(function: &'a FunctionValue, name: &String, names


pub fn is_panic_block(bb: &BasicBlock) -> Option<bool> {
if let Some(terminator) = bb.get_terminator() {
return if let Some(terminator) = bb.get_terminator() {
let opcode = terminator.get_opcode();
match &opcode {
InstructionOpcode::Return => {
return Some(false);
Some(false)
}
InstructionOpcode::Br => {
return Some(false);
Some(false)
}
InstructionOpcode::Switch => {
return Some(false);
Some(false)
}
InstructionOpcode::IndirectBr => {
warn!("Unsure if opcode {:?} implies a panicking block.", opcode);
return None;
None
}
InstructionOpcode::Invoke => {
warn!("Unsure if opcode {:?} implies a panicking block.", opcode);
return None;
None
}
InstructionOpcode::CallBr => {
warn!("Unsure if opcode {:?} implies a panicking block.", opcode);
return None;
None
}
InstructionOpcode::Resume => {
warn!("Unsure if opcode {:?} implies a panicking block.", opcode);
return None;
None
}
InstructionOpcode::CatchSwitch => {
warn!("Unsure if opcode {:?} implies a panicking block.", opcode);
return None;
None
}
InstructionOpcode::CatchRet => {
warn!("Unsure if opcode {:?} implies a panicking block.", opcode);
return None;
None
}
InstructionOpcode::CleanupRet => {
warn!("Unsure if opcode {:?} implies a panicking block.", opcode);
return None;
None
}
InstructionOpcode::Unreachable => {
return Some(true);
Some(true)
}
_ => {
warn!("Opcode {:?} is not supported as a terminator for panic detection", opcode);
return None;
None
}
}
} else {
warn!("\tNo terminator found for panic detection");
return None;
None
}
}

Expand Down
124 changes: 23 additions & 101 deletions src/codegen_call.rs → src/codegen/codegen_call.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,10 @@ use inkwell::values::{InstructionValue};
use z3::Solver;
use z3::ast::{Ast, Bool, Int};

use crate::codegen_function::codegen_function;
use crate::codegen::codegen_function::codegen_function;
use crate::control_flow_graph::forward_topological_sort;
use crate::function_utils::{get_function_name, get_function_by_name};
use crate::get_var_name::get_var_name;
use crate::utils::function_utils::{get_function_name, get_function_by_name};
use crate::utils::var_utils::{get_min_max_signed_int, get_var_name};
use crate::symbolic_execution::get_module_name_from_file_name;

fn codegen_general_call<'a>(
Expand Down Expand Up @@ -67,7 +67,7 @@ fn codegen_general_call<'a>(
let assignment = lvalue._eq(&rvalue);
node_var = assignment.implies(&node_var);
} else {
warn!("Currently unsuppported type {:?} for input parameter to {}", input.get_type().to_string(), call_operation_name_string);
warn!("Currently unsupported type {:?} for input parameter to {}", input.get_type().to_string(), call_operation_name_string);
}
}

Expand All @@ -94,37 +94,11 @@ pub fn codegen_call<'a>(
}

match call_operation_name_str {
"llvm.sadd.with.overflow.i32" => {
let operand1_name = get_var_name(
&instruction.get_operand(0).unwrap().left().unwrap(),
&solver,
namespace
);
let operand2_name = get_var_name(
&instruction.get_operand(1).unwrap().left().unwrap(),
&solver,
namespace
);
s if s.starts_with("llvm.sadd.with.overflow.i") => {
// Translate the intrinsic integer size to an i64 representing the min/max representable numbers
let s_size = &s[25..];
wu-benjamin marked this conversation as resolved.
Show resolved Hide resolved
let (min_int_val, max_int_val) = get_min_max_signed_int(s_size);

let lvalue_var_name_1 = format!("{}.0", get_var_name(&instruction, &solver, namespace));
let lvalue_var_1 = Int::new_const(solver.get_context(), lvalue_var_name_1);
let rvalue_var_1 = Int::add(solver.get_context(), &[
&Int::new_const(solver.get_context(), operand1_name),
&Int::new_const(solver.get_context(), operand2_name)
]);

let assignment_1 = lvalue_var_1._eq(&rvalue_var_1);

let lvalue_var_name_2 = format!("{}.1", get_var_name(&instruction, &solver, namespace));
let min_int = Int::from_i64(solver.get_context(), i32::MIN.into());
let max_int = Int::from_i64(solver.get_context(), i32::MAX.into());
let rvalue_var_2 = Bool::or(solver.get_context(), &[&rvalue_var_1.gt(&max_int), &rvalue_var_1.lt(&min_int)]);

let assignment_2 = Bool::new_const(solver.get_context(), lvalue_var_name_2)._eq(&rvalue_var_2);
let assignment = Bool::and(solver.get_context(), &[&assignment_1, &assignment_2]);
node_var = assignment.implies(&node_var);
}
"llvm.sadd.with.overflow.i64" => {
let operand1_name = get_var_name(
&instruction.get_operand(0).unwrap().left().unwrap(),
&solver,
Expand All @@ -146,45 +120,19 @@ pub fn codegen_call<'a>(
let assignment_1 = lvalue_var_1._eq(&rvalue_var_1);

let lvalue_var_name_2 = format!("{}.1", get_var_name(&instruction, &solver, namespace));
let min_int = Int::from_i64(solver.get_context(), i64::MIN);
let max_int = Int::from_i64(solver.get_context(), i64::MAX);
let min_int = Int::from_i64(solver.get_context(), min_int_val);
let max_int = Int::from_i64(solver.get_context(), max_int_val);
let rvalue_var_2 = Bool::or(solver.get_context(), &[&rvalue_var_1.gt(&max_int), &rvalue_var_1.lt(&min_int)]);

let assignment_2 = Bool::new_const(solver.get_context(), lvalue_var_name_2)._eq(&rvalue_var_2);
let assignment = Bool::and(solver.get_context(), &[&assignment_1, &assignment_2]);
node_var = assignment.implies(&node_var);
}
"llvm.ssub.with.overflow.i32" => {
let operand1_name = get_var_name(
&instruction.get_operand(0).unwrap().left().unwrap(),
&solver,
namespace
);
let operand2_name = get_var_name(
&instruction.get_operand(1).unwrap().left().unwrap(),
&solver,
namespace
);

let lvalue_var_name_1 = format!("{}.0", get_var_name(&instruction, &solver, namespace));
let lvalue_var_1 = Int::new_const(solver.get_context(), lvalue_var_name_1);
let rvalue_var_1 = Int::sub(solver.get_context(), &[
&Int::new_const(solver.get_context(), operand1_name),
&Int::new_const(solver.get_context(), operand2_name)
]);

let assignment_1 = lvalue_var_1._eq(&rvalue_var_1);
s if s.starts_with("llvm.ssub.with.overflow.i") => {
// Translate the intrinsic integer size to an i64 representing the min/max representable numbers
let s_size = &s[25..];
let (min_int_val, max_int_val) = get_min_max_signed_int(s_size);

let lvalue_var_name_2 = format!("{}.1", get_var_name(&instruction, &solver, namespace));
let min_int = Int::from_i64(solver.get_context(), i32::MIN.into());
let max_int = Int::from_i64(solver.get_context(), i32::MAX.into());
let rvalue_var_2 = Bool::or(solver.get_context(), &[&rvalue_var_1.gt(&max_int), &rvalue_var_1.lt(&min_int)]);

let assignment_2 = Bool::new_const(solver.get_context(), lvalue_var_name_2)._eq(&rvalue_var_2);
let assignment = Bool::and(solver.get_context(), &[&assignment_1, &assignment_2]);
node_var = assignment.implies(&node_var);
}
"llvm.ssub.with.overflow.i64" => {
let operand1_name = get_var_name(
&instruction.get_operand(0).unwrap().left().unwrap(),
&solver,
Expand All @@ -206,45 +154,19 @@ pub fn codegen_call<'a>(
let assignment_1 = lvalue_var_1._eq(&rvalue_var_1);

let lvalue_var_name_2 = format!("{}.1", get_var_name(&instruction, &solver, namespace));
let min_int = Int::from_i64(solver.get_context(), i64::MIN);
let max_int = Int::from_i64(solver.get_context(), i64::MAX);
let min_int = Int::from_i64(solver.get_context(), min_int_val);
let max_int = Int::from_i64(solver.get_context(), max_int_val);
let rvalue_var_2 = Bool::or(solver.get_context(), &[&rvalue_var_1.gt(&max_int), &rvalue_var_1.lt(&min_int)]);

let assignment_2 = Bool::new_const(solver.get_context(), lvalue_var_name_2)._eq(&rvalue_var_2);
let assignment = Bool::and(solver.get_context(), &[&assignment_1, &assignment_2]);
node_var = assignment.implies(&node_var);
}
"llvm.smul.with.overflow.i32" => {
let operand1_name = get_var_name(
&instruction.get_operand(0).unwrap().left().unwrap(),
&solver,
namespace
);
let operand2_name = get_var_name(
&instruction.get_operand(1).unwrap().left().unwrap(),
&solver,
namespace
);
s if s.starts_with("llvm.smul.with.overflow.i") => {
// Translate the intrinsic integer size to an i64 representing the min/max representable numbers
let s_size = &s[25..];
let (min_int_val, max_int_val) = get_min_max_signed_int(s_size);

let lvalue_var_name_1 = format!("{}.0", get_var_name(&instruction, &solver, namespace));
let lvalue_var_1 = Int::new_const(solver.get_context(), lvalue_var_name_1);
let rvalue_var_1 = Int::mul(solver.get_context(), &[
&Int::new_const(solver.get_context(), operand1_name),
&Int::new_const(solver.get_context(), operand2_name)
]);

let assignment_1 = lvalue_var_1._eq(&rvalue_var_1);

let lvalue_var_name_2 = format!("{}.1", get_var_name(&instruction, &solver, namespace));
let min_int = Int::from_i64(solver.get_context(), i32::MIN.into());
let max_int = Int::from_i64(solver.get_context(), i32::MAX.into());
let rvalue_var_2 = Bool::or(solver.get_context(), &[&rvalue_var_1.gt(&max_int), &rvalue_var_1.lt(&min_int)]);

let assignment_2 = Bool::new_const(solver.get_context(), lvalue_var_name_2)._eq(&rvalue_var_2);
let assignment = Bool::and(solver.get_context(), &[&assignment_1, &assignment_2]);
node_var = assignment.implies(&node_var);
}
"llvm.smul.with.overflow.i64" => {
let operand1_name = get_var_name(
&instruction.get_operand(0).unwrap().left().unwrap(),
&solver,
Expand All @@ -266,8 +188,8 @@ pub fn codegen_call<'a>(
let assignment_1 = lvalue_var_1._eq(&rvalue_var_1);

let lvalue_var_name_2 = format!("{}.1", get_var_name(&instruction, &solver, namespace));
let min_int = Int::from_i64(solver.get_context(), i64::MIN);
let max_int = Int::from_i64(solver.get_context(), i64::MAX);
let min_int = Int::from_i64(solver.get_context(), min_int_val);
let max_int = Int::from_i64(solver.get_context(), max_int_val);
let rvalue_var_2 = Bool::or(solver.get_context(), &[&rvalue_var_1.gt(&max_int), &rvalue_var_1.lt(&min_int)]);

let assignment_2 = Bool::new_const(solver.get_context(), lvalue_var_name_2)._eq(&rvalue_var_2);
Expand All @@ -294,7 +216,7 @@ pub fn codegen_call<'a>(
let assignment = Bool::new_const(solver.get_context(), lvalue_var_name)._eq(&rvalue_var);
node_var = assignment.implies(&node_var);
}
"core::panicking::panic::he60bb304466ccbaf" => {
s if s.starts_with("core::panicking::panic") => {
// NO-OP
}
_ => {
Expand Down
4 changes: 2 additions & 2 deletions src/codegen_function.rs → src/codegen/codegen_function.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,9 @@ use inkwell::values::{FunctionValue};

use z3::Solver;

use crate::codegen_basic_block::codegen_basic_block;
use crate::codegen::codegen_basic_block::codegen_basic_block;
use crate::control_flow_graph::{get_forward_edges, get_backward_edges, backward_topological_sort};
use crate::pretty_print::pretty_print_function;
use crate::utils::pretty_print::pretty_print_function;


pub fn codegen_function(module: &InkwellModule, function: &FunctionValue, solver: &Solver, namespace: &str, call_stack: &str, return_target_node: &str, return_register: &str) -> () {
Expand Down
Loading