Skip to content

Commit ced868d

Browse files
danwtdanwt
committed
claude: fix(symbolic): improve error handling and Z3 failure messages
1 parent e351278 commit ced868d

9 files changed

Lines changed: 198 additions & 84 deletions

File tree

‎specl/crates/specl-symbolic/src/bmc.rs‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ pub fn check_bmc(
7373
match solver.check() {
7474
SatResult::Sat => {
7575
info!(invariant = inv.name, depth = k, "invariant violation found");
76-
let model = solver.get_model().expect("SAT result must have model");
76+
let model = crate::get_model_or_err(&solver)?;
7777
let trace = extract_trace(&model, &layout, &all_step_vars, spec, consts, k);
7878
return Ok(SymbolicOutcome::InvariantViolation {
7979
invariant: inv.name.clone(),
@@ -84,9 +84,10 @@ pub fn check_bmc(
8484
SatResult::Unknown => {
8585
solver.pop(1);
8686
return Ok(SymbolicOutcome::Unknown {
87-
reason: format!(
88-
"Z3 returned unknown at depth {} for invariant '{}'",
89-
k, inv.name
87+
reason: crate::unknown_reason(
88+
&format!("BMC at depth {k}"),
89+
&inv.name,
90+
timeout_ms,
9091
),
9192
});
9293
}

‎specl/crates/specl-symbolic/src/encoder.rs‎

Lines changed: 74 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -365,7 +365,9 @@ impl<'a> EncoderCtx<'a> {
365365
BinOp::Eq => self.encode_eq(left, right),
366366
BinOp::Ne => {
367367
let eq = self.encode_eq(left, right)?;
368-
let eq_bool = eq.as_bool().unwrap();
368+
let eq_bool = eq.as_bool().ok_or_else(|| {
369+
SymbolicError::Encoding("!= comparison: equality did not produce Bool".into())
370+
})?;
369371
Ok(Dynamic::from_ast(&eq_bool.not()))
370372
}
371373
BinOp::Lt => {
@@ -859,10 +861,15 @@ impl<'a> EncoderCtx<'a> {
859861
VarKind::ExplodedSet { .. } => {
860862
let one = Int::from_i64(1);
861863
let zero = Int::from_i64(0);
862-
let terms: Vec<Int> = vars
863-
.iter()
864-
.map(|v| v.as_bool().unwrap().ite(&one, &zero))
865-
.collect();
864+
let mut terms = Vec::with_capacity(vars.len());
865+
for v in vars {
866+
let b = v.as_bool().ok_or_else(|| {
867+
SymbolicError::Encoding(
868+
"set length: expected Bool Z3 variable for set element".into(),
869+
)
870+
})?;
871+
terms.push(b.ite(&one, &zero));
872+
}
866873
Ok(Dynamic::from_ast(&Int::add(&terms)))
867874
}
868875
VarKind::ExplodedDict { key_lo, key_hi, .. } => {
@@ -967,10 +974,15 @@ impl<'a> EncoderCtx<'a> {
967974
let z3_vars = &self.step_vars[step][*idx];
968975
let one = Int::from_i64(1);
969976
let zero = Int::from_i64(0);
970-
let terms: Vec<Int> = z3_vars
971-
.iter()
972-
.map(|v| v.as_bool().unwrap().ite(&one, &zero))
973-
.collect();
977+
let mut terms = Vec::with_capacity(z3_vars.len());
978+
for v in z3_vars {
979+
let b = v.as_bool().ok_or_else(|| {
980+
SymbolicError::Encoding(
981+
"set len: expected Bool Z3 variable".into(),
982+
)
983+
})?;
984+
terms.push(b.ite(&one, &zero));
985+
}
974986
Ok(Dynamic::from_ast(&Int::add(&terms)))
975987
}
976988
VarKind::ExplodedSeq { .. } => {
@@ -1078,7 +1090,11 @@ impl<'a> EncoderCtx<'a> {
10781090
if let Some(concrete_elem) = self.try_concrete_int(elem) {
10791091
let offset = (concrete_elem - lo) as usize;
10801092
let result = if offset < z3_vars.len() {
1081-
z3_vars[offset].as_bool().unwrap()
1093+
z3_vars[offset].as_bool().ok_or_else(|| {
1094+
SymbolicError::Encoding(
1095+
"set membership: expected Bool for set element".into(),
1096+
)
1097+
})?
10821098
} else {
10831099
Bool::from_bool(false)
10841100
};
@@ -1087,7 +1103,11 @@ impl<'a> EncoderCtx<'a> {
10871103
} else {
10881104
let elem_z3 = self.encode_int(elem)?;
10891105
let result = Self::build_ite_chain(&elem_z3, z3_vars, lo)?;
1090-
let result_bool = result.as_bool().unwrap();
1106+
let result_bool = result.as_bool().ok_or_else(|| {
1107+
SymbolicError::Encoding(
1108+
"set membership: ITE chain did not produce Bool".into(),
1109+
)
1110+
})?;
10911111
let final_val = if negate {
10921112
result_bool.not()
10931113
} else {
@@ -1328,7 +1348,11 @@ impl<'a> EncoderCtx<'a> {
13281348
if let Some(concrete_elem) = self.try_concrete_int(elem) {
13291349
let offset = (concrete_elem - lo) as usize;
13301350
let result = if offset < set_vars.len() {
1331-
set_vars[offset].as_bool().unwrap()
1351+
set_vars[offset].as_bool().ok_or_else(|| {
1352+
SymbolicError::Encoding(
1353+
"nested set membership: expected Bool".into(),
1354+
)
1355+
})?
13321356
} else {
13331357
Bool::from_bool(false)
13341358
};
@@ -1337,7 +1361,11 @@ impl<'a> EncoderCtx<'a> {
13371361
} else {
13381362
let elem_z3 = self.encode_int(elem)?;
13391363
let result = Self::build_ite_chain(&elem_z3, set_vars, lo)?;
1340-
let result_bool = result.as_bool().unwrap();
1364+
let result_bool = result.as_bool().ok_or_else(|| {
1365+
SymbolicError::Encoding(
1366+
"nested set membership: ITE chain did not produce Bool".into(),
1367+
)
1368+
})?;
13411369
let final_val = if negate {
13421370
result_bool.not()
13431371
} else {
@@ -1370,7 +1398,12 @@ impl<'a> EncoderCtx<'a> {
13701398
let z3_vars: Vec<Dynamic> =
13711399
flags.iter().map(|b| Dynamic::from_ast(b)).collect();
13721400
let result = Self::build_ite_chain(&elem_z3, &z3_vars, lo)?;
1373-
let result_bool = result.as_bool().unwrap();
1401+
let result_bool = result.as_bool().ok_or_else(|| {
1402+
SymbolicError::Encoding(
1403+
"set expression membership: ITE chain did not produce Bool"
1404+
.into(),
1405+
)
1406+
})?;
13741407
let final_val = if negate {
13751408
result_bool.not()
13761409
} else {
@@ -1673,8 +1706,12 @@ impl<'a> EncoderCtx<'a> {
16731706

16741707
let mut conjuncts = Vec::new();
16751708
// len equality
1676-
let l_len = l_vars[0].as_int().unwrap();
1677-
let r_len = r_vars[0].as_int().unwrap();
1709+
let l_len = l_vars[0].as_int().ok_or_else(|| {
1710+
SymbolicError::Encoding("seq equality: left seq len is not Int".into())
1711+
})?;
1712+
let r_len = r_vars[0].as_int().ok_or_else(|| {
1713+
SymbolicError::Encoding("seq equality: right seq len is not Int".into())
1714+
})?;
16781715
conjuncts.push(l_len.eq(&r_len));
16791716
// element equality (for all positions up to max_len)
16801717
for i in 0..max_len {
@@ -1750,7 +1787,16 @@ impl<'a> EncoderCtx<'a> {
17501787
_ => self.next_step,
17511788
};
17521789
let z3_vars = &self.step_vars[step][*idx];
1753-
Ok(z3_vars.iter().map(|v| v.as_bool().unwrap()).collect())
1790+
z3_vars
1791+
.iter()
1792+
.map(|v| {
1793+
v.as_bool().ok_or_else(|| {
1794+
SymbolicError::Encoding(
1795+
"encode_as_set: expected Bool Z3 variable for set element".into(),
1796+
)
1797+
})
1798+
})
1799+
.collect::<SymbolicResult<Vec<_>>>()
17541800
}
17551801
CompiledExpr::SetLit(elements) => {
17561802
let mut flags = vec![Bool::from_bool(false); count];
@@ -2074,13 +2120,13 @@ pub fn assert_range_constraints(
20742120
fn assert_var_range(solver: &Solver, kind: &VarKind, z3_vars: &[Dynamic]) {
20752121
match kind {
20762122
VarKind::Int { lo, hi } => {
2077-
if let Some(lo) = lo {
2078-
let z3_lo = Int::from_i64(*lo);
2079-
solver.assert(z3_vars[0].as_int().unwrap().ge(&z3_lo));
2080-
}
2081-
if let Some(hi) = hi {
2082-
let z3_hi = Int::from_i64(*hi);
2083-
solver.assert(z3_vars[0].as_int().unwrap().le(&z3_hi));
2123+
if let Some(int_var) = z3_vars.first().and_then(|v| v.as_int()) {
2124+
if let Some(lo) = lo {
2125+
solver.assert(int_var.ge(Int::from_i64(*lo)));
2126+
}
2127+
if let Some(hi) = hi {
2128+
solver.assert(int_var.le(Int::from_i64(*hi)));
2129+
}
20842130
}
20852131
}
20862132
VarKind::ExplodedDict {
@@ -2097,9 +2143,10 @@ fn assert_var_range(solver: &Solver, kind: &VarKind, z3_vars: &[Dynamic]) {
20972143
}
20982144
VarKind::ExplodedSeq { max_len, elem_kind } => {
20992145
// len bounded: 0 <= len <= max_len
2100-
let len_var = z3_vars[0].as_int().unwrap();
2101-
solver.assert(len_var.ge(Int::from_i64(0)));
2102-
solver.assert(len_var.le(Int::from_i64(*max_len as i64)));
2146+
if let Some(len_var) = z3_vars.first().and_then(|v| v.as_int()) {
2147+
solver.assert(len_var.ge(Int::from_i64(0)));
2148+
solver.assert(len_var.le(Int::from_i64(*max_len as i64)));
2149+
}
21032150
// Element range constraints
21042151
let elem_stride = elem_kind.z3_var_count();
21052152
for i in 0..*max_len {

‎specl/crates/specl-symbolic/src/golem.rs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -139,9 +139,9 @@ fn run_golem_with_timeout(
139139
if std::time::Instant::now() >= deadline {
140140
let _ = child.kill();
141141
let _ = child.wait();
142-
return Err(crate::SymbolicError::Internal(format!(
143-
"Golem timed out after {}ms for invariant '{}'",
144-
ms, inv_name
142+
return Err(crate::SymbolicError::Z3(format!(
143+
"Golem timed out after {ms}ms for invariant '{inv_name}'. \
144+
Consider increasing --timeout or using --bfs instead."
145145
)));
146146
}
147147
std::thread::sleep(std::time::Duration::from_millis(100));

‎specl/crates/specl-symbolic/src/ic3.rs‎

Lines changed: 9 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -292,10 +292,17 @@ pub fn check_ic3(
292292
reason = reason,
293293
"IC3 returned unknown"
294294
);
295+
let timeout_hint = if timeout_ms.is_some() {
296+
" Consider increasing --timeout or"
297+
} else {
298+
" Consider setting --timeout or"
299+
};
295300
return Ok(SymbolicOutcome::Unknown {
296301
reason: format!(
297-
"IC3 returned unknown for invariant '{}': {}",
298-
inv.name, reason
302+
"IC3/Spacer returned unknown for invariant '{}': {}.{} \
303+
using --bfs for explicit-state exploration, or trying \
304+
a different --spacer-profile.",
305+
inv.name, reason, timeout_hint
299306
),
300307
});
301308
}

‎specl/crates/specl-symbolic/src/inductive.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ pub fn check_inductive(
9393
match solver.check() {
9494
SatResult::Sat => {
9595
info!(invariant = inv.name, "invariant is NOT inductive");
96-
let model = solver.get_model().expect("SAT result must have model");
96+
let model = crate::get_model_or_err(&solver)?;
9797
let trace = extract_trace(&model, &layout, &all_step_vars, spec, consts, 1);
9898
return Ok(SymbolicOutcome::InvariantViolation {
9999
invariant: inv.name.clone(),
@@ -106,7 +106,7 @@ pub fn check_inductive(
106106
SatResult::Unknown => {
107107
solver.pop(1);
108108
return Ok(SymbolicOutcome::Unknown {
109-
reason: format!("Z3 returned unknown for invariant '{}'", inv.name),
109+
reason: crate::unknown_reason("inductive check", &inv.name, timeout_ms),
110110
});
111111
}
112112
}

‎specl/crates/specl-symbolic/src/k_induction.rs‎

Lines changed: 10 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ fn check_base_case(
112112
match solver.check() {
113113
SatResult::Sat => {
114114
info!(invariant = inv.name, depth, "base case violation found");
115-
let model = solver.get_model().expect("SAT result must have model");
115+
let model = crate::get_model_or_err(&solver)?;
116116
let trace = extract_trace(&model, layout, &all_step_vars, spec, consts, depth);
117117
return Ok(Some(SymbolicOutcome::InvariantViolation {
118118
invariant: inv.name.clone(),
@@ -123,9 +123,10 @@ fn check_base_case(
123123
SatResult::Unknown => {
124124
solver.pop(1);
125125
return Ok(Some(SymbolicOutcome::Unknown {
126-
reason: format!(
127-
"Z3 returned unknown at base depth {} for invariant '{}'",
128-
depth, inv.name
126+
reason: crate::unknown_reason(
127+
&format!("k-induction base case at depth {depth}"),
128+
&inv.name,
129+
timeout_ms,
129130
),
130131
}));
131132
}
@@ -227,7 +228,7 @@ fn check_inductive_step_with_cti(
227228
match solver.check() {
228229
SatResult::Sat => {
229230
info!(invariant = inv.name, k, cti_iter, "extracting CTI");
230-
let model = solver.get_model().expect("SAT result must have model");
231+
let model = crate::get_model_or_err(&solver)?;
231232

232233
// Extract state at step k-1 (last assumption step)
233234
let equalities =
@@ -288,9 +289,10 @@ fn check_inductive_step_with_cti(
288289
solver.pop(1);
289290
return Ok(KInductionResult {
290291
outcome: SymbolicOutcome::Unknown {
291-
reason: format!(
292-
"Z3 returned unknown for k-induction step for invariant '{}'",
293-
inv.name
292+
reason: crate::unknown_reason(
293+
&format!("k-induction step (k={k})"),
294+
&inv.name,
295+
timeout_ms,
294296
),
295297
},
296298
cti_lemmas,

‎specl/crates/specl-symbolic/src/lib.rs‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,28 @@ pub(crate) fn apply_solver_timeout(solver: &Solver, timeout_ms: Option<u64>) {
3131
}
3232
}
3333

34+
/// Extract model from solver after SAT result, with proper error handling.
35+
pub(crate) fn get_model_or_err(solver: &Solver) -> SymbolicResult<z3::Model> {
36+
solver.get_model().ok_or_else(|| {
37+
SymbolicError::Z3(
38+
"solver returned SAT but no model is available (possible Z3 internal error)".into(),
39+
)
40+
})
41+
}
42+
43+
/// Build an actionable Unknown reason from a Z3 "unknown" result.
44+
pub(crate) fn unknown_reason(context: &str, invariant: &str, timeout_ms: Option<u64>) -> String {
45+
let timeout_hint = if timeout_ms.is_some() {
46+
" Consider increasing --timeout or"
47+
} else {
48+
" Consider setting --timeout or"
49+
};
50+
format!(
51+
"Z3 returned unknown for {context} on invariant '{invariant}'.{timeout_hint} \
52+
using --bfs for explicit-state exploration instead."
53+
)
54+
}
55+
3456
/// Symbolic checking error.
3557
#[derive(Debug, Error)]
3658
pub enum SymbolicError {
@@ -40,6 +62,9 @@ pub enum SymbolicError {
4062
#[error("encoding error: {0}")]
4163
Encoding(String),
4264

65+
#[error("Z3 solver error: {0}")]
66+
Z3(String),
67+
4368
#[error("internal error: {0}")]
4469
Internal(String),
4570
}

‎specl/crates/specl-symbolic/src/portfolio.rs‎

Lines changed: 2 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -232,7 +232,6 @@ pub fn check_portfolio(
232232
let overall_timeout = timeout_ms.unwrap_or(300_000); // 5 min default
233233
let deadline = std::time::Instant::now() + Duration::from_millis(overall_timeout);
234234

235-
let mut first_ok = None;
236235
let mut reasons = Vec::new();
237236
let mut received = 0;
238237

@@ -250,14 +249,8 @@ pub fn check_portfolio(
250249
}
251250
Ok(StrategyResult::Done(outcome @ SymbolicOutcome::Ok { .. })) => {
252251
done.store(true, Ordering::Relaxed);
253-
if first_ok.is_none() {
254-
first_ok = Some(outcome);
255-
}
256-
// Found a proof — return immediately (other strategies are hinted to stop)
257-
if let Some(ok) = first_ok {
258-
info!("portfolio: property proven");
259-
return Ok(ok);
260-
}
252+
info!("portfolio: property proven");
253+
return Ok(outcome);
261254
}
262255
Ok(StrategyResult::Done(SymbolicOutcome::Unknown { reason })) => {
263256
reasons.push(reason);
@@ -276,11 +269,6 @@ pub fn check_portfolio(
276269
received += 1;
277270
}
278271

279-
if let Some(ok) = first_ok {
280-
info!("portfolio: property proven");
281-
return Ok(ok);
282-
}
283-
284272
Ok(SymbolicOutcome::Unknown {
285273
reason: format!("all strategies inconclusive: {}", reasons.join("; ")),
286274
})

0 commit comments

Comments
 (0)