Refactor executor

Split various stack/frame types and the task types into their own files
rems-project · Feb 6, 2024 · c512e87 · c512e87
1 parent 97cdca7
commit c512e87
Show file tree

Hide file tree

Showing 12 changed files with 558 additions and 447 deletions.
diff --git 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
@@ -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,15 +307,15 @@ where
                         .add_lets(&lets)
                         .add_regs(&regs)
                         .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();
                     LocalFrame::new(thread.call, args, ret_ty, Some(&[Val::Unit]), instrs)
                         .add_lets(&lets)
                         .add_regs(&regs)
                         .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 {