crux-mir: remove default initialValue for crucible::any::Any

crux-mir/src/Mir/Trans.hs

@@ -1525,6 +1525,10 @@ initialValue (CTyArray t) = tyToReprM t >>= \(Some tpr) -> case tpr of
 initialValue ty@(CTyBv _sz) = tyToReprM ty >>= \(Some tpr) -> case tpr of
     C.BVRepr w -> return $ Just $ MirExp (C.BVRepr w) $ S.app $ eBVLit w 0
     _ -> mirFail $ "Bv type " ++ show ty ++ " does not have BVRepr"
+-- `Any` values have no reasonable default.  Any default we provide might get
+-- muxed with actual non-default values, which will fail (unless the concrete
+-- type happens to match exactly).
+initialValue CTyAny = return Nothing
 initialValue CTyMethodSpec = return Nothing
 initialValue CTyMethodSpecBuilder = return Nothing
 

crux-mir/src/Mir/TransTy.hs

@@ -256,6 +256,7 @@ tyToReprM ty = do
 canInitialize :: M.Collection -> M.Ty -> Bool
 canInitialize col ty = case ty of
     -- Custom types
+    CTyAny -> False
     CTyMethodSpec -> False
     CTyMethodSpecBuilder -> False
 

crux-mir/test/symb_eval/any/conditional.good

@@ -0,0 +1,3 @@
+test conditional/3a1fbbbh::crux_test[0]: ok
+
+[Crux] Overall status: Valid.

crux-mir/test/symb_eval/any/conditional.rs

@@ -0,0 +1,16 @@
+//! Regression test for `Any`-typed locals under a symbolic branch.  Previously, this would mux the
+//! assigned value with the default value produced by `initialValue`, causing an error ("Attempted
+//! to mux ANY values of different runtime type").  Now `Any` no longer has a default value, so the
+//! error no longer occurs.
+#![feature(crucible_intrinsics)]
+extern crate crucible;
+use crucible::*;
+use crucible::any::Any;
+
+#[crux_test]
+fn crux_test() {
+    let mut x = bool::symbolic("x");
+    if x {
+        let y = Any::new(1);
+    }
+}

crux-mir/test/symb_eval/concretize/assert.good

@@ -7,8 +7,5 @@ failures:
 [Crux]   ./lib/crucible/lib.rs:47:17: 47:82 !test/symb_eval/concretize/assert.rs:10:5: 10:82: error: in assert/3a1fbbbh::crux_test[0]
 [Crux]   MIR assertion at test/symb_eval/concretize/assert.rs:10:5:
 [Crux]   	100 + 157 == 1
-[Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/concretize/assert.rs:11:16: 11:17: error: in assert/3a1fbbbh::crux_test[0]
-[Crux]   Unsupported feature: Attempted to mux ANY values of different runtime type StructRepr [BVRepr 8] IntrinsicRepr MirReference [BVRepr 8]
 
 [Crux] Overall status: Invalid.