From 4c5b9042b6fa1130c69d359d7f000204a7a5e477 Mon Sep 17 00:00:00 2001 From: Langston Barrett Date: Fri, 9 Aug 2024 11:37:56 -0400 Subject: [PATCH] llvm: Fix validity predicate for memory reads with symbolic block numbers Previously, this case returned the concretely-true predicate. This is incorrect, as `isAllocatedGeneric` takes an argument `inAlloc`, which is supposed to be applied to the `AllocInfo` of the allocation with the matching block number, as it is in the other branch. Mea culpa, looks like I introduced this bug long ago. re: UC-Crux tests. It looks to me like what's happening is that UC-Crux previously found certain errors in each of these test cases that were adequately handled by its heuristics. Fixing this predicate introduces a new kind of error, and the heuristics aren't sophisticated enough to deal with this one. UC-Crux then gives up, saying it's not sure how to avoid these errors with a new precondition (leaving them "unclassified"). This is unfortunate, but UC-Crux already can't abduce preconditions for a wide variety of programs, so I don't consider this a blocker. --- .../src/Lang/Crucible/LLVM/MemModel/MemLog.hs | 7 +---- uc-crux-llvm/test/Test.hs | 27 ++++++++++++++----- 2 files changed, 21 insertions(+), 13 deletions(-) diff --git a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs index 5317528b5..282db1e89 100644 --- a/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs +++ b/crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs @@ -252,12 +252,7 @@ isAllocatedGeneric sym inAlloc blk = go (pure (falsePred sym)) (pure (truePred s Just True -> -- This is where where this block was allocated, and it -- couldn't have been freed before it was allocated. - -- - -- NOTE(lb): It's not clear to me that this branch is - -- reachable: If the equality test can succeed - -- concretely, wouldn't asNat have returned a Just - -- above? In either case, this answer should be sound. - return (truePred sym, truePred sym) + (, truePred sym) <$> inAlloc ba Just False -> k Nothing -> do (fallback', fallbackFreed') <- k diff --git a/uc-crux-llvm/test/Test.hs b/uc-crux-llvm/test/Test.hs index 4a9c17526..7222d74f9 100644 --- a/uc-crux-llvm/test/Test.hs +++ b/uc-crux-llvm/test/Test.hs @@ -291,6 +291,19 @@ _isUnannotated fn (Result.SomeBugfindingResult' (Result.SomeBugfindingResult _ r Text.unpack (Result.printFunctionSummary (Result.summary result)) ] +isUnfixable :: String -> SomeBugfindingResult' -> IO () +isUnfixable fn (Result.SomeBugfindingResult' (Result.SomeBugfindingResult _ result _)) = + do + let (_missingAnn, _failedAssert, _unimpl, _unclass, _unfixed, unfixable, _timeouts) = + partitionUncertainty (Result.uncertainResults result) + 0 < length unfixable + TH.@? unwords + [ "Expected", + fn, + "to be unfixable but the result was:\n", + Text.unpack (Result.printFunctionSummary (Result.summary result)) + ] + _hasFailedAssert :: String -> SomeBugfindingResult' -> IO () _hasFailedAssert fn (Result.SomeBugfindingResult' (Result.SomeBugfindingResult _ result _)) = do @@ -462,22 +475,16 @@ inFileTests = ("deref_arg_const_index.c", [("deref_arg_const_index", isSafeWithPreconditions mempty DidntHitBounds)]), ("deref_struct_field.c", [("deref_struct_field", isSafeWithPreconditions mempty DidntHitBounds)]), ("do_free.c", [("do_free", isSafeWithPreconditions mempty DidntHitBounds)]), - ("free_dict.c", [("free_dict", isSafeWithPreconditions mempty DidHitBounds)]), - ("free_dict_kv.c", [("free_dict_kv", isSafeWithPreconditions mempty DidHitBounds)]), - ("free_linked_list.c", [("free_linked_list", isSafeWithPreconditions mempty DidHitBounds)]), ("gethostname_arg_ptr.c", [("gethostname_arg_ptr", isSafeWithPreconditions (unsoundOverride "gethostname") DidntHitBounds)]), - ("linked_list_sum.c", [("linked_list_sum", isSafeWithPreconditions mempty DidHitBounds)]), ("lots_of_loops.c", [("lots_of_loops", isSafeWithPreconditions mempty DidHitBounds)]), ("memset_const_len.c", [("memset_const_len", isSafeWithPreconditions mempty DidntHitBounds)]), ("memset_const_len_arg_byte.c", [("memset_const_len_arg_byte", isSafeWithPreconditions mempty DidntHitBounds)]), - ("mutually_recursive_linked_list_sum.c", [("mutually_recursive_linked_list_sum", isSafeWithPreconditions mempty DidHitBounds)]), ("not_double_free.c", [("not_double_free", isSafeWithPreconditions mempty DidntHitBounds)]), ("ptr_as_array.c", [("ptr_as_array", isSafeWithPreconditions mempty DidntHitBounds)]), ("read_errno.c", [("read_errno", isSafeWithPreconditions (skipOverride "__errno_location") DidntHitBounds)]), ("read_pointer_from_global_struct.c", [("read_pointer_from_global_struct", isSafeWithPreconditions mempty DidntHitBounds)]), ("read_null_global_pointer.c", [("read_null_global_pointer", isSafeWithPreconditions mempty DidntHitBounds)]), ("sized_array_arg.c", [("sized_array_arg", isSafeWithPreconditions mempty DidntHitBounds)]), - ("struct_with_array.c", [("struct_with_array", isSafeWithPreconditions mempty DidntHitBounds)]), ("writes_to_arg.c", [("writes_to_arg", isSafeWithPreconditions mempty DidntHitBounds)]), ("writes_to_arg_conditional.c", [("writes_to_arg_conditional", isSafeWithPreconditions mempty DidntHitBounds)]), ("writes_to_arg_conditional_ptr.c", [("writes_to_arg_conditional_ptr", isSafeWithPreconditions mempty DidntHitBounds)]), @@ -490,10 +497,15 @@ inFileTests = ("unsized_array.c", [("unsized_array", isSafeWithPreconditions mempty DidntHitBounds)]), ("cast_float_to_pointer_free.c", [("cast_float_to_pointer_free", isUnclassified)]), ("cast_float_to_pointer_write.c", [("cast_float_to_pointer_write", isUnclassified)]), + ("free_dict.c", [("free_dict", isUnclassified)]), -- goal: isSafeWP + ("free_dict_kv.c", [("free_dict_kv", isUnclassified)]), -- goal: isSafeWP + ("free_linked_list.c", [("free_linked_list", isUnclassified)]), -- goal: isSafeWP ("free_with_offset.c", [("free_with_offset", isUnclassified)]), -- goal: hasBugs + ("linked_list_sum.c", [("linked_list_sum", isUnclassified)]), -- goal: isSafeWP ("memset_arg_len.c", [("memset_arg_len", isUnclassified)]), -- goal: isSafeWP ("memset_func_ptr.c", [("memset_func_ptr", isUnclassified)]), -- goal: hasBugs ("memset_void_ptr.c", [("memset_void_ptr", isUnclassified)]), -- goal: isSafeWP + ("mutually_recursive_linked_list_sum.c", [("mutually_recursive_linked_list_sum", isUnclassified)]), -- goal: isSafeWP ("nested_structs.c", [("nested_structs", isUnclassified)]), -- goal: ??? ("oob_read_heap.c", [("oob_read_heap", isUnclassified)]), -- goal: hasBugs ("oob_read_stack.c", [("oob_read_stack", isUnclassified)]), -- goal: hasBugs @@ -502,6 +514,7 @@ inFileTests = ("signed_add_wrap_concrete.c", [("signed_add_wrap_concrete", isUnclassified)]), -- goal: hasBugs ("signed_mul_wrap_concrete.c", [("signed_mul_wrap_concrete", isUnclassified)]), -- goal: hasBugs ("signed_sub_wrap_concrete.c", [("signed_sub_wrap_concrete", isUnclassified)]), -- goal: hasBugs + ("struct_with_array.c", [("struct_with_array", isUnclassified)]), -- goal: isSafeWP ("write_const_global.c", [("write_const_global", isUnclassified)]), -- goal: hasBugs ("use_after_free.c", [("use_after_free", isUnclassified)]), -- goal: hasBugs -- @@ -514,7 +527,7 @@ inFileTests = ("compare_ptrs_different_heap_allocs.c", [("compare_ptrs_different_heap_allocs", hasMissingAnn)]), -- goal: hasBugs ("compare_ptrs_different_stack_allocs.c", [("compare_ptrs_different_stack_allocs", hasMissingAnn)]), -- goal: hasBugs ("memcpy_const_len.c", [("memcpy_const_len", hasMissingAnn)]), - ("deref_arg_arg_index.c", [("deref_arg_arg_index", hasMissingAnn)]), + ("deref_arg_arg_index.c", [("deref_arg_arg_index", isUnfixable)]), -- This one could use an override. Currently fails because it's -- skipped, and so unreachable code gets reached. ("do_exit.c", [("do_exit", hasMissingAnn)]), -- goal: isSafe