Skip to content

Commit c60c428

Browse files
danwtdanwt
authored
Fix parser, powerset domains, and compound var aliases#11
Fix parser, powerset domains, and compound var aliases
2 parents 3293292 + 1a51f34 commit c60c428

8 files changed

Lines changed: 104 additions & 15 deletions

File tree

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,7 @@ pub fn check_bmc(
5757
locals: Vec::new(),
5858
compound_locals: Vec::new(),
5959
set_locals: Vec::new(),
60+
whole_var_locals: Vec::new(),
6061
};
6162

6263
let inv_encoded = enc.encode_bool(&inv.body)?;

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

Lines changed: 80 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,9 @@ pub struct EncoderCtx<'a> {
2727
/// Set locals: maps absolute locals stack position → concrete set members.
2828
/// Used for powerset quantifier bindings where the local represents a concrete subset.
2929
pub set_locals: Vec<(usize, Vec<i64>)>,
30+
/// Whole-var locals: locals that alias an entire compound variable.
31+
/// Each entry: (abs_depth, var_idx, step).
32+
pub whole_var_locals: Vec<(usize, usize, usize)>,
3033
}
3134

3235
impl<'a> EncoderCtx<'a> {
@@ -136,6 +139,27 @@ impl<'a> EncoderCtx<'a> {
136139
self.compound_locals.pop();
137140
self.locals.pop();
138141
result
142+
} else if let CompiledExpr::Var(var_idx)
143+
| CompiledExpr::PrimedVar(var_idx) = value.as_ref()
144+
{
145+
// Bare compound variable alias (e.g., inlined function arg)
146+
let step = if matches!(value.as_ref(), CompiledExpr::Var(_)) {
147+
self.current_step
148+
} else {
149+
self.next_step
150+
};
151+
let entry = &self.layout.entries[*var_idx];
152+
if entry.kind.z3_var_count() > 1 {
153+
let abs_depth = self.locals.len();
154+
self.locals.push(Dynamic::from_ast(&Int::from_i64(0)));
155+
self.whole_var_locals.push((abs_depth, *var_idx, step));
156+
let result = self.encode(body);
157+
self.whole_var_locals.pop();
158+
self.locals.pop();
159+
return result;
160+
}
161+
// Re-raise the original error
162+
self.encode(value).and_then(|_| unreachable!())
139163
} else {
140164
// Re-raise the original error
141165
self.encode(value).and_then(|_| unreachable!())
@@ -547,10 +571,13 @@ impl<'a> EncoderCtx<'a> {
547571
domain: &CompiledExpr,
548572
predicate: &CompiledExpr,
549573
) -> SymbolicResult<Dynamic> {
550-
let (lo, hi) = self.extract_range(domain)?;
551-
// Build ITE chain: if P(lo) then lo else if P(lo+1) then lo+1 else ... else lo
552-
let mut result = Dynamic::from_ast(&Int::from_i64(lo)); // default fallback
553-
for val in (lo..=hi).rev() {
574+
let values = self.resolve_domain_values(domain)?;
575+
// Build ITE chain: if P(first) then first else if P(second) then second else ... else first
576+
let fallback = *values
577+
.first()
578+
.ok_or_else(|| SymbolicError::Encoding("empty domain in choose".into()))?;
579+
let mut result = Dynamic::from_ast(&Int::from_i64(fallback));
580+
for val in values.into_iter().rev() {
554581
let z3_val = Dynamic::from_ast(&Int::from_i64(val));
555582
self.locals.push(z3_val);
556583
let pred = self.encode_bool(predicate)?;
@@ -589,6 +616,12 @@ impl<'a> EncoderCtx<'a> {
589616
{
590617
return self.encode_compound_local_chain(var_idx, step, &key_z3, &keys);
591618
}
619+
// Whole-var alias: redirect to the original compound variable
620+
if let Some((var_idx, step)) = self.resolve_whole_var_local(*local_idx) {
621+
let entry = &self.layout.entries[var_idx];
622+
let z3_vars = &self.step_vars[step][var_idx];
623+
return self.resolve_index_chain(&entry.kind, z3_vars, &keys);
624+
}
592625
}
593626

594627
let (specl_var_idx, step) = self.extract_var_step(current)?;
@@ -855,12 +888,12 @@ impl<'a> EncoderCtx<'a> {
855888
filter,
856889
} = inner
857890
{
858-
let (lo, hi) = self.extract_range(domain)?;
891+
let values = self.resolve_domain_values(domain)?;
859892
let one = Int::from_i64(1);
860893
let zero = Int::from_i64(0);
861894
let mut sum_terms = Vec::new();
862895

863-
for val in lo..=hi {
896+
for val in values {
864897
let z3_val = Dynamic::from_ast(&Int::from_i64(val));
865898
self.locals.push(z3_val);
866899
let included = if let Some(f) = filter {
@@ -872,7 +905,11 @@ impl<'a> EncoderCtx<'a> {
872905
sum_terms.push(included.ite(&one, &zero));
873906
}
874907

875-
Ok(Dynamic::from_ast(&Int::add(&sum_terms)))
908+
if sum_terms.is_empty() {
909+
Ok(Dynamic::from_ast(&Int::from_i64(0)))
910+
} else {
911+
Ok(Dynamic::from_ast(&Int::add(&sum_terms)))
912+
}
876913
} else {
877914
match inner {
878915
CompiledExpr::Var(idx) | CompiledExpr::PrimedVar(idx) => {
@@ -1043,11 +1080,18 @@ impl<'a> EncoderCtx<'a> {
10431080
domain,
10441081
filter,
10451082
} => {
1046-
let (lo, hi) = self.extract_range(domain)?;
1083+
let values = self.resolve_domain_values(domain)?;
10471084
let elem_z3 = self.encode_int(elem)?;
1048-
let lo_z3 = Int::from_i64(lo);
1049-
let hi_z3 = Int::from_i64(hi);
1050-
let in_domain = Bool::and(&[elem_z3.ge(&lo_z3), elem_z3.le(&hi_z3)]);
1085+
let eqs: Vec<Bool> = values
1086+
.iter()
1087+
.map(|v| elem_z3.eq(&Int::from_i64(*v)))
1088+
.collect();
1089+
let eq_refs: Vec<&Bool> = eqs.iter().collect();
1090+
let in_domain = if eq_refs.is_empty() {
1091+
Bool::from_bool(false)
1092+
} else {
1093+
Bool::or(&eq_refs)
1094+
};
10511095

10521096
let result = if let Some(f) = filter {
10531097
let elem_encoded = self.encode(elem)?;
@@ -1354,6 +1398,18 @@ impl<'a> EncoderCtx<'a> {
13541398
None
13551399
}
13561400

1401+
/// Check if a Local(idx) resolves to a whole-variable alias.
1402+
/// Returns (var_idx, step) if so.
1403+
fn resolve_whole_var_local(&self, local_idx: usize) -> Option<(usize, usize)> {
1404+
let abs_idx = self.locals.len() - 1 - local_idx;
1405+
for &(abs_depth, var_idx, step) in self.whole_var_locals.iter().rev() {
1406+
if abs_depth == abs_idx {
1407+
return Some((var_idx, step));
1408+
}
1409+
}
1410+
None
1411+
}
1412+
13571413
/// Resolve nested len for a compound local: len(Local(n)[k1][k2]...).
13581414
fn encode_compound_local_nested_len(
13591415
&mut self,
@@ -1677,9 +1733,9 @@ impl<'a> EncoderCtx<'a> {
16771733
domain,
16781734
filter,
16791735
} => {
1680-
let (dom_lo, dom_hi) = self.extract_range(domain)?;
1736+
let values = self.resolve_domain_values(domain)?;
16811737
let mut flags = vec![Bool::from_bool(false); count];
1682-
for val in dom_lo..=dom_hi {
1738+
for val in values {
16831739
let offset = (val - lo) as usize;
16841740
if offset >= count {
16851741
continue;
@@ -1764,6 +1820,17 @@ impl<'a> EncoderCtx<'a> {
17641820
}
17651821
}
17661822

1823+
/// Resolve a domain to concrete values, handling both Range and set-local domains.
1824+
fn resolve_domain_values(&mut self, domain: &CompiledExpr) -> SymbolicResult<Vec<i64>> {
1825+
if let CompiledExpr::Local(idx) = domain {
1826+
if let Some(members) = self.resolve_set_local(*idx) {
1827+
return Ok(members.clone());
1828+
}
1829+
}
1830+
let (lo, hi) = self.extract_range(domain)?;
1831+
Ok((lo..=hi).collect())
1832+
}
1833+
17671834
pub fn extract_range(&mut self, domain: &CompiledExpr) -> SymbolicResult<(i64, i64)> {
17681835
match domain {
17691836
CompiledExpr::Range { lo, hi } => {

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,7 @@ pub fn check_ic3(
9898
locals: Vec::new(),
9999
compound_locals: Vec::new(),
100100
set_locals: Vec::new(),
101+
whole_var_locals: Vec::new(),
101102
};
102103
let inv_encoded = enc.encode_bool(&inv.body)?;
103104
let inv_raw = inv_encoded.get_z3_ast();

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,7 @@ pub fn check_inductive(
5050
locals: Vec::new(),
5151
compound_locals: Vec::new(),
5252
set_locals: Vec::new(),
53+
whole_var_locals: Vec::new(),
5354
};
5455
let inv_at_0 = enc0.encode_bool(&inv.body)?;
5556
solver.assert(&inv_at_0);
@@ -64,6 +65,7 @@ pub fn check_inductive(
6465
locals: Vec::new(),
6566
compound_locals: Vec::new(),
6667
set_locals: Vec::new(),
68+
whole_var_locals: Vec::new(),
6769
};
6870
let inv_at_1 = enc1.encode_bool(&inv.body)?;
6971
solver.assert(&inv_at_1.not());

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,7 @@ fn check_base_case(
7878
locals: Vec::new(),
7979
compound_locals: Vec::new(),
8080
set_locals: Vec::new(),
81+
whole_var_locals: Vec::new(),
8182
};
8283
let inv_encoded = enc.encode_bool(&inv.body)?;
8384
solver.assert(&inv_encoded.not());
@@ -151,6 +152,7 @@ fn check_inductive_step(
151152
locals: Vec::new(),
152153
compound_locals: Vec::new(),
153154
set_locals: Vec::new(),
155+
whole_var_locals: Vec::new(),
154156
};
155157
let inv_at_step = enc.encode_bool(&inv.body)?;
156158
solver.assert(&inv_at_step);
@@ -167,6 +169,7 @@ fn check_inductive_step(
167169
locals: Vec::new(),
168170
compound_locals: Vec::new(),
169171
set_locals: Vec::new(),
172+
whole_var_locals: Vec::new(),
170173
};
171174
let inv_at_k = enc_k.encode_bool(&inv.body)?;
172175
solver.assert(&inv_at_k.not());

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -122,6 +122,7 @@ fn guard_satisfied(
122122
locals: Vec::new(),
123123
compound_locals: Vec::new(),
124124
set_locals: Vec::new(),
125+
whole_var_locals: Vec::new(),
125126
};
126127

127128
let Ok(guard) = enc.encode_bool(&action.guard) else {

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,7 @@ fn encode_init_expr(
6868
locals: Vec::new(),
6969
compound_locals: Vec::new(),
7070
set_locals: Vec::new(),
71+
whole_var_locals: Vec::new(),
7172
};
7273
let constraint = enc.encode_bool(expr)?;
7374
solver.assert(&constraint);
@@ -90,6 +91,7 @@ fn encode_init_expr(
9091
locals: Vec::new(),
9192
compound_locals: Vec::new(),
9293
set_locals: Vec::new(),
94+
whole_var_locals: Vec::new(),
9395
};
9496
let constraint = enc.encode_bool(expr)?;
9597
solver.assert(&constraint);
@@ -121,6 +123,7 @@ fn encode_init_assignment(
121123
locals: Vec::new(),
122124
compound_locals: Vec::new(),
123125
set_locals: Vec::new(),
126+
whole_var_locals: Vec::new(),
124127
};
125128
let rhs_z3 = enc.encode(rhs)?;
126129
if let (Some(vi), Some(ri)) = (z3_vars[0].as_int(), rhs_z3.as_int()) {
@@ -151,6 +154,7 @@ fn encode_init_assignment(
151154
locals: Vec::new(),
152155
compound_locals: Vec::new(),
153156
set_locals: Vec::new(),
157+
whole_var_locals: Vec::new(),
154158
};
155159
let k_val = Dynamic::from_ast(&Int::from_i64(k));
156160
enc.locals.push(k_val);
@@ -188,6 +192,7 @@ fn encode_init_assignment(
188192
locals: Vec::new(),
189193
compound_locals: Vec::new(),
190194
set_locals: Vec::new(),
195+
whole_var_locals: Vec::new(),
191196
};
192197
let key_val = enc.extract_concrete_int_helper(key_expr)?;
193198
let offset = (key_val - key_lo) as usize;
@@ -219,6 +224,7 @@ fn encode_init_assignment(
219224
locals: Vec::new(),
220225
compound_locals: Vec::new(),
221226
set_locals: Vec::new(),
227+
whole_var_locals: Vec::new(),
222228
};
223229
let flags = enc.encode_as_set(rhs, *lo, *hi)?;
224230
for (i, flag) in flags.iter().enumerate() {
@@ -238,6 +244,7 @@ fn encode_init_assignment(
238244
locals: Vec::new(),
239245
compound_locals: Vec::new(),
240246
set_locals: Vec::new(),
247+
whole_var_locals: Vec::new(),
241248
};
242249
match rhs {
243250
CompiledExpr::SeqLit(elems) => {
@@ -437,6 +444,7 @@ fn encode_action(
437444
locals: Vec::new(),
438445
compound_locals: Vec::new(),
439446
set_locals: Vec::new(),
447+
whole_var_locals: Vec::new(),
440448
};
441449

442450
let guard = enc.encode_bool(&action.guard)?;
@@ -465,6 +473,7 @@ fn encode_action(
465473
locals: Vec::new(),
466474
compound_locals: Vec::new(),
467475
set_locals: Vec::new(),
476+
whole_var_locals: Vec::new(),
468477
};
469478

470479
let guard = enc.encode_bool(&action.guard)?;
@@ -514,6 +523,7 @@ fn encode_effect(
514523
locals: Vec::new(),
515524
compound_locals: Vec::new(),
516525
set_locals: Vec::new(),
526+
whole_var_locals: Vec::new(),
517527
};
518528

519529
encode_effect_expr(&action.effect, &mut enc, layout, step_vars, step)

‎specl/crates/specl-syntax/src/parser.rs‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -618,8 +618,12 @@ impl Parser {
618618
},
619619
span,
620620
);
621-
} else if self.match_token(TokenKind::LParen) {
622-
// Function call
621+
} else if self.check(TokenKind::LParen)
622+
&& matches!(expr.kind, ExprKind::Ident(_) | ExprKind::Field { .. })
623+
{
624+
// Function call — only after identifiers and field accesses.
625+
// Without this guard, `10\n(x = x+1)` would parse as `10(x = x+1)`.
626+
self.advance();
623627
let args = self.parse_call_args()?;
624628
self.expect(TokenKind::RParen)?;
625629
let span = expr.span.merge(self.prev_span());

0 commit comments

Comments
 (0)