True processes in symbolic mode

[mgree]

Core problem: the symbolic process model is inadequate.

The variable $$ isn't currently installed in a symbolic shell, but PPID is. Trickiness: $$ is unchanged in subshells, which can signal the top-level. We need to carefully hold on to such signals.

It's not currently possible for symbolic shells to send signals to themselves---including SIGPIPE, which leads to a wrong execution of the following two programs:

while true; do echo 5; done | true
while true; do echo 5; done | { read x; echo $((x + 42)) ; }

The first should terminate immediately; the second should print 47 and terminate. Right now neither loop ever stops, because the first process in either pipeline never receives the SIGPIPE.

Plan (checked means done in local branch sigpipe):

• Check readers in symbolic_write_fd
• Add process entry for top-level shell
• Each shell process has an status : maybe nat (of a possible exit status) and pending : list signal and stepped : bool
• Stepping sets stepped
• Symbolic state has curpid representing current thread of execution
• Symbolic system calls require that curpid is a live thread, otherwise immediate abort of call
• Sending a signal mutates shell process state. Set status on, e.g., uncaught SIGPIPE
• Implement os_pending_signal for symbolic mode
• Tests for pending signals in symbolic mode
• Tracer looks up pid 0 each time and steps it (with a cascade of curpid updates)
• Tracer finds pids that weren't stepped and steps them
• Update visualization
  • Change shim.ml to send over the full OS state, including the proc list
  • Render all of the live procs side by side, collapsing all but the main shell and the active proc

[mgree]

• need to check in about the KLUDGE at os_symbolic.lem:277 for the exit trap
• something to show exit_code in the shtepper