AbortResult has two ways to represent a call to exit

[langston-barrett]

Compare:

crucible/crucible/src/Lang/Crucible/Simulator/ExecutionTree.hs

Lines 232 to 233 in 8021814

	-- | An aborted execution that was ended by a call to 'exit'.
	AbortedExit ::

to

crucible/crucible/src/Lang/Crucible/Simulator/ExecutionTree.hs

Lines 226 to 228 in 8021814

	-- | A single aborted execution with the execution state at time of the abort and the reason.
	AbortedExec ::
	!AbortExecReason ->

with

crucible/crucible/src/Lang/Crucible/Backend.hs

Lines 135 to 137 in 8021814

	| EarlyExit ProgramLoc
	-- ^ We invoked a function which ends the current thread of execution
	-- (e.g., @abort()@ or @exit(1)@).

We should decide on a single, unambiguous way to represent calls to exit or abort.

In fact, we may want to consider a more general mechanism. There are many (often language-specific) ways for a process/thread/unit of execution to abort/exit/end. For example, LLVM has llvm.trap:

crucible/crucible-llvm/src/Lang/Crucible/LLVM/Intrinsics/LLVM.hs

Line 455 in 8021814

liftIO $ addFailedAssertion bak $ AssertFailureSimError "llvm.trap() called" "")

The pattern at the moment is to use AbortExecReason.AssertionFailure for these more language-specific conditions.

So, we are left with a few options:

1. Simply eliminate one of the above constructors, changing all uses to the other
2. Eliminate both of the above constructors, use AssertionFailure to represent all early exit states
3. Parameterize AbortExecReason over ext (the language extension) and provide a type family over ext that resolves to an enumeration of the language-specific early exit reasons

If we pick (1), we would want to decide between:

a. Specifying that this constructor only represents calls to the exit system call, and so must provide an ExitCode
b. Generalize the constructor to all kinds of early exits, but provide more flexible data alongside it, such as a String or Dynamic

I'm partial to (3), but it might not be feasible.

[RyanGlScott]

I suspect that there may be subtle differences in behavior among these options. For instance, adding an AssertionFailure on its own won't cause the current thread of execution to stop—you have to do something else on top of that for that to happen (see #789). I'm not sure off the top of my head what the difference between AbortedExit and AbortedExec is off the top of my head, but I wouldn't be surprised if it were similarly nuanced.

I think it would be helpful to characterize what each option does before we make a choice about which option to use.

[kquick]

It looks like AbortedExec is intended to be used in broader cases for resuming on a different symbolic branch point, whereas AbortedExit is intended for exit(). See https://github.com/GaloisInc/crucible/blob/master/crucible/src/Lang/Crucible/Simulator/Operations.hs#L678-L680 and its uses. This seems like a significant semantic difference.

[langston-barrett]

For instance, adding an AssertionFailure on its own won't cause the current thread of execution to stop

...unless the assertion is added via addFailedAssertion (rather than, e.g., assert (falsePred sym)), as it is in e.g., llvm.trap, in which case AbortExecReason has a different constructor for that:

crucible/crucible/src/Lang/Crucible/Backend.hs

Lines 128 to 129 in 8021814

	| AssertionFailure SimError
	-- ^ An assertion concretely failed.

whereas AbortedExit is intended for exit().

Both AbortedExec (EarlyExit loc) and AbortedExit are documented as representing calls to exit, hence my confusion (see the Haddocks in the original post).

I think it would be helpful to characterize what each option does before we make a choice about which option to use.

Yeah, I find this a bit confusing. Here are some places the treatment/description of these two options differs:

crucible/crucible/src/Lang/Crucible/Simulator/Operations.hs

Lines 678 to 680 in 8021814

	-- | Abort the current execution and roll back to the nearest
	-- symbolic branch point.
	abortExec ::

crucible/crucible/src/Lang/Crucible/Simulator/OverrideSim.hs

Lines 156 to 160 in 8021814

	-- | Exit from the current execution by ignoring the continuation
	-- and immediately returning an aborted execution result.
	exitExecution :: IsSymInterface sym => ExitCode -> OverrideSim p sym ext rtp args r a
	exitExecution ec = Sim $ StateContT $ \_c s ->
	return $ ResultState $ AbortedResult (s^.stateContext) (AbortedExit ec)

crucible/crucible/src/Lang/Crucible/Simulator/Operations.hs

Lines 122 to 130 in 8021814

	mergeAbortedResult ::
	ProgramLoc {- ^ Program location of control-flow branching -} ->
	Pred sym {- ^ Branch predicate -} ->
	AbortedResult sym ext ->
	AbortedResult sym ext ->
	AbortedResult sym ext
	mergeAbortedResult _ _ (AbortedExit ec) _ = AbortedExit ec
	mergeAbortedResult _ _ _ (AbortedExit ec) = AbortedExit ec
	mergeAbortedResult loc pred q r = AbortedBranch loc pred q r

It appears that:

• Using AbortExecReason (of which EarlyExit is one) via abortExec results in calling resumeValueFromFrameAbort, which attempts other branches
• Using AbortedExit via exitExecution does not attempt other branches

It's worth noting that exitExecution is the only place in crucible that constructs an AbortedExit, and it is for use in OverrideSim (not an internal simulator operation), and is not called elsewhere within crucible. In fact, it is not called elsewhere within this repo, nor indeed anywhere that I can find.