diff --git a/isla-axiomatic/src/footprint_analysis.rs b/isla-axiomatic/src/footprint_analysis.rs index fa7d369..74a94c3 100644 --- a/isla-axiomatic/src/footprint_analysis.rs +++ b/isla-axiomatic/src/footprint_analysis.rs @@ -50,7 +50,7 @@ use std::time::Instant; use isla_lib::bitvector::BV; use isla_lib::cache::{Cacheable, Cachekey}; use isla_lib::executor; -use isla_lib::executor::{LocalFrame, TaskState, TraceError}; +use isla_lib::executor::{LocalFrame, TaskId, TaskState, TraceError}; use isla_lib::ir::*; use isla_lib::log; use isla_lib::simplify::{EventReferences, Taints}; @@ -511,7 +511,7 @@ where LocalFrame::new(function_id, args, ret_ty, Some(&[Val::Bits(*opcode)]), instrs) .add_lets(arch.lets) .add_regs(arch.regs) - .task(i, &task_state), + .task(TaskId::from_usize(i), &task_state), ) }) .unzip(); @@ -542,7 +542,7 @@ where .collect(); isla_lib::simplify::remove_unused(&mut events); - footprint_buckets[task_id].push(events) + footprint_buckets[task_id.as_usize()].push(events) } // Error during execution Some(Err(err)) => return Err(FootprintError::Trace(err)), diff --git a/isla-axiomatic/src/run_litmus.rs b/isla-axiomatic/src/run_litmus.rs index d4a8573..5ce842f 100644 --- a/isla-axiomatic/src/run_litmus.rs +++ b/isla-axiomatic/src/run_litmus.rs @@ -43,7 +43,7 @@ use std::time::Instant; use isla_lib::bitvector::BV; use isla_lib::error::{ExecError, IslaError}; use isla_lib::executor; -use isla_lib::executor::{LocalFrame, TaskState, TraceError}; +use isla_lib::executor::{LocalFrame, TaskId, TaskState, TraceError}; use isla_lib::ir::*; use isla_lib::memory::Memory; use isla_lib::simplify; @@ -307,7 +307,7 @@ where .add_lets(&lets) .add_regs(®s) .set_memory(memory.clone()) - .task_with_checkpoint(i, &task_states[i], initial_checkpoint.clone()) + .task_with_checkpoint(TaskId::from_usize(i), &task_states[i], initial_checkpoint.clone()) } Thread::IR(thread) => { let (args, ret_ty, instrs) = shared_state.functions.get(&thread.call).unwrap(); @@ -315,7 +315,7 @@ where .add_lets(&lets) .add_regs(®s) .set_memory(memory.clone()) - .task_with_checkpoint(i, &task_states[i], initial_checkpoint.clone()) + .task_with_checkpoint(TaskId::from_usize(i), &task_states[i], initial_checkpoint.clone()) } } }) @@ -344,10 +344,10 @@ where simplify::remove_unused(&mut events); for event in events.iter_mut() { let total = threads.len(); - assert!(task_id < total); - simplify::renumber_event(event, &mut |id| id * total as u32 + task_id as u32) + assert!(task_id.as_usize() < total); + simplify::renumber_event(event, &mut |id| id * total as u32 + task_id.as_usize() as u32) } - threads[task_id].push(events) + threads[task_id.as_usize()].push(events) } // Error during execution Some(Err(err)) => match err { diff --git a/isla-lib/src/executor.rs b/isla-lib/src/executor.rs index 6015c84..05599d6 100644 --- a/isla-lib/src/executor.rs +++ b/isla-lib/src/executor.rs @@ -36,7 +36,6 @@ use crossbeam::queue::SegQueue; use std::borrow::Cow; use std::collections::HashMap; use std::fmt; -use std::mem; use std::sync::atomic::{AtomicBool, Ordering}; use std::sync::mpsc; use std::sync::mpsc::{Receiver, Sender}; @@ -49,22 +48,20 @@ use crate::error::{ExecError, IslaError}; use crate::fraction::Fraction; use crate::ir::*; use crate::log; -use crate::memory::Memory; use crate::primop; use crate::primop_util::{build_ite, ite_phi, smt_value, symbolic}; use crate::probe; -use crate::register::*; use crate::smt::smtlib::Def; use crate::smt::*; use crate::source_loc::SourceLoc; use crate::zencode; -#[derive(Clone)] -struct LocalState<'ir, B> { - vars: Bindings<'ir, B>, - regs: RegisterBindings<'ir, B>, - lets: Bindings<'ir, B>, -} +mod frame; +mod task; + +pub use frame::{freeze_frame, unfreeze_frame, Backtrace, Frame, LocalFrame, LocalState}; +use frame::{pop_call_stack, push_call_stack}; +pub use task::{StopAction, StopConditions, Task, TaskId, TaskState}; /// Gets a value from a variable `Bindings` map. Note that this function is set up to handle the /// following case: @@ -595,255 +592,6 @@ fn assign<'ir, B: BV>( assign_with_accessor(loc, v, local_state, shared_state, solver, &mut Vec::new(), info) } -/// The callstack is implemented as a closure that restores the -/// caller's stack frame. It additionally takes the shared state as -/// input also to avoid ownership issues when creating the closure. -type Stack<'ir, B> = Option< - Arc< - dyn 'ir - + Send - + Sync - + Fn(Val, &mut LocalFrame<'ir, B>, &SharedState<'ir, B>, &mut Solver) -> Result<(), ExecError>, - >, ->; - -pub type Backtrace = Vec<(Name, usize)>; - -/// A `Frame` is an immutable snapshot of the program state while it -/// is being symbolically executed. -#[derive(Clone)] -pub struct Frame<'ir, B> { - function_name: Name, - pc: usize, - forks: u32, - backjumps: u32, - local_state: Arc>, - memory: Arc>, - instrs: &'ir [Instr], - stack_vars: Arc>>, - stack_call: Stack<'ir, B>, - backtrace: Arc, - function_assumptions: Arc>, Val)>>>, - pc_counts: Arc>, -} - -/// A `LocalFrame` is a mutable frame which is used by a currently -/// executing thread. It is turned into an immutable `Frame` when the -/// control flow forks on a choice, which can be shared by threads. -pub struct LocalFrame<'ir, B> { - function_name: Name, - pc: usize, - forks: u32, - backjumps: u32, - local_state: LocalState<'ir, B>, - memory: Memory, - instrs: &'ir [Instr], - stack_vars: Vec>, - stack_call: Stack<'ir, B>, - backtrace: Backtrace, - function_assumptions: HashMap>, Val)>>, - pc_counts: HashMap, -} - -pub fn unfreeze_frame<'ir, B: BV>(frame: &Frame<'ir, B>) -> LocalFrame<'ir, B> { - LocalFrame { - function_name: frame.function_name, - pc: frame.pc, - forks: frame.forks, - backjumps: frame.backjumps, - local_state: (*frame.local_state).clone(), - memory: (*frame.memory).clone(), - instrs: frame.instrs, - stack_vars: (*frame.stack_vars).clone(), - stack_call: frame.stack_call.clone(), - backtrace: (*frame.backtrace).clone(), - function_assumptions: (*frame.function_assumptions).clone(), - pc_counts: (*frame.pc_counts).clone(), - } -} - -pub fn freeze_frame<'ir, B: BV>(frame: &LocalFrame<'ir, B>) -> Frame<'ir, B> { - Frame { - function_name: frame.function_name, - pc: frame.pc, - forks: frame.forks, - backjumps: frame.backjumps, - local_state: Arc::new(frame.local_state.clone()), - memory: Arc::new(frame.memory.clone()), - instrs: frame.instrs, - stack_vars: Arc::new(frame.stack_vars.clone()), - stack_call: frame.stack_call.clone(), - backtrace: Arc::new(frame.backtrace.clone()), - function_assumptions: Arc::new(frame.function_assumptions.clone()), - pc_counts: Arc::new(frame.pc_counts.clone()), - } -} - -impl<'ir, B: BV> LocalFrame<'ir, B> { - pub fn vars_mut(&mut self) -> &mut Bindings<'ir, B> { - &mut self.local_state.vars - } - - pub fn vars(&self) -> &Bindings<'ir, B> { - &self.local_state.vars - } - - pub fn regs_mut(&mut self) -> &mut RegisterBindings<'ir, B> { - &mut self.local_state.regs - } - - pub fn regs(&self) -> &RegisterBindings<'ir, B> { - &self.local_state.regs - } - - pub fn add_regs(&mut self, regs: &RegisterBindings<'ir, B>) -> &mut Self { - for (k, v) in regs { - self.local_state.regs.insert_register(*k, v.clone()) - } - self - } - - pub fn lets_mut(&mut self) -> &mut Bindings<'ir, B> { - &mut self.local_state.lets - } - - pub fn lets(&self) -> &Bindings<'ir, B> { - &self.local_state.lets - } - - pub fn add_lets(&mut self, lets: &Bindings<'ir, B>) -> &mut Self { - for (k, v) in lets { - self.local_state.lets.insert(*k, v.clone()); - } - self - } - - pub fn get_exception(&self) -> Option<(&Val, &str)> { - if let Some(UVal::Init(Val::Bool(true))) = self.lets().get(&HAVE_EXCEPTION) { - if let Some(UVal::Init(val)) = self.lets().get(&CURRENT_EXCEPTION) { - let loc = match self.lets().get(&THROW_LOCATION) { - Some(UVal::Init(Val::String(s))) => s, - Some(UVal::Init(_)) => "location has wrong type", - _ => "missing location", - }; - Some((val, loc)) - } else { - None - } - } else { - None - } - } - - pub fn memory(&self) -> &Memory { - &self.memory - } - - pub fn memory_mut(&mut self) -> &mut Memory { - &mut self.memory - } - - pub fn set_memory(&mut self, memory: Memory) -> &mut Self { - self.memory = memory; - self - } - - pub fn new( - name: Name, - args: &[(Name, &'ir Ty)], - ret_ty: &'ir Ty, - vals: Option<&[Val]>, - instrs: &'ir [Instr], - ) -> Self { - let mut vars = HashMap::default(); - vars.insert(RETURN, UVal::Uninit(ret_ty)); - match vals { - Some(vals) => { - for ((id, _), val) in args.iter().zip(vals) { - vars.insert(*id, UVal::Init(val.clone())); - } - } - None => { - for (id, ty) in args { - vars.insert(*id, UVal::Uninit(ty)); - } - } - } - - let mut lets = HashMap::default(); - lets.insert(HAVE_EXCEPTION, UVal::Init(Val::Bool(false))); - lets.insert(CURRENT_EXCEPTION, UVal::Uninit(&Ty::Union(SAIL_EXCEPTION))); - lets.insert(THROW_LOCATION, UVal::Uninit(&Ty::String)); - lets.insert(NULL, UVal::Init(Val::List(Vec::new()))); - - let regs = RegisterBindings::new(); - - LocalFrame { - function_name: name, - pc: 0, - forks: 0, - backjumps: 0, - local_state: LocalState { vars, regs, lets }, - memory: Memory::new(), - instrs, - stack_vars: Vec::new(), - stack_call: None, - backtrace: Vec::new(), - function_assumptions: HashMap::new(), - pc_counts: HashMap::new(), - } - } - - pub fn new_call( - &self, - name: Name, - args: &[(Name, &'ir Ty)], - ret_ty: &'ir Ty, - vals: Option<&[Val]>, - instrs: &'ir [Instr], - ) -> Self { - let mut new_frame = LocalFrame::new(name, args, ret_ty, vals, instrs); - new_frame.forks = self.forks; - new_frame.local_state.regs = self.local_state.regs.clone(); - new_frame.local_state.lets = self.local_state.lets.clone(); - new_frame.memory = self.memory.clone(); - new_frame - } - - pub fn task_with_checkpoint<'task>( - &self, - task_id: usize, - state: &'task TaskState, - checkpoint: Checkpoint, - ) -> Task<'ir, 'task, B> { - Task { - id: task_id, - fraction: Fraction::one(), - frame: freeze_frame(self), - checkpoint, - fork_cond: None, - state, - stop_conditions: None, - } - } - - pub fn task<'task>(&self, task_id: usize, state: &'task TaskState) -> Task<'ir, 'task, B> { - self.task_with_checkpoint(task_id, state, Checkpoint::new()) - } -} - -fn push_call_stack(frame: &mut LocalFrame<'_, B>) { - let mut vars = HashMap::default(); - mem::swap(&mut vars, frame.vars_mut()); - frame.stack_vars.push(vars) -} - -fn pop_call_stack(frame: &mut LocalFrame<'_, B>) { - if let Some(mut vars) = frame.stack_vars.pop() { - mem::swap(&mut vars, frame.vars_mut()) - } -} - #[derive(Copy, Clone, Debug)] struct Timeout { start_time: Instant, @@ -982,101 +730,10 @@ pub fn reset_registers<'ir, 'task, B: BV>( Ok(()) } -// A collection of simple conditions under which to stop the execution -// of path. The conditions are formed of the name of a function to -// stop at, with an optional second name that must appear in the -// backtrace. - -#[derive(Clone)] -pub struct StopConditions { - stops: HashMap, Option)>, -} - -#[derive(Clone, Copy)] -pub enum StopAction { - Kill, // Remove entire trace - Abstract, // Keep trace, put abstract call at end -} - -impl StopConditions { - pub fn new() -> Self { - StopConditions { stops: HashMap::new() } - } - - pub fn add(&mut self, function: Name, context: Option, action: StopAction) { - let fn_entry = self.stops.entry(function).or_insert((HashMap::new(), None)); - if let Some(ctx) = context { - fn_entry.0.insert(ctx, action); - } else { - fn_entry.1 = Some(action); - } - } - - pub fn union(&self, other: &StopConditions) -> Self { - let mut dest: StopConditions = self.clone(); - for (f, (ctx, direct)) in &other.stops { - if let Some(action) = direct { - dest.add(*f, None, *action); - } - for (context, action) in ctx { - dest.add(*f, Some(*context), *action); - } - } - dest - } - - pub fn should_stop(&self, callee: Name, caller: Name, backtrace: &Backtrace) -> Option { - if let Some((ctx, direct)) = self.stops.get(&callee) { - for (name, action) in ctx { - if *name == caller || backtrace.iter().any(|(bt_name, _)| *name == *bt_name) { - return Some(*action); - } - } - *direct - } else { - None - } - } - - fn parse_function_name(f: &str, shared_state: &SharedState) -> Name { - let fz = zencode::encode(f); - shared_state - .symtab - .get(&fz) - .or_else(|| shared_state.symtab.get(f)) - .unwrap_or_else(|| panic!("Function {} not found", f)) - } - - pub fn parse(args: Vec, shared_state: &SharedState, action: StopAction) -> StopConditions { - let mut conds = StopConditions::new(); - for arg in args { - let mut names = arg.split(','); - if let Some(f) = names.next() { - if let Some(ctx) = names.next() { - if names.next().is_none() { - conds.add( - StopConditions::parse_function_name(f, shared_state), - Some(StopConditions::parse_function_name(ctx, shared_state)), - action, - ); - } else { - panic!("Bad stop condition: {}", arg); - } - } else { - conds.add(StopConditions::parse_function_name(f, shared_state), None, action); - } - } else { - panic!("Bad stop condition: {}", arg); - } - } - conds - } -} - #[allow(clippy::too_many_arguments)] fn run<'ir, 'task, B: BV>( tid: usize, - task_id: usize, + task_id: TaskId, task_fraction: &mut Fraction, timeout: Timeout, stop_conditions: Option<&'task StopConditions>, @@ -1300,7 +957,7 @@ pub enum Run { #[allow(clippy::too_many_arguments)] fn run_loop<'ir, 'task, B: BV>( tid: usize, - task_id: usize, + task_id: TaskId, task_fraction: &mut Fraction, timeout: Timeout, stop_conditions: Option<&'task StopConditions>, @@ -1708,63 +1365,7 @@ fn run_loop<'ir, 'task, B: BV>( /// collecting the results into a type R. pub type Collector<'ir, B, R> = dyn 'ir + Sync - + Fn(usize, usize, Result<(Run, LocalFrame<'ir, B>), (ExecError, Backtrace)>, &SharedState<'ir, B>, Solver, &R); - -pub struct TaskState { - reset_registers: HashMap, Reset>, - // We might want to avoid loops in the assembly by requiring that - // any unique program counter (pc) is only visited a fixed number - // of times. Note that this is the architectural PC, not the isla - // IR program counter in the frame. - pc_limit: Option<(Name, usize)>, - // Exit if we ever announce an instruction with all bits set to zero - zero_announce_exit: bool, -} - -impl TaskState { - pub fn new() -> Self { - TaskState { reset_registers: HashMap::new(), pc_limit: None, zero_announce_exit: true } - } - - pub fn with_reset_registers(self, reset_registers: HashMap, Reset>) -> Self { - TaskState { reset_registers, ..self } - } - - pub fn with_pc_limit(self, pc: Name, limit: usize) -> Self { - TaskState { pc_limit: Some((pc, limit)), ..self } - } - - pub fn with_zero_announce_exit(self, b: bool) -> Self { - TaskState { zero_announce_exit: b, ..self } - } -} - -impl Default for TaskState { - fn default() -> Self { - Self::new() - } -} - -/// A `Task` is a suspended point in the symbolic execution of a -/// program. It consists of a frame, which is a snapshot of the -/// program variables, a checkpoint which allows us to reconstruct the -/// SMT solver state, and finally an option SMTLIB definiton which is -/// added to the solver state when the task is resumed. -pub struct Task<'ir, 'task, B> { - id: usize, - fraction: Fraction, - frame: Frame<'ir, B>, - checkpoint: Checkpoint, - fork_cond: Option<(smtlib::Def, Event)>, - state: &'task TaskState, - stop_conditions: Option<&'task StopConditions>, -} - -impl<'ir, 'task, B> Task<'ir, 'task, B> { - pub fn set_stop_conditions(&mut self, new_fns: &'task StopConditions) { - self.stop_conditions = Some(new_fns); - } -} + + Fn(usize, TaskId, Result<(Run, LocalFrame<'ir, B>), (ExecError, Backtrace)>, &SharedState<'ir, B>, Solver, &R); /// Start symbolically executing a Task using just the current thread, collecting the results using /// the given collector. @@ -1852,7 +1453,7 @@ enum Response { } enum Progress { - Finished { tid: usize, task_id: usize, frac: Fraction }, + Finished { tid: usize, task_id: TaskId, frac: Fraction }, Idle { tid: usize }, } @@ -1874,7 +1475,7 @@ pub fn start_multi<'ir, 'task, B: BV, R>( let global: Arc>> = Arc::new(Injector::>::new()); let stealers: Arc>>>> = Arc::new(RwLock::new(Vec::new())); - let mut progress: HashMap = HashMap::default(); + let mut progress: HashMap = HashMap::default(); for task in tasks { progress.insert(task.id, Fraction::zero()); @@ -1943,8 +1544,8 @@ pub fn start_multi<'ir, 'task, B: BV, R>( } } if all_tasks_complete { - for tid in 0..num_threads { - poke_txs[tid].send(Response::Kill).unwrap() + for poke_tx in poke_txs.iter() { + poke_tx.send(Response::Kill).unwrap() } break; } @@ -1959,7 +1560,7 @@ pub fn start_multi<'ir, 'task, B: BV, R>( /// true. pub fn all_unsat_collector<'ir, B: BV>( tid: usize, - _: usize, + _: TaskId, result: Result<(Run, LocalFrame<'ir, B>), (ExecError, Backtrace)>, shared_state: &SharedState<'ir, B>, mut solver: Solver, @@ -2047,15 +1648,15 @@ impl TraceError { } } -pub type TraceQueue = SegQueue>), TraceError>>; +pub type TraceQueue = SegQueue>), TraceError>>; -pub type TraceResultQueue = SegQueue>), TraceError>>; +pub type TraceResultQueue = SegQueue>), TraceError>>; -pub type TraceValueQueue = SegQueue, Vec>), TraceError>>; +pub type TraceValueQueue = SegQueue, Vec>), TraceError>>; pub fn trace_collector<'ir, B: BV>( tid: usize, - task_id: usize, + task_id: TaskId, result: Result<(Run, LocalFrame<'ir, B>), (ExecError, Backtrace)>, shared_state: &SharedState<'ir, B>, mut solver: Solver, @@ -2085,7 +1686,7 @@ pub fn trace_collector<'ir, B: BV>( pub fn trace_value_collector<'ir, B: BV>( _: usize, - task_id: usize, + task_id: TaskId, result: Result<(Run, LocalFrame<'ir, B>), (ExecError, Backtrace)>, _: &SharedState<'ir, B>, mut solver: Solver, @@ -2111,7 +1712,7 @@ pub fn trace_value_collector<'ir, B: BV>( pub fn trace_result_collector<'ir, B: BV>( _: usize, - task_id: usize, + task_id: TaskId, result: Result<(Run, LocalFrame<'ir, B>), (ExecError, Backtrace)>, _: &SharedState<'ir, B>, solver: Solver, @@ -2132,7 +1733,7 @@ pub fn trace_result_collector<'ir, B: BV>( pub fn footprint_collector<'ir, B: BV>( _: usize, - task_id: usize, + task_id: TaskId, result: Result<(Run, LocalFrame<'ir, B>), (ExecError, Backtrace)>, _: &SharedState<'ir, B>, solver: Solver, diff --git a/isla-lib/src/executor/frame.rs b/isla-lib/src/executor/frame.rs new file mode 100644 index 0000000..86b19bf --- /dev/null +++ b/isla-lib/src/executor/frame.rs @@ -0,0 +1,299 @@ +// BSD 2-Clause License +// +// Copyright (c) 2019-2024 Alasdair Armstrong +// Copyright (c) 2020 Brian Campbell +// Copyright (c) 2020 Dhruv Makwana +// +// All rights reserved. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are +// met: +// +// 1. Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// +// 2. Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +// HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +use std::collections::HashMap; +use std::mem; +use std::sync::Arc; + +use crate::bitvector::BV; +use crate::error::ExecError; +use crate::executor::task::{Task, TaskId, TaskState}; +use crate::fraction::Fraction; +use crate::ir::*; +use crate::memory::Memory; +use crate::register::RegisterBindings; +use crate::smt::{Checkpoint, Solver}; + +#[derive(Clone)] +pub struct LocalState<'ir, B> { + pub(super) vars: Bindings<'ir, B>, + pub(super) regs: RegisterBindings<'ir, B>, + pub(super) lets: Bindings<'ir, B>, +} + +/// The callstack is implemented as a closure that restores the +/// caller's stack frame. It additionally takes the shared state as +/// input also to avoid ownership issues when creating the closure. +pub(super) type Stack<'ir, B> = Option< + Arc< + dyn 'ir + + Send + + Sync + + Fn(Val, &mut LocalFrame<'ir, B>, &SharedState<'ir, B>, &mut Solver) -> Result<(), ExecError>, + >, +>; + +pub type Backtrace = Vec<(Name, usize)>; + +/// A `Frame` is an immutable snapshot of the program state while it +/// is being symbolically executed. +#[derive(Clone)] +pub struct Frame<'ir, B> { + pub(super) function_name: Name, + pub(super) pc: usize, + pub(super) forks: u32, + pub(super) backjumps: u32, + pub(super) local_state: Arc>, + pub(super) memory: Arc>, + pub(super) instrs: &'ir [Instr], + pub(super) stack_vars: Arc>>, + pub(super) stack_call: Stack<'ir, B>, + pub(super) backtrace: Arc, + pub(super) function_assumptions: Arc>, Val)>>>, + pub(super) pc_counts: Arc>, +} + +pub fn unfreeze_frame<'ir, B: BV>(frame: &Frame<'ir, B>) -> LocalFrame<'ir, B> { + LocalFrame { + function_name: frame.function_name, + pc: frame.pc, + forks: frame.forks, + backjumps: frame.backjumps, + local_state: (*frame.local_state).clone(), + memory: (*frame.memory).clone(), + instrs: frame.instrs, + stack_vars: (*frame.stack_vars).clone(), + stack_call: frame.stack_call.clone(), + backtrace: (*frame.backtrace).clone(), + function_assumptions: (*frame.function_assumptions).clone(), + pc_counts: (*frame.pc_counts).clone(), + } +} + +/// A `LocalFrame` is a mutable frame which is used by a currently +/// executing thread. It is turned into an immutable `Frame` when the +/// control flow forks on a choice, which can be shared by threads. +pub struct LocalFrame<'ir, B> { + pub(super) function_name: Name, + pub(super) pc: usize, + pub(super) forks: u32, + pub(super) backjumps: u32, + pub(super) local_state: LocalState<'ir, B>, + pub(super) memory: Memory, + pub(super) instrs: &'ir [Instr], + pub(super) stack_vars: Vec>, + pub(super) stack_call: Stack<'ir, B>, + pub(super) backtrace: Backtrace, + pub(super) function_assumptions: HashMap>, Val)>>, + pub(super) pc_counts: HashMap, +} + +pub fn freeze_frame<'ir, B: BV>(frame: &LocalFrame<'ir, B>) -> Frame<'ir, B> { + Frame { + function_name: frame.function_name, + pc: frame.pc, + forks: frame.forks, + backjumps: frame.backjumps, + local_state: Arc::new(frame.local_state.clone()), + memory: Arc::new(frame.memory.clone()), + instrs: frame.instrs, + stack_vars: Arc::new(frame.stack_vars.clone()), + stack_call: frame.stack_call.clone(), + backtrace: Arc::new(frame.backtrace.clone()), + function_assumptions: Arc::new(frame.function_assumptions.clone()), + pc_counts: Arc::new(frame.pc_counts.clone()), + } +} + +impl<'ir, B: BV> LocalFrame<'ir, B> { + pub fn vars_mut(&mut self) -> &mut Bindings<'ir, B> { + &mut self.local_state.vars + } + + pub fn vars(&self) -> &Bindings<'ir, B> { + &self.local_state.vars + } + + pub fn regs_mut(&mut self) -> &mut RegisterBindings<'ir, B> { + &mut self.local_state.regs + } + + pub fn regs(&self) -> &RegisterBindings<'ir, B> { + &self.local_state.regs + } + + pub fn add_regs(&mut self, regs: &RegisterBindings<'ir, B>) -> &mut Self { + for (k, v) in regs { + self.local_state.regs.insert_register(*k, v.clone()) + } + self + } + + pub fn lets_mut(&mut self) -> &mut Bindings<'ir, B> { + &mut self.local_state.lets + } + + pub fn lets(&self) -> &Bindings<'ir, B> { + &self.local_state.lets + } + + pub fn add_lets(&mut self, lets: &Bindings<'ir, B>) -> &mut Self { + for (k, v) in lets { + self.local_state.lets.insert(*k, v.clone()); + } + self + } + + pub fn get_exception(&self) -> Option<(&Val, &str)> { + if let Some(UVal::Init(Val::Bool(true))) = self.lets().get(&HAVE_EXCEPTION) { + if let Some(UVal::Init(val)) = self.lets().get(&CURRENT_EXCEPTION) { + let loc = match self.lets().get(&THROW_LOCATION) { + Some(UVal::Init(Val::String(s))) => s, + Some(UVal::Init(_)) => "location has wrong type", + _ => "missing location", + }; + Some((val, loc)) + } else { + None + } + } else { + None + } + } + + pub fn memory(&self) -> &Memory { + &self.memory + } + + pub fn memory_mut(&mut self) -> &mut Memory { + &mut self.memory + } + + pub fn set_memory(&mut self, memory: Memory) -> &mut Self { + self.memory = memory; + self + } + + pub fn new( + name: Name, + args: &[(Name, &'ir Ty)], + ret_ty: &'ir Ty, + vals: Option<&[Val]>, + instrs: &'ir [Instr], + ) -> Self { + let mut vars = HashMap::default(); + vars.insert(RETURN, UVal::Uninit(ret_ty)); + match vals { + Some(vals) => { + for ((id, _), val) in args.iter().zip(vals) { + vars.insert(*id, UVal::Init(val.clone())); + } + } + None => { + for (id, ty) in args { + vars.insert(*id, UVal::Uninit(ty)); + } + } + } + + let mut lets = HashMap::default(); + lets.insert(HAVE_EXCEPTION, UVal::Init(Val::Bool(false))); + lets.insert(CURRENT_EXCEPTION, UVal::Uninit(&Ty::Union(SAIL_EXCEPTION))); + lets.insert(THROW_LOCATION, UVal::Uninit(&Ty::String)); + lets.insert(NULL, UVal::Init(Val::List(Vec::new()))); + + let regs = RegisterBindings::new(); + + LocalFrame { + function_name: name, + pc: 0, + forks: 0, + backjumps: 0, + local_state: LocalState { vars, regs, lets }, + memory: Memory::new(), + instrs, + stack_vars: Vec::new(), + stack_call: None, + backtrace: Vec::new(), + function_assumptions: HashMap::new(), + pc_counts: HashMap::new(), + } + } + + pub fn new_call( + &self, + name: Name, + args: &[(Name, &'ir Ty)], + ret_ty: &'ir Ty, + vals: Option<&[Val]>, + instrs: &'ir [Instr], + ) -> Self { + let mut new_frame = LocalFrame::new(name, args, ret_ty, vals, instrs); + new_frame.forks = self.forks; + new_frame.local_state.regs = self.local_state.regs.clone(); + new_frame.local_state.lets = self.local_state.lets.clone(); + new_frame.memory = self.memory.clone(); + new_frame + } + + pub fn task_with_checkpoint<'task>( + &self, + task_id: TaskId, + state: &'task TaskState, + checkpoint: Checkpoint, + ) -> Task<'ir, 'task, B> { + Task { + id: task_id, + fraction: Fraction::one(), + frame: freeze_frame(self), + checkpoint, + fork_cond: None, + state, + stop_conditions: None, + } + } + + pub fn task<'task>(&self, task_id: TaskId, state: &'task TaskState) -> Task<'ir, 'task, B> { + self.task_with_checkpoint(task_id, state, Checkpoint::new()) + } +} + +pub(super) fn push_call_stack(frame: &mut LocalFrame<'_, B>) { + let mut vars = HashMap::default(); + mem::swap(&mut vars, frame.vars_mut()); + frame.stack_vars.push(vars) +} + +pub(super) fn pop_call_stack(frame: &mut LocalFrame<'_, B>) { + if let Some(mut vars) = frame.stack_vars.pop() { + mem::swap(&mut vars, frame.vars_mut()) + } +} diff --git a/isla-lib/src/executor/task.rs b/isla-lib/src/executor/task.rs new file mode 100644 index 0000000..73c08d7 --- /dev/null +++ b/isla-lib/src/executor/task.rs @@ -0,0 +1,206 @@ +// BSD 2-Clause License +// +// Copyright (c) 2019-2024 Alasdair Armstrong +// Copyright (c) 2020 Brian Campbell +// Copyright (c) 2020 Dhruv Makwana +// +// All rights reserved. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are +// met: +// +// 1. Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// +// 2. Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +// HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +use std::collections::HashMap; +use std::sync::atomic::{AtomicUsize, Ordering}; + +use crate::executor::frame::{Backtrace, Frame}; +use crate::fraction::Fraction; +use crate::ir::{Loc, Name, Reset, SharedState}; +use crate::smt::{smtlib, Checkpoint, Event}; +use crate::zencode; + +static TASK_COUNTER: AtomicUsize = AtomicUsize::new(0); + +#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] +pub struct TaskId { + id: usize, +} + +impl TaskId { + pub fn from_usize(id: usize) -> Self { + TaskId { id } + } + + pub fn as_usize(self) -> usize { + self.id + } + + pub fn fresh() -> Self { + TaskId { id: TASK_COUNTER.fetch_add(1, Ordering::SeqCst) } + } +} + +pub struct TaskState { + pub(super) reset_registers: HashMap, Reset>, + // We might want to avoid loops in the assembly by requiring that + // any unique program counter (pc) is only visited a fixed number + // of times. Note that this is the architectural PC, not the isla + // IR program counter in the frame. + pub(super) pc_limit: Option<(Name, usize)>, + // Exit if we ever announce an instruction with all bits set to zero + pub(super) zero_announce_exit: bool, +} + +impl TaskState { + pub fn new() -> Self { + TaskState { reset_registers: HashMap::new(), pc_limit: None, zero_announce_exit: true } + } + + pub fn with_reset_registers(self, reset_registers: HashMap, Reset>) -> Self { + TaskState { reset_registers, ..self } + } + + pub fn with_pc_limit(self, pc: Name, limit: usize) -> Self { + TaskState { pc_limit: Some((pc, limit)), ..self } + } + + pub fn with_zero_announce_exit(self, b: bool) -> Self { + TaskState { zero_announce_exit: b, ..self } + } +} + +impl Default for TaskState { + fn default() -> Self { + Self::new() + } +} + +/// A collection of simple conditions under which to stop the execution +/// of path. The conditions are formed of the name of a function to +/// stop at, with an optional second name that must appear in the +/// backtrace. +#[derive(Clone)] +pub struct StopConditions { + stops: HashMap, Option)>, +} + +#[derive(Clone, Copy)] +pub enum StopAction { + Kill, // Remove entire trace + Abstract, // Keep trace, put abstract call at end +} + +impl StopConditions { + pub fn new() -> Self { + StopConditions { stops: HashMap::new() } + } + + pub fn add(&mut self, function: Name, context: Option, action: StopAction) { + let fn_entry = self.stops.entry(function).or_insert((HashMap::new(), None)); + if let Some(ctx) = context { + fn_entry.0.insert(ctx, action); + } else { + fn_entry.1 = Some(action); + } + } + + pub fn union(&self, other: &StopConditions) -> Self { + let mut dest: StopConditions = self.clone(); + for (f, (ctx, direct)) in &other.stops { + if let Some(action) = direct { + dest.add(*f, None, *action); + } + for (context, action) in ctx { + dest.add(*f, Some(*context), *action); + } + } + dest + } + + pub fn should_stop(&self, callee: Name, caller: Name, backtrace: &Backtrace) -> Option { + if let Some((ctx, direct)) = self.stops.get(&callee) { + for (name, action) in ctx { + if *name == caller || backtrace.iter().any(|(bt_name, _)| *name == *bt_name) { + return Some(*action); + } + } + *direct + } else { + None + } + } + + fn parse_function_name(f: &str, shared_state: &SharedState) -> Name { + let fz = zencode::encode(f); + shared_state + .symtab + .get(&fz) + .or_else(|| shared_state.symtab.get(f)) + .unwrap_or_else(|| panic!("Function {} not found", f)) + } + + pub fn parse(args: Vec, shared_state: &SharedState, action: StopAction) -> StopConditions { + let mut conds = StopConditions::new(); + for arg in args { + let mut names = arg.split(','); + if let Some(f) = names.next() { + if let Some(ctx) = names.next() { + if names.next().is_none() { + conds.add( + StopConditions::parse_function_name(f, shared_state), + Some(StopConditions::parse_function_name(ctx, shared_state)), + action, + ); + } else { + panic!("Bad stop condition: {}", arg); + } + } else { + conds.add(StopConditions::parse_function_name(f, shared_state), None, action); + } + } else { + panic!("Bad stop condition: {}", arg); + } + } + conds + } +} + +/// A `Task` is a suspended point in the symbolic execution of a +/// program. It consists of a frame, which is a snapshot of the +/// program variables, a checkpoint which allows us to reconstruct the +/// SMT solver state, and finally an option SMTLIB definiton which is +/// added to the solver state when the task is resumed. +pub struct Task<'ir, 'task, B> { + pub(crate) id: TaskId, + pub(crate) fraction: Fraction, + pub(crate) frame: Frame<'ir, B>, + pub(crate) checkpoint: Checkpoint, + pub(crate) fork_cond: Option<(smtlib::Def, Event)>, + pub(crate) state: &'task TaskState, + pub(crate) stop_conditions: Option<&'task StopConditions>, +} + +impl<'ir, 'task, B> Task<'ir, 'task, B> { + pub fn set_stop_conditions(&mut self, new_fns: &'task StopConditions) { + self.stop_conditions = Some(new_fns); + } +} diff --git a/isla-lib/src/init.rs b/isla-lib/src/init.rs index d7eaf3e..df60932 100644 --- a/isla-lib/src/init.rs +++ b/isla-lib/src/init.rs @@ -56,7 +56,8 @@ use std::sync::Mutex; use crate::bitvector::BV; use crate::config::ISAConfig; -use crate::executor::{start_single, LocalFrame, TaskState}; +use crate::executor::start_single; +use crate::executor::{LocalFrame, TaskId, TaskState}; use crate::ir::*; use crate::log; use crate::register::RegisterBindings; @@ -77,7 +78,7 @@ fn initialize_letbinding<'ir, B: BV>( LocalFrame::new(TOP_LEVEL_LET, &vars, &Ty::Unit, None, setup) .add_regs(®s) .add_lets(&lets) - .task(0, &task_state) + .task(TaskId::fresh(), &task_state) }; start_single( @@ -135,7 +136,7 @@ fn initialize_register<'ir, B: BV>( LocalFrame::new(REGISTER_INIT, &[], &Ty::Unit, None, setup) .add_regs(®s) .add_lets(&lets) - .task(0, &task_state) + .task(TaskId::fresh(), &task_state) }; start_single( diff --git a/isla-lib/src/ir/linearize.rs b/isla-lib/src/ir/linearize.rs index 2c872db..e8c30df 100644 --- a/isla-lib/src/ir/linearize.rs +++ b/isla-lib/src/ir/linearize.rs @@ -478,7 +478,7 @@ pub fn self_test<'ir, B: BV>( let task = executor::LocalFrame::new(comparison, args, &Ty::Bool, None, instrs) .add_lets(&lets) .add_regs(®s) - .task(0, &task_state); + .task(executor::TaskId::fresh(), &task_state); let result = Arc::new(AtomicBool::new(true)); executor::start_multi(num_threads, None, vec![task], &shared_state, result.clone(), &executor::all_unsat_collector); diff --git a/src/client.rs b/src/client.rs index 3e4636e..2fe9188 100644 --- a/src/client.rs +++ b/src/client.rs @@ -40,7 +40,7 @@ use isla_axiomatic::litmus::assemble_instruction; use isla_lib::bitvector::{b64::B64, BV}; use isla_lib::config::ISAConfig; use isla_lib::executor; -use isla_lib::executor::{LocalFrame, TaskState}; +use isla_lib::executor::{LocalFrame, TaskId, TaskState}; use isla_lib::init::{initialize_architecture, Initialized}; use isla_lib::ir::*; use isla_lib::register::RegisterBindings; @@ -119,7 +119,7 @@ fn execute_opcode( let task = LocalFrame::new(function_id, args, ret_ty, Some(&[Val::Bits(opcode)]), instrs) .add_lets(letbindings) .add_regs(register_state) - .task(0, &task_state); + .task(TaskId::fresh(), &task_state); let queue = Arc::new(SegQueue::new()); diff --git a/src/execute-function.rs b/src/execute-function.rs index 778d1a2..b737549 100644 --- a/src/execute-function.rs +++ b/src/execute-function.rs @@ -41,7 +41,7 @@ use isla_lib::bitvector::b129::B129; use isla_lib::bitvector::BV; use isla_lib::error::ExecError; use isla_lib::executor; -use isla_lib::executor::{reset_registers, Backtrace, LocalFrame, Run, StopAction, StopConditions, TaskState}; +use isla_lib::executor::{reset_registers, Backtrace, LocalFrame, Run, StopAction, StopConditions, TaskId, TaskState}; use isla_lib::init::{initialize_architecture, Initialized}; use isla_lib::ir::*; use isla_lib::ir_lexer::new_ir_lexer; @@ -167,7 +167,7 @@ fn isla_main() -> i32 { reset_registers(0, &mut frame, &task_state, &shared_state, &mut solver, SourceLoc::unknown()) .expect("Reset registers failed"); - let mut task = frame.task_with_checkpoint(0, &task_state, smt::checkpoint(&mut solver)); + let mut task = frame.task_with_checkpoint(TaskId::fresh(), &task_state, smt::checkpoint(&mut solver)); task.set_stop_conditions(&stop_conditions); let traces = matches.opt_present("traces"); @@ -297,11 +297,11 @@ fn concrete_value(model: &mut Model, val: &Val) -> Val { } } -type AllTraceValueQueue = SegQueue, Vec>), (String, Vec>)>>; +type AllTraceValueQueue = SegQueue, Vec>), (String, Vec>)>>; fn model_collector<'ir, B: BV>( tid: usize, - task_id: usize, + task_id: TaskId, result: Result<(Run, LocalFrame<'ir, B>), (ExecError, Backtrace)>, shared_state: &SharedState<'ir, B>, mut solver: Solver, diff --git a/src/footprint.rs b/src/footprint.rs index 4597ce8..3339ab7 100644 --- a/src/footprint.rs +++ b/src/footprint.rs @@ -48,7 +48,7 @@ use isla_elf::relocation_types::SymbolicRelocation; use isla_lib::bitvector::{b129::B129, BV}; use isla_lib::error::IslaError; use isla_lib::executor; -use isla_lib::executor::{LocalFrame, StopAction, StopConditions, TaskState}; +use isla_lib::executor::{LocalFrame, StopAction, StopConditions, TaskId, TaskState}; use isla_lib::init::{initialize_architecture, InitArchWithConfig}; use isla_lib::ir::*; use isla_lib::log; @@ -603,7 +603,7 @@ fn isla_main() -> i32 { .add_lets(lets) .add_regs(regs) .set_memory(memory) - .task_with_checkpoint(0, &task_state, initial_checkpoint); + .task_with_checkpoint(TaskId::fresh(), &task_state, initial_checkpoint); task.set_stop_conditions(&stop_conditions); let queue = Arc::new(SegQueue::new()); diff --git a/src/property.rs b/src/property.rs index 1c990a8..f019c15 100644 --- a/src/property.rs +++ b/src/property.rs @@ -34,7 +34,7 @@ use std::sync::Arc; use isla_lib::bitvector::b64::B64; use isla_lib::executor; -use isla_lib::executor::{LocalFrame, TaskState}; +use isla_lib::executor::{LocalFrame, TaskId, TaskState}; use isla_lib::init::{initialize_architecture, Initialized}; use isla_lib::ir::*; use isla_lib::zencode; @@ -71,8 +71,10 @@ fn isla_main() -> i32 { let function_id = shared_state.symtab.lookup(&property); let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); let task_state = TaskState::new(); - let task = - LocalFrame::new(function_id, args, ret_ty, None, instrs).add_lets(&lets).add_regs(®s).task(0, &task_state); + let task = LocalFrame::new(function_id, args, ret_ty, None, instrs) + .add_lets(&lets) + .add_regs(®s) + .task(TaskId::fresh(), &task_state); let result = Arc::new(AtomicBool::new(true)); executor::start_multi(num_threads, None, vec![task], &shared_state, result.clone(), &executor::all_unsat_collector); diff --git a/src/property129.rs b/src/property129.rs index 14300d5..fe24fb9 100644 --- a/src/property129.rs +++ b/src/property129.rs @@ -34,7 +34,7 @@ use std::sync::Arc; use isla_lib::bitvector::b129::B129; use isla_lib::executor; -use isla_lib::executor::{LocalFrame, TaskState}; +use isla_lib::executor::{LocalFrame, TaskId, TaskState}; use isla_lib::init::{initialize_architecture, Initialized}; use isla_lib::ir::*; use isla_lib::zencode; @@ -71,8 +71,10 @@ fn isla_main() -> i32 { let function_id = shared_state.symtab.lookup(&property); let (args, ret_ty, instrs) = shared_state.functions.get(&function_id).unwrap(); let task_state = TaskState::new(); - let task = - LocalFrame::new(function_id, args, ret_ty, None, instrs).add_lets(&lets).add_regs(®s).task(0, &task_state); + let task = LocalFrame::new(function_id, args, ret_ty, None, instrs) + .add_lets(&lets) + .add_regs(®s) + .task(TaskId::fresh(), &task_state); let result = Arc::new(AtomicBool::new(true)); executor::start_multi(num_threads, None, vec![task], &shared_state, result.clone(), &executor::all_unsat_collector);