Suspicious code in LLVM.ResolveSetupValue.resolveSAWPred

[RyanGlScott]

During a code review, @eddywestbrook noticed this part of SAWScript.Crucible.LLVM.ResolveSetupValue.resolveSAWPred:

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

Lines 734 to 740 in e0e94c6

	(_,tm') <- rewriteSharedTerm sc ss tm
	mx <- case getAllExts tm' of
	-- concretely evaluate if it is a closed term
	[] -> do modmap <- scGetModuleMap sc
	let v = Concrete.evalSharedTerm modmap mempty mempty tm
	pure (Just (Concrete.toBool v))
	_ -> return Nothing

We make an effort to rewrite tm into tm', but immediately afterwards we call evalSharedTerm on tm, not tm'. This seems very suspicious. I don't have a test case on hand to verify that this would introduce bugs, but I bet you could construct one with enough cleverness.

[eddywestbrook]

@andreistefanescu Do you have any insight here? I haven't done enough complex SAW proofs to generate a useful test case for this potential change.

[andreistefanescu]

I don't think this is a bug. tm' is used to check that the term is ground in getAllExts tm'. evalSharedTerm should evaluate both tm and tm' to the same concrete value. Of course, I would need to look at the code more to be sure.

[andreistefanescu]

this is the definition of basic_ss

saw-script/src/SAWScript/Prover/Rewrite.hs

Lines 21 to 68 in e0e94c6

	basic_ss :: SharedContext -> IO (Simpset a)
	basic_ss sc =
	do rs1 <- concat <$> traverse (defRewrites sc) defs
	rs2 <- scEqsRewriteRules sc eqs
	return $ addConvs procs (addRules (rs1 ++ rs2) emptySimpset)
	where
	eqs = map (mkIdent preludeName)
	[ "unsafeCoerce_same"
	, "not_not"
	, "true_implies"
	, "implies__eq"
	, "and_True1"
	, "and_False1"
	, "and_True2"
	, "and_False2"
	, "and_idem"
	, "or_True1"
	, "or_False1"
	, "or_True2"
	, "or_False2"
	, "or_idem"
	, "not_True"
	, "not_False"
	, "not_or"
	, "not_and"
	, "ite_true"
	, "ite_false"
	, "ite_not"
	, "ite_nest1"
	, "ite_nest2"
	, "ite_fold_not"
	, "ite_eq"
	, "ite_true"
	, "ite_false"
	, "or_triv1"
	, "and_triv1"
	, "or_triv2"
	, "and_triv2"
	, "bvAddZeroL"
	, "bvAddZeroR"
	, "bveq_sameL"
	, "bveq_sameR"
	, "bveq_same2"
	, "bvNat_bvToNat"
	]
	defs = map (mkIdent (mkModuleName ["Cryptol"])) ["seq", "ecEq", "ecNotEq"]
	procs = [tupleConversion, recordConversion] ++
	bvConversions ++ natConversions ++ vecConversions

Those simplifications can eliminate variables, such as true || x + 1 == x rewrites to true. I don't know if Concrete.evalSharedTerm handles that via laziness. Either way, I don't see any reason not to switch to tm'. If we do that, let's make the change for JVM and MIR as well.

[RyanGlScott]

If we do that, let's make the change for JVM and MIR as well.

FWIW, this code doesn't exist in the JVM backend, since it doesn't do any of this evalSharedTerm business for whatever reason. (Perhaps it should.)

[RyanGlScott]

Fixed in #2037.