Skip to content

Commit 29eacb6

Browse files
committed
fix(ci): resolve secondary compilation and KANI installation issues
This commit addresses the remaining CI failures after the primary blocker was resolved, focusing on memory provider consistency and KANI toolchain installation. MEMORY PROVIDER FIXES: - Fix StacklessEngine memory size inconsistency (1024 vs 4096) - Use RUNTIME_MEMORY_SIZE constant consistently across std/no_std - Remove unsafe type casts in StacklessEngine constructor - Separate std/no_std initialization paths properly KANI INSTALLATION FIXES: - Remove non-existent kani-driver installation - Fix KANI setup to use: cargo install kani-verifier + cargo kani setup - Update both kani-regression.yml and deploy-verification.yml workflows TECHNICAL DETAILS: - StacklessEngine now uses proper types instead of casting BoundedMap to HashMap - Memory allocation uses RUNTIME_MEMORY_SIZE (4096) instead of hardcoded 1024 - KANI follows official 2025 installation guide from model-checking.github.io IMPACT: - Should resolve most Test Default, Integration Tests, and other test job failures - Should fix all KANI Verification job failures - Maintains backward compatibility for both std and no_std configurations These fixes target the type mismatch errors (E0605, E0308) and KANI setup issues that were blocking CI after the primary SIMD compilation issue was resolved.
1 parent 2a86caf commit 29eacb6

File tree

4 files changed

+33
-16
lines changed

4 files changed

+33
-16
lines changed

.github/workflows/deploy-verification.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ jobs:
5656
- name: Install KANI and cargo-wrt
5757
run: |
5858
cargo install --locked kani-verifier
59-
cargo install --locked kani-driver
59+
cargo kani setup
6060
cargo install --path cargo-wrt --locked
6161
6262
- name: Run pre-deployment verification

.github/workflows/kani-regression.yml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -105,9 +105,10 @@ jobs:
105105
106106
- name: Install KANI Verifier
107107
run: |
108-
# Install KANI from source for latest features
108+
# Install KANI verifier
109109
cargo install --locked kani-verifier
110-
cargo install --locked kani-driver
110+
# Setup KANI dependencies
111+
cargo kani setup
111112
# Verify installation
112113
kani --version
113114

wrt-build-core/src/wast_execution.rs

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -70,13 +70,13 @@ impl WastEngine {
7070
Module::from_wrt_module(&wrt_module).context("Failed to convert to runtime module")?;
7171

7272
// Create a module instance from the module
73-
use wrt_runtime::module_instance::ModuleInstance;
7473
use std::sync::Arc;
74+
75+
use wrt_runtime::module_instance::ModuleInstance;
7576
let module_instance = Arc::new(
76-
ModuleInstance::new(module.clone(), 0)
77-
.context("Failed to create module instance")?
77+
ModuleInstance::new(module.clone(), 0).context("Failed to create module instance")?,
7878
);
79-
79+
8080
// Set the current module in the engine
8181
let _instance_idx = self
8282
.engine

wrt-runtime/src/stackless/engine.rs

Lines changed: 25 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -212,14 +212,29 @@ impl StacklessEngine {
212212
let operand_stack = BoundedVec::new(provider)
213213
.map_err(|_| wrt_error::Error::runtime_error("Failed to create operand stack"))?;
214214

215-
Ok(Self {
216-
instances: instances as HashMap<usize, Arc<ModuleInstance>>,
217-
next_instance_id: AtomicU64::new(1),
218-
current_instance_id: None,
219-
operand_stack: operand_stack as Vec<Value>,
220-
call_frames_count: 0,
221-
stats: ExecutionStats::default(),
222-
})
215+
#[cfg(any(feature = "std", feature = "alloc"))]
216+
{
217+
Ok(Self {
218+
instances: HashMap::new(),
219+
next_instance_id: AtomicU64::new(1),
220+
current_instance_id: None,
221+
operand_stack: Vec::new(),
222+
call_frames_count: 0,
223+
stats: ExecutionStats::default(),
224+
})
225+
}
226+
227+
#[cfg(not(any(feature = "std", feature = "alloc")))]
228+
{
229+
Ok(Self {
230+
instances,
231+
next_instance_id: AtomicU64::new(1),
232+
current_instance_id: None,
233+
operand_stack,
234+
call_frames_count: 0,
235+
stats: ExecutionStats::default(),
236+
})
237+
}
223238
}
224239

225240
/// Set the current module for execution
@@ -303,11 +318,12 @@ impl StacklessEngine {
303318

304319
#[cfg(not(any(feature = "std", feature = "alloc")))]
305320
let mut results = {
321+
use crate::bounded_runtime_infra::RUNTIME_MEMORY_SIZE;
306322
use wrt_foundation::{
307323
budget_aware_provider::CrateId,
308324
safe_managed_alloc,
309325
};
310-
let provider = safe_managed_alloc!(1024, CrateId::Runtime)?;
326+
let provider = safe_managed_alloc!(RUNTIME_MEMORY_SIZE, CrateId::Runtime)?;
311327
BoundedVec::new(provider)?
312328
};
313329
for result_type in &func_type.results {

0 commit comments

Comments
 (0)