From 2ea9f9e50361014a91520c1393dead29172e51e2 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 9 Feb 2021 18:28:22 -0800 Subject: [PATCH] Add a invalidation pass for pre-state allocations in jvm_verify. This ensures that executing an incomplete override, which omits some field modifications that are not mentioned in the override spec, will not lead to unsoundness. Fixes #900. --- intTests/test_jvm_unsound/test.saw | 23 +++++++-------- src/SAWScript/Crucible/JVM/Override.hs | 41 +++++++++++++++++++++++--- 2 files changed, 47 insertions(+), 17 deletions(-) diff --git a/intTests/test_jvm_unsound/test.saw b/intTests/test_jvm_unsound/test.saw index a8588a3830..d3ed007faf 100644 --- a/intTests/test_jvm_unsound/test.saw +++ b/intTests/test_jvm_unsound/test.saw @@ -8,6 +8,7 @@ enable_experimental; c <- java_load_class "Test"; +// An incomplete spec for method "set". let set_spec_1 = do { this <- jvm_alloc_object "Test"; @@ -16,6 +17,7 @@ let set_spec_1 = jvm_field_is this "b" (jvm_term x); }; +// Another incomplete spec for method "set". let set_spec_2 = do { this <- jvm_alloc_object "Test"; @@ -24,8 +26,8 @@ let set_spec_2 = jvm_static_field_is "a" (jvm_term x); }; -set_ov_1 <- jvm_unsafe_assume_spec c "set" set_spec_1; -set_ov_2 <- jvm_unsafe_assume_spec c "set" set_spec_2; +set_ov_1 <- jvm_verify c "set" [] false set_spec_1 z3; +set_ov_2 <- jvm_verify c "set" [] false set_spec_2 z3; let one = jvm_term {{ 1:[32] }}; let two = jvm_term {{ 2:[32] }}; @@ -44,6 +46,7 @@ jvm_verify c "test_a" [] false // An incorrect spec for test_a, which can be proven using the bogus // spec set_ov_1. +// FIXME: this should fail jvm_verify c "test_a" [set_ov_1] false do { this <- jvm_alloc_object "Test"; @@ -68,8 +71,9 @@ jvm_verify c "test_b" [] false } z3; -// An incorrect spec for test_b, which can be proven using the bogus -// spec set_ov_2. +// An incorrect spec for test_b, which would be provable using the +// incomplete spec set_ov_2, if not for the memory invalidation pass. +fails ( jvm_verify c "test_b" [set_ov_2] false do { this <- jvm_alloc_object "Test"; @@ -80,12 +84,5 @@ jvm_verify c "test_b" [set_ov_2] false jvm_field_is this "b" one; jvm_return one; } - z3; - -// It should be impossible to verify the bogus set_spec_1. -// FIXME: this should fail -jvm_verify c "set" [] false set_spec_1 z3; - -// It should be impossible to verify the bogus set_spec_2. -// FIXME: this should fail -jvm_verify c "set" [] false set_spec_2 z3; + z3 +); diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs index dad0b0c6a5..1d4b9c90cc 100644 --- a/src/SAWScript/Crucible/JVM/Override.hs +++ b/src/SAWScript/Crucible/JVM/Override.hs @@ -308,13 +308,13 @@ methodSpecHandler_prestate opts sc cc args cs = -- which involves writing values into memory, computing the return value, -- and computing postcondition predicates. methodSpecHandler_poststate :: - forall ret w. + forall ret. Options {- ^ output/verbosity options -} -> SharedContext {- ^ context for constructing SAW terms -} -> JVMCrucibleContext {- ^ context for interacting with Crucible -} -> Crucible.TypeRepr ret {- ^ type representation of function return value -} -> CrucibleMethodSpecIR {- ^ specification for current function override -} -> - OverrideMatcher CJ.JVM w (Crucible.RegValue Sym ret) + OverrideMatcher CJ.JVM RW (Crucible.RegValue Sym ret) methodSpecHandler_poststate opts sc cc retTy cs = do executeCond opts sc cc cs (cs ^. MS.csPostState) computeReturnValue opts cc sc cs retTy (cs ^. MS.csRetValue) @@ -354,16 +354,17 @@ enforceCompleteSubstitution loc ss = unless (null missing) (failure loc (AmbiguousVars missing)) --- execute a pre/post condition +-- | Execute a post condition. executeCond :: Options -> SharedContext -> JVMCrucibleContext -> CrucibleMethodSpecIR -> StateSpec -> - OverrideMatcher CJ.JVM w () + OverrideMatcher CJ.JVM RW () executeCond opts sc cc cs ss = do refreshTerms sc ss + invalidateAllocs cc cs traverse_ (executeAllocation opts cc) (Map.assocs (ss ^. MS.csAllocs)) traverse_ (executePointsTo opts sc cc cs) (ss ^. MS.csPointsTos) traverse_ (executeSetupCondition opts sc cc cs) (ss ^. MS.csConditions) @@ -764,6 +765,38 @@ learnPred sc cc loc prepost t = ------------------------------------------------------------------------ +-- | Invalidate all memory that was allocated in the method spec +-- precondition using either @jvm_alloc_object@ or @jvm_alloc_array@. +invalidateAllocs :: + JVMCrucibleContext -> + MS.CrucibleMethodSpecIR CJ.JVM -> + OverrideMatcher CJ.JVM RW () +invalidateAllocs cc cs = + do let allocs = cs ^. MS.csPreState . MS.csAllocs + void $ Map.traverseWithKey invalidateAlloc allocs + where + invalidateAlloc :: AllocIndex -> (W4.ProgramLoc, Allocation) -> OverrideMatcher CJ.JVM RW () + invalidateAlloc i (_loc, alloc) = + do sym <- Ov.getSymInterface + globals <- OM (use overrideGlobals) + ref <- resolveAllocIndexJVM i + -- TODO: annotate the value with a descriptive error message. + let val = CJ.unassignedJVMValue + case alloc of + AllocObject cName -> + do let jc = cc ^. jccJVMContext + let fids = CJ.fieldsOfClassName jc cName + let clear g fid = liftIO $ CJ.doFieldStore sym g ref fid val + globals' <- foldM clear globals fids + OM (overrideGlobals .= globals') + AllocArray len _ty -> + do let idxs = take len [0..] + let clear g idx = liftIO $ CJ.doArrayStore sym g ref idx val + globals' <- foldM clear globals idxs + OM (overrideGlobals .= globals') + +------------------------------------------------------------------------ + -- TODO: replace (W4.ProgramLoc, J.Type) by some allocation datatype -- that includes constructors for object allocations and array -- allocations (with length).