Support ghost values in all language backends

[RyanGlScott]

This patch:

• Factors out the machinery needed to track ghost state into the SAWScript.Crucible.Common.Override and SAWScript.Builtins modules. Nothing about ghost state is specific to any language backend, so it deserves to live in a non-LLVM–specific location.
• Adds jvm_ghost_value and mir_ghost_value commands, which behave exactly like the LLVM backend's llvm_ghost_value command does, but for the JVM and MIR backends, respectively.
• Adds a test_mir_ghost test case in SAWScript and the remote API to ensure that everything works as expected.

Fixes #1929.

[RyanGlScott]

Documentation-related changes involving ghost state.

[RyanGlScott]

A test case involving ghost state in the SAW MIR backend.

[RyanGlScott]

@qsctr discovered that SAW will panic when it attempts to combine MIR ghost state with symbolic branching. Here is a small example which triggers the issue:

// Meant to be overridden
pub fn f(_x: u32) {}

pub fn g(b: bool) {
    if b {
        f(27)
    } else {
        f(42)
    }
}

enable_experimental;

m <- mir_load_module "test.linked-mir.json";

g <- declare_ghost_state "g";

let f_spec = do {
    x <- mir_fresh_var "x" mir_u32;

    mir_execute_func [mir_term x];

    mir_ghost_value g x;
};

let g_spec = do {
    b <- mir_fresh_var "b" mir_bool;

    mir_execute_func [mir_term b];

    mir_ghost_value g ({{ if b then 27 else 42 : [32] }});
};

f_ov <- mir_unsafe_assume_spec m "test::f" f_spec;
mir_verify m "test::g" [f_ov] false g_spec z3;

$ ./bin/saw test.saw



[13:41:31.524] Loading file "/home/ryanscott/Documents/Hacking/Haskell/saw-script/test.saw"
[13:41:31.552] Verifying test/40fac751::g[0] ...
[13:41:31.561] Simulating test/40fac751::g[0] ...
[13:41:31.561] Matching 1 overrides of  test/40fac751::f[0] ...
[13:41:31.561] Branching on 1 override variants of test/40fac751::f[0] ...
[13:41:31.561] Applied override! test/40fac751::f[0]
[13:41:31.562] Matching 1 overrides of  test/40fac751::f[0] ...
[13:41:31.562] Branching on 1 override variants of test/40fac751::f[0] ...
[13:41:31.562] Applied override! test/40fac751::f[0]
[13:41:31.562] You have encountered a bug in Crucible's implementation.
*** Please create an issue at https://github.com/GaloisInc/crucible/issues

%< --------------------------------------------------- 
  Revision:  c19fc2c53851cdd162ae1ccca14032467e3c2fd1
  Branch:    HEAD
  Location:  RegMap.muxRegForType
  Message:   Unknown intrinsic type:
             *** Name: GhostValue
CallStack (from HasCallStack):
  panic, called at src/Lang/Crucible/Panic.hs:11:9 in crucible-0.6-inplace:Lang.Crucible.Panic
  panic, called at src/Lang/Crucible/Simulator/RegMap.hs:252:12 in crucible-0.6-inplace:Lang.Crucible.Simulator.RegMap
%< ---------------------------------------------------

The reason that this does not happen in the LLVM backend is because we add the GhostValue intrinsic on top of the default LLVM intrinsics here:

saw-script/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

Lines 254 to 259 in 0202016

	intrinsics :: MapF.MapF Crucible.SymbolRepr (Crucible.IntrinsicMuxFn Sym)
	intrinsics =
	MapF.insert
	(Crucible.knownSymbol :: Crucible.SymbolRepr MS.GhostValue)
	Crucible.IntrinsicMuxFn
	CL.llvmIntrinsicTypes

We need to do something similar for the JVM and MIR backends.

[RyanGlScott]

The issue in #1958 (comment) is fixed as of 276a54b.

[qsctr]

Looks good, thanks. It's a bit unfortunate that we have to duplicate some more code across the 3 backends, hopefully one day that can be addressed with a solution to #379.