use crossbeam::queue::SegQueue;
use sha2::{Digest, Sha256};
use std::convert::TryInto;
use std::process::exit;
use std::sync::Arc;
use std::time::Instant;
use isla_axiomatic::footprint_analysis::footprint_analysis;
use isla_axiomatic::litmus::assemble_instruction;
use isla_axiomatic::page_table::{PageTables, S1PageAttrs, S2PageAttrs};
use isla_lib::bitvector::{b129::B129, BV};
use isla_lib::executor;
use isla_lib::executor::{LocalFrame, TaskState};
use isla_lib::init::{initialize_architecture, Initialized};
use isla_lib::ir::*;
use isla_lib::memory::{Memory, Region};
use isla_lib::smt::{EvPath, Event};
use isla_lib::zencode;
use isla_lib::{simplify, simplify::WriteOpts};
mod opts;
use opts::CommonOpts;
fn main() {
let code = isla_main();
unsafe { isla_lib::smt::finalize_solver() };
exit(code)
}
pub fn hex_bytes(s: &str) -> Result<Vec<u8>, std::num::ParseIntError> {
(0..s.len()).step_by(2).map(|i| u8::from_str_radix(&s[i..i + 2], 16)).collect()
}
fn isla_main() -> i32 {
let mut opts = opts::common_opts();
opts.reqopt("i", "instruction", "display footprint of instruction", "<instruction>");
opts.optopt("e", "endianness", "instruction encoding endianness (default: little)", "big/little");
opts.optflag("d", "dependency", "view instruction dependency info");
opts.optflag("x", "hex", "parse instruction as hexadecimal opcode, rather than assembly");
opts.optflag("s", "simplify", "simplify instruction footprint");
opts.optopt("f", "function", "use a custom footprint function", "<identifer>");
opts.optflag("c", "continue-on-error", "continue generating traces upon encountering an error");
opts.optmulti("", "identity-map", "set up an identity mapping for the provided address", "<address>");
let mut hasher = Sha256::new();
let (matches, arch) = opts::parse(&mut hasher, &opts);
let CommonOpts { num_threads, mut arch, symtab, isa_config } =
opts::parse_with_arch(&mut hasher, &opts, &matches, &arch);
let Initialized { regs, lets, shared_state } =
initialize_architecture(&mut arch, symtab, &isa_config, AssertionMode::Optimistic);
let little_endian = match matches.opt_str("endianness").as_deref() {
Some("little") | None => true,
Some("big") => false,
Some(_) => {
eprintln!("--endianness argument must be one of either `big` or `little`");
exit(1)
}
};
let instruction = matches.opt_str("instruction").unwrap();
let opcode = if matches.opt_present("hex") {
match hex_bytes(&instruction) {
Ok(opcode) => opcode,
Err(e) => {
eprintln!("Could not parse hexadecimal opcode: {}", e);
exit(1)
}
}
} else {
match assemble_instruction(&instruction, &isa_config) {
Ok(opcode) => opcode,
Err(msg) => {
eprintln!("{}", msg);
return 1;
}
}
};
if opcode.len() > 8 {
eprintln!("Currently instructions greater than 8 bytes in length are not supported");
return 1;
}
let opcode = if opcode.len() == 2 {
let opcode: Box<[u8; 2]> = opcode.into_boxed_slice().try_into().unwrap();
B129::from_u16(if little_endian { u16::from_le_bytes(*opcode) } else { u16::from_be_bytes(*opcode) })
} else if opcode.len() == 4 {
let opcode: Box<[u8; 4]> = opcode.into_boxed_slice().try_into().unwrap();
B129::from_u32(if little_endian { u32::from_le_bytes(*opcode) } else { u32::from_be_bytes(*opcode) })
} else {
B129::from_bytes(&opcode)
};
eprintln!("opcode: {}", opcode);
let mut memory = Memory::new();
let mut s1_tables = PageTables::new("stage 1", isa_config.page_table_base);
let mut s2_tables = PageTables::new("stage 2", isa_config.s2_page_table_base);
let s1_level0 = s1_tables.alloc();
let s2_level0 = s2_tables.alloc();
matches.opt_strs("identity-map").iter().for_each(|addr| {
if let Some(addr) = B129::from_str(addr) {
s1_tables.identity_map(s1_level0, addr.lower_u64(), S1PageAttrs::default());
s2_tables.identity_map(s2_level0, addr.lower_u64(), S2PageAttrs::default());
} else {
eprintln!("Could not parse address {} in --identity-map argument", addr);
exit(1)
}
});
let mut page = isa_config.page_table_base;
while page < s1_tables.range().end {
s2_tables.identity_map(s2_level0, page, S2PageAttrs::default());
page += isa_config.page_size
}
memory.add_region(Region::Custom(s1_tables.range(), Box::new(s1_tables.freeze())));
memory.add_region(Region::Custom(s2_tables.range(), Box::new(s2_tables.freeze())));
memory.add_zero_region(0x0..0xffff_ffff_ffff_ffff);
let footprint_function = match matches.opt_str("function") {
Some(id) => zencode::encode(&id),
None => "zisla_footprint".to_string(),
};
let function_id = shared_state.symtab.lookup(&footprint_function);
let (args, _, instrs) = shared_state.functions.get(&function_id).unwrap();
let task_state = TaskState::new();
let task = LocalFrame::new(function_id, args, Some(&[Val::Bits(opcode)]), instrs)
.add_lets(&lets)
.add_regs(®s)
.set_memory(memory)
.task(0, &task_state);
let queue = Arc::new(SegQueue::new());
let now = Instant::now();
executor::start_multi(num_threads, None, vec![task], &shared_state, queue.clone(), &executor::trace_collector);
eprintln!("Execution took: {}ms", now.elapsed().as_millis());
let mut paths = Vec::new();
let rk_ifetch = shared_state.enum_member(isa_config.ifetch_read_kind).expect("Invalid ifetch read kind");
loop {
match queue.pop() {
Ok(Ok((_, mut events))) if matches.opt_present("dependency") => {
let mut events: EvPath<B129> = events
.drain(..)
.rev()
.filter(|ev| {
(ev.is_memory() && !ev.has_read_kind(rk_ifetch))
|| ev.is_smt()
|| ev.is_instr()
|| ev.is_cycle()
|| ev.is_write_reg()
})
.collect();
simplify::remove_unused(&mut events);
paths.push(events)
}
Ok(Ok((_, mut events))) => {
if matches.opt_present("simplify") {
simplify::hide_initialization(&mut events);
simplify::remove_unused(&mut events);
simplify::propagate_forwards_used_once(&mut events);
simplify::commute_extract(&mut events);
simplify::eval(&mut events);
}
let events: Vec<Event<B129>> = events.drain(..).rev().collect();
let stdout = std::io::stdout();
let mut handle = stdout.lock();
let write_opts = WriteOpts { define_enum: !matches.opt_present("simplify"), ..WriteOpts::default() };
simplify::write_events_with_opts(&mut handle, &events, &shared_state.symtab, &write_opts).unwrap();
}
Ok(Err(msg)) => {
eprintln!("{}", msg);
if !matches.opt_present("continue-on-error") {
return 1;
}
}
Err(_) => break,
}
}
if matches.opt_present("dependency") {
match footprint_analysis(num_threads, &[paths], &lets, ®s, &shared_state, &isa_config, None) {
Ok(footprints) => {
for (_, footprint) in footprints {
{
let stdout = std::io::stdout();
let mut handle = stdout.lock();
let _ = footprint.pretty(&mut handle, &shared_state.symtab);
}
}
}
Err(footprint_error) => {
eprintln!("{:?}", footprint_error);
return 1;
}
}
}
0
}