Skip to content

Commit e9f8a90

Browse files
authored
fixes a knowledge base race condition in the run plugin (#1347)
The run plugin was resetting the state of the toplevel knowledge base to the initial and effectively discarding the knowledge that was accumulated when the Program.t and Symtab.t were constructed as well discarding any information that might be added to the knowledge base in project passes. The run pass was capturing the state at the time when the Project.t is not fully ready, and at then end was using `Toplevel.set` to reset any accumualted knowledge. Effectively, this bug is a race condition, which we could prevent if the toplevel interface provided safe functions. This will be addressed in the next couple of pull requests (they will be more aggresive and change the semantics of several constructs so I decided to split them for this hotfix). Big thanks to @anwarmamat for providing a minimal reproducible example, without it would be nearly impossible to identify it.
1 parent 8a9bf35 commit e9f8a90

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

plugins/run/run_main.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -309,7 +309,6 @@ let find_first_unvisited_blk prog =
309309

310310
let main {Config.get=(!)} proj =
311311
let open Param in
312-
let state = Toplevel.current () in
313312
let run_until_visited = !until_visited in
314313
let enqueue_jobs = if !in_isolation
315314
then enqueue_separate_jobs else enqueue_super_job in
@@ -330,7 +329,8 @@ let main {Config.get=(!)} proj =
330329
~args:!argv ~envp:!envp
331330
~name:(Primus.Linker.Name.to_string p)
332331
~start:(exec p)) in
333-
let rec run proj state =
332+
let rec run proj =
333+
let state = Toplevel.current () in
334334
let result = Primus.Jobs.run ~on_failure ~on_success proj state in
335335
let state = Primus.Jobs.knowledge result in
336336
Toplevel.set state;
@@ -339,14 +339,14 @@ let main {Config.get=(!)} proj =
339339
if run_until_visited
340340
then match find_first_unvisited_sub prog with
341341
| Some sub ->
342-
enqueue_term sub; run proj state
342+
enqueue_term sub; run proj
343343
| None -> match find_first_unvisited_blk prog with
344344
| Some blk ->
345345
enqueue_term blk;
346-
run proj state
346+
run proj
347347
| None -> proj
348348
else proj in
349-
run proj state
349+
run proj
350350

351351
let deps = [
352352
"trivial-condition-form"

0 commit comments

Comments
 (0)