logicaffeine_compile/concurrency/
classify.rs1use std::collections::{HashMap, HashSet};
17
18use crate::analysis::callgraph::calls_in_stmts;
19use crate::ast::stmt::{Expr, SelectBranch, Stmt};
20use crate::intern::Symbol;
21
22use super::model::{direct_nondet_witnesses, Determinacy, NondetKind, NondetWitness};
23
24pub fn classify_program(stmts: &[Stmt]) -> Determinacy {
26 let mut witnesses = Vec::new();
27 for stmt in stmts {
28 collect_witnesses_stmt(stmt, &mut witnesses);
29 }
30 collect_concurrent_print(stmts, &mut witnesses);
33 if witnesses.is_empty() {
34 Determinacy::Determinate
35 } else {
36 Determinacy::Nondeterminate { witnesses }
37 }
38}
39
40fn collect_witnesses_stmt(stmt: &Stmt, out: &mut Vec<NondetWitness>) {
41 direct_nondet_witnesses(stmt, out);
43 match stmt {
45 Stmt::If { then_block, else_block, .. } => {
46 for s in *then_block {
47 collect_witnesses_stmt(s, out);
48 }
49 if let Some(eb) = else_block {
50 for s in *eb {
51 collect_witnesses_stmt(s, out);
52 }
53 }
54 }
55 Stmt::While { body, .. }
56 | Stmt::Repeat { body, .. }
57 | Stmt::Zone { body, .. }
58 | Stmt::FunctionDef { body, .. } => {
59 for s in *body {
60 collect_witnesses_stmt(s, out);
61 }
62 }
63 Stmt::Concurrent { tasks } | Stmt::Parallel { tasks } => {
64 for s in *tasks {
65 collect_witnesses_stmt(s, out);
66 }
67 }
68 Stmt::Inspect { arms, .. } => {
69 for arm in arms.iter() {
70 for s in arm.body.iter() {
71 collect_witnesses_stmt(s, out);
72 }
73 }
74 }
75 Stmt::Select { branches } => {
76 for branch in branches {
77 match branch {
78 SelectBranch::Receive { body, .. } | SelectBranch::Timeout { body, .. } => {
79 for s in body.iter() {
80 collect_witnesses_stmt(s, out);
81 }
82 }
83 }
84 }
85 }
86 _ => {}
87 }
88}
89
90fn collect_concurrent_print(stmts: &[Stmt], out: &mut Vec<NondetWitness>) {
102 let mut fn_bodies: HashMap<Symbol, &[Stmt]> = HashMap::new();
104 for_each_stmt(stmts, &mut |s| {
105 if let Stmt::FunctionDef { name, body, .. } = s {
106 fn_bodies.insert(*name, body);
107 }
108 });
109
110 let direct_show_fns: HashSet<Symbol> = fn_bodies
113 .iter()
114 .filter(|(_, body)| block_directly_shows(body))
115 .map(|(name, _)| *name)
116 .collect();
117
118 let fn_prints = |start: Symbol| -> bool {
121 let mut stack = vec![start];
122 let mut seen = HashSet::new();
123 while let Some(g) = stack.pop() {
124 if !seen.insert(g) {
125 continue;
126 }
127 if direct_show_fns.contains(&g) {
128 return true;
129 }
130 if let Some(body) = fn_bodies.get(&g) {
131 stack.extend(calls_in_stmts(body));
132 }
133 }
134 false
135 };
136
137 let mut printers = 0usize;
138
139 if block_directly_shows(stmts) || calls_in_stmts(stmts).into_iter().any(&fn_prints) {
142 printers += 1;
143 }
144
145 let mut launch_targets: Vec<Symbol> = Vec::new();
147 for_each_stmt(stmts, &mut |s| match s {
148 Stmt::LaunchTask { function, .. } | Stmt::LaunchTaskWithHandle { function, .. } => {
149 launch_targets.push(*function)
150 }
151 _ => {}
152 });
153 for f in launch_targets {
154 if printers >= 2 {
155 break;
156 }
157 if fn_prints(f) {
158 printers += 1;
159 }
160 }
161
162 if printers < 2 {
165 let mut blocks: Vec<&[Stmt]> = Vec::new();
166 for_each_stmt(stmts, &mut |s| {
167 if let Stmt::Concurrent { tasks } | Stmt::Parallel { tasks } = s {
168 blocks.push(tasks);
169 }
170 });
171 printers += blocks.iter().map(|b| count_shows(b)).sum::<usize>();
172 }
173
174 if printers >= 2 {
175 out.push(NondetWitness { kind: NondetKind::ConcurrentPrint });
176 }
177}
178
179fn for_each_stmt<'a>(stmts: &'a [Stmt<'a>], f: &mut impl FnMut(&'a Stmt<'a>)) {
181 for s in stmts {
182 f(s);
183 match s {
184 Stmt::If { then_block, else_block, .. } => {
185 for_each_stmt(then_block, f);
186 if let Some(eb) = else_block {
187 for_each_stmt(eb, f);
188 }
189 }
190 Stmt::While { body, .. }
191 | Stmt::Repeat { body, .. }
192 | Stmt::Zone { body, .. }
193 | Stmt::FunctionDef { body, .. } => for_each_stmt(body, f),
194 Stmt::Concurrent { tasks } | Stmt::Parallel { tasks } => for_each_stmt(tasks, f),
195 Stmt::Inspect { arms, .. } => {
196 for arm in arms.iter() {
197 for_each_stmt(arm.body, f);
198 }
199 }
200 Stmt::Select { branches } => {
201 for branch in branches {
202 match branch {
203 SelectBranch::Receive { body, .. } | SelectBranch::Timeout { body, .. } => {
204 for_each_stmt(body, f)
205 }
206 }
207 }
208 }
209 _ => {}
210 }
211 }
212}
213
214fn block_directly_shows(stmts: &[Stmt]) -> bool {
218 stmts.iter().any(stmt_directly_shows)
219}
220
221fn stmt_directly_shows(stmt: &Stmt) -> bool {
222 match stmt {
223 Stmt::Show { .. } => true,
224 Stmt::If { then_block, else_block, .. } => {
225 block_directly_shows(then_block)
226 || else_block.map_or(false, |eb| block_directly_shows(eb))
227 }
228 Stmt::While { body, .. } | Stmt::Repeat { body, .. } | Stmt::Zone { body, .. } => {
229 block_directly_shows(body)
230 }
231 Stmt::Inspect { arms, .. } => arms.iter().any(|arm| block_directly_shows(arm.body)),
232 Stmt::Select { branches } => branches.iter().any(|branch| match branch {
233 SelectBranch::Receive { body, .. } | SelectBranch::Timeout { body, .. } => {
234 block_directly_shows(body)
235 }
236 }),
237 _ => false,
238 }
239}
240
241fn count_shows(stmts: &[Stmt]) -> usize {
243 let mut n = 0;
244 for_each_stmt(stmts, &mut |s| {
245 if matches!(s, Stmt::Show { .. }) {
246 n += 1;
247 }
248 });
249 n
250}
251
252pub fn branches_independent(tasks: &[Stmt]) -> bool {
260 let infos: Vec<BranchInfo> = tasks.iter().map(BranchInfo::of).collect();
261 for i in 0..infos.len() {
262 for j in (i + 1)..infos.len() {
263 if infos[i].conflicts_with(&infos[j]) {
264 return false;
265 }
266 }
267 }
268 true
269}
270
271pub fn branches_share_mutable_state(tasks: &[Stmt]) -> bool {
281 let infos: Vec<BranchInfo> = tasks.iter().map(BranchInfo::of).collect();
282 for i in 0..infos.len() {
283 for j in (i + 1)..infos.len() {
284 if infos[i].shares_mutable_state_with(&infos[j]) {
285 return true;
286 }
287 }
288 }
289 false
290}
291
292#[derive(Default)]
293struct BranchInfo {
294 writes: HashSet<Symbol>,
296 refs: HashSet<Symbol>,
298 pipes: HashSet<Symbol>,
300}
301
302impl BranchInfo {
303 fn of(stmt: &Stmt) -> Self {
304 let mut info = BranchInfo::default();
305 info.scan_stmt(stmt);
306 info
307 }
308
309 fn conflicts_with(&self, other: &BranchInfo) -> bool {
310 !self.pipes.is_disjoint(&other.pipes) || self.shares_mutable_state_with(other)
311 }
312
313 fn shares_mutable_state_with(&self, other: &BranchInfo) -> bool {
316 !self.writes.is_disjoint(&other.writes)
317 || !self.writes.is_disjoint(&other.refs)
318 || !other.writes.is_disjoint(&self.refs)
319 }
320
321 fn scan_stmt(&mut self, stmt: &Stmt) {
322 match stmt {
323 Stmt::Let { value, .. } => self.scan_expr(value),
324 Stmt::Set { target, value } => {
325 self.writes.insert(*target);
326 self.scan_expr(value);
327 }
328 Stmt::Push { collection, value } | Stmt::Add { collection, value } | Stmt::Remove { collection, value } => {
329 self.note_mutated(collection);
330 self.scan_expr(value);
331 }
332 Stmt::Pop { collection, .. } => self.note_mutated(collection),
333 Stmt::SetIndex { collection, index, value } => {
334 self.note_mutated(collection);
335 self.scan_expr(index);
336 self.scan_expr(value);
337 }
338 Stmt::Show { object, .. } => self.scan_expr(object),
339 Stmt::Return { value } => {
340 if let Some(v) = value {
341 self.scan_expr(v);
342 }
343 }
344 Stmt::Call { args, .. } => {
345 for a in args.iter() {
346 self.scan_expr(a);
347 }
348 }
349 Stmt::LaunchTask { args, .. } | Stmt::LaunchTaskWithHandle { args, .. } => {
350 for a in args.iter() {
351 self.scan_expr(a);
352 }
353 }
354 Stmt::SendPipe { value, pipe } | Stmt::TrySendPipe { value, pipe, .. } => {
355 self.note_pipe(pipe);
356 self.scan_expr(value);
357 }
358 Stmt::ReceivePipe { pipe, .. } | Stmt::TryReceivePipe { pipe, .. } => {
359 self.note_pipe(pipe);
360 }
361 Stmt::If { cond, then_block, else_block } => {
362 self.scan_expr(cond);
363 for s in *then_block {
364 self.scan_stmt(s);
365 }
366 if let Some(eb) = else_block {
367 for s in *eb {
368 self.scan_stmt(s);
369 }
370 }
371 }
372 Stmt::While { cond, body, .. } => {
373 self.scan_expr(cond);
374 for s in *body {
375 self.scan_stmt(s);
376 }
377 }
378 Stmt::Repeat { iterable, body, .. } => {
379 self.scan_expr(iterable);
380 for s in *body {
381 self.scan_stmt(s);
382 }
383 }
384 Stmt::Zone { body, .. } => {
385 for s in *body {
386 self.scan_stmt(s);
387 }
388 }
389 _ => {}
390 }
391 }
392
393 fn note_mutated(&mut self, collection: &Expr) {
394 if let Some(root) = root_symbol(collection) {
395 self.writes.insert(root);
396 }
397 }
398
399 fn note_pipe(&mut self, pipe: &Expr) {
400 if let Expr::Identifier(sym) = pipe {
401 self.pipes.insert(*sym);
402 }
403 }
404
405 fn scan_expr(&mut self, expr: &Expr) {
406 match expr {
407 Expr::Identifier(sym) => {
408 self.refs.insert(*sym);
409 }
410 Expr::BinaryOp { left, right, .. } => {
411 self.scan_expr(left);
412 self.scan_expr(right);
413 }
414 Expr::Call { args, .. } => {
415 for a in args.iter() {
416 self.scan_expr(a);
417 }
418 }
419 Expr::CallExpr { callee, args } => {
420 self.scan_expr(callee);
421 for a in args.iter() {
422 self.scan_expr(a);
423 }
424 }
425 Expr::Index { collection, index } => {
426 self.scan_expr(collection);
427 self.scan_expr(index);
428 }
429 Expr::FieldAccess { object, .. } => self.scan_expr(object),
430 Expr::Length { collection } => self.scan_expr(collection),
431 Expr::Not { operand } => self.scan_expr(operand),
432 Expr::List(items) | Expr::Tuple(items) => {
433 for i in items.iter() {
434 self.scan_expr(i);
435 }
436 }
437 _ => {}
438 }
439 }
440}
441
442fn root_symbol(expr: &Expr) -> Option<Symbol> {
444 match expr {
445 Expr::Identifier(sym) => Some(*sym),
446 Expr::FieldAccess { object, .. } => root_symbol(object),
447 Expr::Index { collection, .. } => root_symbol(collection),
448 _ => None,
449 }
450}