From 2e249bff5c28524bc0ea9406e061471b91ba40b4 Mon Sep 17 00:00:00 2001 From: Owen Carey <37121709+owenthcarey@users.noreply.github.com> Date: Mon, 5 Oct 2026 16:49:19 -0700 Subject: [PATCH 1/6] feat!: inline shadow guards and confirmed errors Implements RFC 0034 (docs/rfcs/0034-fast-enforcement.md), which amends RFCs 0032 and 0033: the model (prove, check, guard, record) stays and each part becomes cheaper. - Guards are declared calls that LLVM passes canonicalize, merge and expand into inline checks against a whole-address-space shadow (one byte per 16-byte granule, with exact encodings for stack and global objects); range caches and the inline guard bodies are deleted. - A local is registered only where a guard can reach it; library calls whose need no term states go through checked wrappers. - A definite error fails the build only when a path replay confirms it; unconfirmed candidates are warnings. - The analysis is bounded by a work budget per run and per unit, plus memory caps; the transfer-count budgets are gone. - Term arithmetic is exact over long long, clamped only at its result, and stack objects write their shadow a run at a time. Gates (amendment 16): F1, F3, F4 met; F2 met but for opus's build time; F5 and F7 carried forward. 725 cases pass in plain, --asan and --checks verify runs; 48 blind programs added (test/cases/detection-blind). BREAKING CHANGE: -fweavec-budget and -fweavec-unit-budget now count analysis work instead of CFG block transfers (defaults 20,000,000 per run and 400 per site, at least 20,000,000, per unit); a definite error that its replay does not confirm is a warning; the guard helpers are declarations the backend lowers, so the prelude and libweavec_chk.a change with the runtime. --- .clang-tidy | 5 + AGENTS.md | 8 +- README.md | 16 +- docs/architecture.md | 139 +- docs/pages/guides/adoption.md | 6 +- docs/pages/guides/build-integration.md | 2 +- docs/pages/reference/cli.md | 74 +- docs/pages/reference/compatibility.md | 2 +- docs/pages/reference/guarantees.md | 20 +- docs/pages/reference/troubleshooting.md | 8 +- docs/rfcs/0034-fast-enforcement.md | 1063 +++++++++ docs/rfcs/README.md | 1 + docs/roadmap.md | 38 +- include/weavec/Analysis/LedgerAdapter.h | 15 + include/weavec/Core/CheckPlan.h | 22 +- include/weavec/Core/Heap.h | 19 +- include/weavec/Core/Ledger.h | 19 +- include/weavec/Core/LibrarySpec.h | 26 + include/weavec/Frontend/CheckEmitter.h | 29 +- include/weavec/Frontend/GuardPasses.h | 88 + include/weavec/Frontend/ObjectRegistration.h | 14 +- lib/Analysis/CheckPlanner.cpp | 145 +- lib/Analysis/Engine.h | 74 +- lib/Analysis/EngineCalls.cpp | 99 +- lib/Analysis/EngineDecide.cpp | 122 +- lib/Analysis/EngineExpr.cpp | 26 +- lib/Analysis/EngineLibrary.cpp | 28 +- lib/Analysis/EngineLifetimes.cpp | 27 +- lib/Analysis/EngineRun.cpp | 238 +- lib/Analysis/EngineSummary.cpp | 105 +- lib/Analysis/EngineUnit.cpp | 11 +- lib/Analysis/KindInference.cpp | 4 + lib/Analysis/KindInferenceFields.cpp | 2 + lib/Analysis/KindInferenceMustAccess.cpp | 7 + lib/Analysis/LedgerAdapter.cpp | 56 +- lib/Core/CheckPlan.cpp | 23 +- lib/Core/Heap.cpp | 72 +- lib/Core/Ledger.cpp | 21 +- lib/Core/LibrarySpec.cpp | 76 +- lib/Core/LibrarySpec.txt | 33 +- lib/Frontend/CMakeLists.txt | 3 + lib/Frontend/CheckEmitter.cpp | 762 +++---- lib/Frontend/Driver.cpp | 116 +- lib/Frontend/GuardPasses.cpp | 866 ++++++++ lib/Frontend/ObjectRegistration.cpp | 125 +- lib/Frontend/Prelude.cpp | 516 +++-- lib/Frontend/RecordFacts.cpp | 11 +- runtime/test/rt_test.c | 95 + runtime/weavec_alloc.c | 106 +- runtime/weavec_objects.c | 327 ++- runtime/weavec_owner.c | 50 +- runtime/weavec_report.c | 2 +- runtime/weavec_rt.h | 304 ++- scripts/check-hygiene.py | 19 +- scripts/corpus-gate.py | 280 ++- scripts/run-cases.py | 321 ++- scripts/test_corpus_gate.py | 186 +- scripts/test_run_cases.py | 123 ++ test/Analysis/rfc0030-budget.c | 6 +- test/Driver/driver-werror.c | 11 + test/Driver/rfc0030-print-prelude.c | 13 +- test/Driver/weavec-archive-note.c | 38 + .../rewrite-oracle-len-before-call.expected.c | 2 +- ...-oracle-lowered-violation-plain.expected.c | 7 + ...ewrite-oracle-lowered-violation.expected.c | 7 +- test/Emission/Inputs/rewrite-oracle.py | 12 +- ...runtime-oracle-checked-wrappers.expected.c | 26 + .../runtime-oracle-global-objects.expected.c | 4 +- .../runtime-oracle-range-cache.expected.c | 31 - .../runtime-oracle-stack-objects.expected.c | 6 +- test/Emission/checked-wrappers-runtime.c | 63 + test/Emission/guard-passes-call-arguments.c | 26 + test/Emission/guard-passes-global-padding.c | 33 + .../rewrite-oracle-lowered-violation.c | 17 +- .../rfc0030-disjoint-computed-pointer.c | 5 +- .../runtime-oracle-checked-wrappers.c | 29 + test/Emission/runtime-oracle-range-cache.c | 31 - test/Emission/runtime-oracle-stack-objects.c | 3 +- .../stack-objects-callback-argument.c | 25 + test/Prelude/rfc0030-prelude-compile.c | 3 - test/Prelude/rfc0030-prelude-runtime.c | 41 +- test/cases/README.md | 66 +- .../detection-blind/01_ring_buffer_wrap.c | 75 + .../detection-blind/02_strbuf_terminator.c | 70 + .../detection-blind/03_csv_quoted_field.c | 77 + .../detection-blind/04_matrix_transpose.c | 101 + test/cases/detection-blind/05_lexer_peek.c | 98 + .../detection-blind/06_strncpy_unterminated.c | 52 + .../detection-blind/07_hash_table_rounding.c | 110 + .../detection-blind/08_histogram_max_bucket.c | 52 + .../detection-blind/09_snprintf_offset.c | 57 + .../detection-blind/10_tlv_record_length.c | 75 + .../detection-blind/11_base64_encode_nul.c | 69 + .../12_strip_slashes_underflow.c | 42 + .../detection-blind/13_missing_sentinel.c | 81 + .../cases/detection-blind/14_utf8_truncated.c | 90 + .../15_smallvec_intra_object.c | 67 + .../16_realloc_bytes_not_elems.c | 67 + .../17_letter_count_negative.c | 44 + .../detection-blind/18_erase_memmove_count.c | 55 + .../detection-blind/19_bitmap_round_down.c | 61 + .../detection-blind/20_list_purge_next.c | 71 + .../detection-blind/21_symtab_stale_pointer.c | 97 + .../22_label_out_param_stack.c | 56 + .../detection-blind/23_callback_ctx_freed.c | 105 + .../detection-blind/24_lru_evicted_value.c | 101 + .../detection-blind/25_hashmap_iter_rehash.c | 155 ++ .../detection-blind/26_arena_reset_stale.c | 104 + .../27_config_reload_dangling.c | 94 + .../28_refcount_borrowed_unref.c | 100 + .../detection-blind/29_global_ctx_stack.c | 78 + .../cases/detection-blind/30_queue_pop_name.c | 86 + .../detection-blind/31_bst_delete_successor.c | 103 + .../32_timer_cancel_in_callback.c | 97 + .../33_realloc_result_ignored.c | 75 + .../detection-blind/34_block_scope_label.c | 53 + .../35_worklist_push_invalidates.c | 75 + .../36_error_pointer_into_copy.c | 73 + .../37_double_free_error_path.c | 81 + .../detection-blind/38_free_trimmed_value.c | 91 + .../detection-blind/39_free_default_name.c | 66 + .../40_shallow_copy_double_free.c | 73 + .../detection-blind/41_realloc_free_old.c | 70 + .../detection-blind/42_skip_level_null.c | 53 + .../detection-blind/43_shape_parse_null.c | 80 + .../detection-blind/44_uninit_stream_buffer.c | 98 + .../detection-blind/45_strchr_null_flag.c | 61 + .../detection-blind/46_uninit_token_text.c | 84 + .../detection-blind/47_thread_stack_arg.c | 87 + .../48_logger_thread_freed_msg.c | 109 + test/cases/detection-blind/README.md | 98 + test/cases/detection-blind/run.sh | 64 + .../cases/detection/01_hof_strcpy_name/prog.c | 59 + .../detection/02_hof_offbyone_parse/prog.c | 52 + .../03_hof_read_declared_count/prog.c | 58 + .../03_hof_read_declared_count/stdin.txt | 1 + .../detection/04_hof_sprintf_logger/prog.c | 36 + .../detection/05_hof_strcat_pathjoin/prog.c | 37 + .../detection/06_hof_memcpy_packet/prog.c | 57 + .../detection/07_hof_intoverflow_size/prog.c | 57 + .../07_hof_intoverflow_size/stdin.txt | 3 + .../detection/08_hof_realloc_bytes/prog.c | 44 + test/cases/detection/09_hunder_rtrim/prog.c | 36 + .../detection/10_hunder_undo_stack/prog.c | 51 + .../detection/11_hadj_image_stride/prog.c | 60 + .../cases/detection/12_hadj_matrix_row/prog.c | 54 + .../detection/13_stack_strcpy_route/prog.c | 35 + .../detection/14_stack_offbyone_read/prog.c | 35 + .../detection/15_stack_intraobj_admin/prog.c | 34 + .../detection/16_stack_member_index/prog.c | 33 + .../detection/17_stack_callee_cursor/prog.c | 30 + .../detection/18_stack_sprintf_addr/prog.c | 36 + test/cases/detection/19_glob_histogram/prog.c | 35 + .../detection/19_glob_histogram/stdin.txt | 1 + .../detection/20_glob_strcpy_progname/prog.c | 33 + .../21_glob_cursor_unterminated/prog.c | 37 + .../detection/22_glob_negative_index/prog.c | 28 + test/cases/detection/23_uaf_list_pop/prog.c | 59 + .../detection/24_uaf_session_alias/prog.c | 69 + .../detection/25_uaf_realloc_elemptr/prog.c | 52 + test/cases/detection/26_uaf_xtu_conn/conn.c | 32 + test/cases/detection/26_uaf_xtu_conn/conn.h | 14 + test/cases/detection/26_uaf_xtu_conn/main.c | 39 + .../detection/27_uaf_callback_ctx/prog.c | 58 + .../detection/28_uaf_strdup_value/prog.c | 42 + .../detection/29_uaf_getline_first/prog.c | 36 + .../detection/29_uaf_getline_first/stdin.txt | 3 + .../detection/30_uaf_table_resize/prog.c | 67 + test/cases/detection/31_df_error_path/prog.c | 40 + test/cases/detection/32_df_xtu_strbuf/main.c | 40 + .../cases/detection/32_df_xtu_strbuf/strbuf.c | 33 + .../cases/detection/32_df_xtu_strbuf/strbuf.h | 13 + .../cases/detection/33_df_shared_title/prog.c | 67 + .../detection/34_if_interior_trim/prog.c | 40 + .../detection/35_if_stack_scratch/prog.c | 35 + .../detection/36_uar_parser_scratch/prog.c | 58 + test/cases/detection/37_uas_block_tmp/prog.c | 35 + .../cases/detection/38_uar_global_opts/prog.c | 57 + .../cases/detection/39_uninit_best_ptr/prog.c | 45 + .../detection/40_uninit_realloc_slots/prog.c | 61 + .../detection/41_null_failed_malloc/prog.c | 43 + test/cases/detection/42_null_lookup/prog.c | 56 + test/cases/detection/43_null_getenv/prog.c | 30 + .../detection/44_overlap_memcpy_remove/prog.c | 45 + .../detection/45_overlap_strcpy_prefix/prog.c | 32 + .../detection/46_fmt_unterminated_heap/prog.c | 44 + .../detection/47_strlen_filled_stack/prog.c | 39 + .../cases/detection/48_asprintf_append/prog.c | 37 + .../detection/49_strdup_strcat_bak/prog.c | 37 + .../detection/50_getline_ptr_array/prog.c | 41 + .../detection/50_getline_ptr_array/stdin.txt | 6 + .../detection/51_tc_shape_factory/prog.c | 65 + .../cases/detection/52_tc_callback_ctx/prog.c | 60 + .../cases/detection/53_stack_ptr_array/prog.c | 36 + .../detection/54_uaf_global_cache/prog.c | 46 + .../detection/55_hof_realloc_shrink/prog.c | 59 + test/cases/detection/56_hof_xtu_sbuf/main.c | 23 + test/cases/detection/56_hof_xtu_sbuf/sbuf.c | 34 + test/cases/detection/56_hof_xtu_sbuf/sbuf.h | 13 + test/cases/detection/57_arena_internal/prog.c | 53 + .../58_fmt_unterminated_struct/prog.c | 40 + .../detection/59_hof_nul_terminator/prog.c | 39 + .../detection/59_hof_nul_terminator/stdin.txt | 1 + .../detection/60_uaf_xtu_callee_frees/main.c | 30 + .../detection/60_uaf_xtu_callee_frees/msg.c | 20 + .../detection/60_uaf_xtu_callee_frees/msg.h | 10 + .../detection/61_if_global_default/prog.c | 39 + test/cases/evaluation/vla-known-miss.c | 2 +- test/cases/pairs/fam-bug.c | 2 +- test/cases/recall/CWE-121/memset_too_much.c | 2 +- test/cases/recall/CWE-121/strcpy_literal.c | 2 +- test/cases/recall/CWE-122/sized_field.c | 2 +- test/cases/recall/CWE-122/strcpy_strlen.c | 4 +- .../recall/CWE-126/strlen_unterminated.c | 4 +- .../recall/CWE-170/strncpy_unterminated.c | 8 +- .../confirm/bounded-element-release.c | 33 + .../confirm/const-shallow-callback-callee.c | 7 + .../confirm/const-shallow-callback.c | 35 + .../confirm/const-shallow-local-callee.c | 9 + .../semantics/confirm/const-shallow-local.c | 24 + .../semantics/confirm/dangling-hint-direct.c | 34 + .../semantics/confirm/disequality-edges.c | 59 + .../semantics/confirm/exclusive-out-params.c | 54 + .../confirm/exclusive-result-or-out-param.c | 24 + .../confirm/exclusive-switch-out-params.c | 29 + .../confirm/loop-exit-release-break.c | 36 + .../confirm/loop-exit-release-search.c | 36 + .../semantics/confirm/loop-exit-release.c | 36 + .../semantics/confirm/munmap-constant-pages.c | 25 + .../semantics/confirm/munmap-hint-address.c | 42 + .../semantics/confirm/munmap-partial-range.c | 38 + .../semantics/confirm/munmap-whole-twice.c | 21 + .../confirm/release-by-flag-stream.c | 34 + .../cases/semantics/confirm/release-by-flag.c | 47 + .../semantics/confirm/shared-out-params.c | 34 + .../semantics/confirm/sprintf-guard-fmt.c | 6 + test/cases/semantics/confirm/sprintf-guard.c | 31 + .../confirm/unreachable-after-assert.c | 46 + .../detect-probes/62_uaf_focus_alias/prog.c | 64 + .../detect-probes/63_uaf_loop_next/prog.c | 68 + .../64_arena_block_overflow/prog.c | 48 + .../emission/lowered-out-of-bounds.c | 2 +- .../lowered-use-after-free-no-runtime.c | 13 +- .../runtime/format-precision-dangling_bug.c | 25 + .../runtime/format-precision-dangling_ok.c | 25 + .../runtime/libcall-copy-source_bug.c | 24 + .../runtime/libcall-copy-source_ok.c | 24 + .../runtime/parameter-neighbours_ok.c | 39 + .../semantics/runtime/term-signed-sum_bug.c | 30 + .../semantics/runtime/term-signed-sum_ok.c | 30 + .../semantics/runtime/wrapper-stpcpy_bug.c | 19 + .../semantics/runtime/wrapper-stpcpy_ok.c | 20 + .../semantics/runtime/wrapper-strcat_bug.c | 21 + .../semantics/runtime/wrapper-strcat_ok.c | 22 + .../semantics/runtime/wrapper-strcpy_bug.c | 18 + .../semantics/runtime/wrapper-strcpy_ok.c | 19 + .../semantics/runtime/wrapper-vsprintf_bug.c | 25 + .../semantics/runtime/wrapper-vsprintf_ok.c | 26 + .../soundness/07_strcpy_stack_overflow_bug.c | 16 +- test/cases/soundness/19_vla_size_bug.c | 2 +- test/cases/soundness/41d_many_branches_bug.c | 6 +- .../Inputs/escaped-local-unknown-call-impl.c | 9 + .../alias-cursor-several-arrays_bug.c | 20 + .../alias-cursor-several-arrays_ok.c | 21 + .../soundness/escaped-local-unknown-call_ok.c | 22 + test/corpus/README.md | 43 + test/corpus/bench/curl-bench.c | 207 ++ test/corpus/bench/janet-bench.janet | 22 + test/corpus/bench/libgit2-bench.c | 362 ++++ test/corpus/bench/lmdb-bench.c | 40 + test/corpus/bench/quickjs-bench.js | 19 + test/corpus/expected.json | 818 ++++--- test/corpus/manifest.json | 491 ++++- test/corpus/support/cmark/cmark_export.h | 42 + test/corpus/support/cmark/cmark_version.h | 7 + test/corpus/support/curl/curl_config.h | 793 +++++++ test/corpus/support/flac/config.h | 232 ++ test/corpus/support/giflib/run-tests.sh | 25 + test/corpus/support/libgit2/experimental.h | 11 + test/corpus/support/libgit2/git2_features.h | 103 + test/corpus/support/libjpeg-turbo/jconfig.h | 60 + .../corpus/support/libjpeg-turbo/jconfigint.h | 82 + test/corpus/support/libjpeg-turbo/jversion.h | 30 + test/corpus/support/lmdb/fixed-seed.h | 9 + test/corpus/support/lmdb/run-tests.sh | 43 + test/corpus/support/opus/config.h | 1 + test/corpus/support/xz/config.h | 66 + test/corpus/support/zlib-ng/gzread_mangle.h | 7 + test/corpus/support/zlib-ng/round-trips.sh | 26 + test/corpus/support/zlib-ng/zconf.h | 205 ++ test/corpus/support/zlib-ng/zlib.h | 1911 +++++++++++++++++ .../support/zlib-ng/zlib_name_mangling.h | 8 + test/corpus/triage.json | 120 ++ tools/weavec/main.cpp | 5 +- unittests/Analysis/CheckPlannerTest.cpp | 109 +- unittests/Core/CheckPlanTest.cpp | 27 +- unittests/Core/HeapTest.cpp | 77 + unittests/Core/LedgerTest.cpp | 8 +- unittests/Core/LibrarySpecTest.cpp | 54 +- unittests/Frontend/CheckEmitterTest.cpp | 152 +- unittests/Frontend/LedgerWriterTest.cpp | 16 +- unittests/Frontend/PreludeTest.cpp | 71 +- 302 files changed, 20162 insertions(+), 1960 deletions(-) create mode 100644 docs/rfcs/0034-fast-enforcement.md create mode 100644 include/weavec/Frontend/GuardPasses.h create mode 100644 lib/Frontend/GuardPasses.cpp create mode 100644 test/Driver/driver-werror.c create mode 100644 test/Driver/weavec-archive-note.c create mode 100644 test/Emission/Inputs/rewrite-oracle-lowered-violation-plain.expected.c create mode 100644 test/Emission/Inputs/runtime-oracle-checked-wrappers.expected.c delete mode 100644 test/Emission/Inputs/runtime-oracle-range-cache.expected.c create mode 100644 test/Emission/checked-wrappers-runtime.c create mode 100644 test/Emission/guard-passes-call-arguments.c create mode 100644 test/Emission/guard-passes-global-padding.c create mode 100644 test/Emission/runtime-oracle-checked-wrappers.c delete mode 100644 test/Emission/runtime-oracle-range-cache.c create mode 100644 test/Emission/stack-objects-callback-argument.c create mode 100644 test/cases/detection-blind/01_ring_buffer_wrap.c create mode 100644 test/cases/detection-blind/02_strbuf_terminator.c create mode 100644 test/cases/detection-blind/03_csv_quoted_field.c create mode 100644 test/cases/detection-blind/04_matrix_transpose.c create mode 100644 test/cases/detection-blind/05_lexer_peek.c create mode 100644 test/cases/detection-blind/06_strncpy_unterminated.c create mode 100644 test/cases/detection-blind/07_hash_table_rounding.c create mode 100644 test/cases/detection-blind/08_histogram_max_bucket.c create mode 100644 test/cases/detection-blind/09_snprintf_offset.c create mode 100644 test/cases/detection-blind/10_tlv_record_length.c create mode 100644 test/cases/detection-blind/11_base64_encode_nul.c create mode 100644 test/cases/detection-blind/12_strip_slashes_underflow.c create mode 100644 test/cases/detection-blind/13_missing_sentinel.c create mode 100644 test/cases/detection-blind/14_utf8_truncated.c create mode 100644 test/cases/detection-blind/15_smallvec_intra_object.c create mode 100644 test/cases/detection-blind/16_realloc_bytes_not_elems.c create mode 100644 test/cases/detection-blind/17_letter_count_negative.c create mode 100644 test/cases/detection-blind/18_erase_memmove_count.c create mode 100644 test/cases/detection-blind/19_bitmap_round_down.c create mode 100644 test/cases/detection-blind/20_list_purge_next.c create mode 100644 test/cases/detection-blind/21_symtab_stale_pointer.c create mode 100644 test/cases/detection-blind/22_label_out_param_stack.c create mode 100644 test/cases/detection-blind/23_callback_ctx_freed.c create mode 100644 test/cases/detection-blind/24_lru_evicted_value.c create mode 100644 test/cases/detection-blind/25_hashmap_iter_rehash.c create mode 100644 test/cases/detection-blind/26_arena_reset_stale.c create mode 100644 test/cases/detection-blind/27_config_reload_dangling.c create mode 100644 test/cases/detection-blind/28_refcount_borrowed_unref.c create mode 100644 test/cases/detection-blind/29_global_ctx_stack.c create mode 100644 test/cases/detection-blind/30_queue_pop_name.c create mode 100644 test/cases/detection-blind/31_bst_delete_successor.c create mode 100644 test/cases/detection-blind/32_timer_cancel_in_callback.c create mode 100644 test/cases/detection-blind/33_realloc_result_ignored.c create mode 100644 test/cases/detection-blind/34_block_scope_label.c create mode 100644 test/cases/detection-blind/35_worklist_push_invalidates.c create mode 100644 test/cases/detection-blind/36_error_pointer_into_copy.c create mode 100644 test/cases/detection-blind/37_double_free_error_path.c create mode 100644 test/cases/detection-blind/38_free_trimmed_value.c create mode 100644 test/cases/detection-blind/39_free_default_name.c create mode 100644 test/cases/detection-blind/40_shallow_copy_double_free.c create mode 100644 test/cases/detection-blind/41_realloc_free_old.c create mode 100644 test/cases/detection-blind/42_skip_level_null.c create mode 100644 test/cases/detection-blind/43_shape_parse_null.c create mode 100644 test/cases/detection-blind/44_uninit_stream_buffer.c create mode 100644 test/cases/detection-blind/45_strchr_null_flag.c create mode 100644 test/cases/detection-blind/46_uninit_token_text.c create mode 100644 test/cases/detection-blind/47_thread_stack_arg.c create mode 100644 test/cases/detection-blind/48_logger_thread_freed_msg.c create mode 100644 test/cases/detection-blind/README.md create mode 100755 test/cases/detection-blind/run.sh create mode 100644 test/cases/detection/01_hof_strcpy_name/prog.c create mode 100644 test/cases/detection/02_hof_offbyone_parse/prog.c create mode 100644 test/cases/detection/03_hof_read_declared_count/prog.c create mode 100644 test/cases/detection/03_hof_read_declared_count/stdin.txt create mode 100644 test/cases/detection/04_hof_sprintf_logger/prog.c create mode 100644 test/cases/detection/05_hof_strcat_pathjoin/prog.c create mode 100644 test/cases/detection/06_hof_memcpy_packet/prog.c create mode 100644 test/cases/detection/07_hof_intoverflow_size/prog.c create mode 100644 test/cases/detection/07_hof_intoverflow_size/stdin.txt create mode 100644 test/cases/detection/08_hof_realloc_bytes/prog.c create mode 100644 test/cases/detection/09_hunder_rtrim/prog.c create mode 100644 test/cases/detection/10_hunder_undo_stack/prog.c create mode 100644 test/cases/detection/11_hadj_image_stride/prog.c create mode 100644 test/cases/detection/12_hadj_matrix_row/prog.c create mode 100644 test/cases/detection/13_stack_strcpy_route/prog.c create mode 100644 test/cases/detection/14_stack_offbyone_read/prog.c create mode 100644 test/cases/detection/15_stack_intraobj_admin/prog.c create mode 100644 test/cases/detection/16_stack_member_index/prog.c create mode 100644 test/cases/detection/17_stack_callee_cursor/prog.c create mode 100644 test/cases/detection/18_stack_sprintf_addr/prog.c create mode 100644 test/cases/detection/19_glob_histogram/prog.c create mode 100644 test/cases/detection/19_glob_histogram/stdin.txt create mode 100644 test/cases/detection/20_glob_strcpy_progname/prog.c create mode 100644 test/cases/detection/21_glob_cursor_unterminated/prog.c create mode 100644 test/cases/detection/22_glob_negative_index/prog.c create mode 100644 test/cases/detection/23_uaf_list_pop/prog.c create mode 100644 test/cases/detection/24_uaf_session_alias/prog.c create mode 100644 test/cases/detection/25_uaf_realloc_elemptr/prog.c create mode 100644 test/cases/detection/26_uaf_xtu_conn/conn.c create mode 100644 test/cases/detection/26_uaf_xtu_conn/conn.h create mode 100644 test/cases/detection/26_uaf_xtu_conn/main.c create mode 100644 test/cases/detection/27_uaf_callback_ctx/prog.c create mode 100644 test/cases/detection/28_uaf_strdup_value/prog.c create mode 100644 test/cases/detection/29_uaf_getline_first/prog.c create mode 100644 test/cases/detection/29_uaf_getline_first/stdin.txt create mode 100644 test/cases/detection/30_uaf_table_resize/prog.c create mode 100644 test/cases/detection/31_df_error_path/prog.c create mode 100644 test/cases/detection/32_df_xtu_strbuf/main.c create mode 100644 test/cases/detection/32_df_xtu_strbuf/strbuf.c create mode 100644 test/cases/detection/32_df_xtu_strbuf/strbuf.h create mode 100644 test/cases/detection/33_df_shared_title/prog.c create mode 100644 test/cases/detection/34_if_interior_trim/prog.c create mode 100644 test/cases/detection/35_if_stack_scratch/prog.c create mode 100644 test/cases/detection/36_uar_parser_scratch/prog.c create mode 100644 test/cases/detection/37_uas_block_tmp/prog.c create mode 100644 test/cases/detection/38_uar_global_opts/prog.c create mode 100644 test/cases/detection/39_uninit_best_ptr/prog.c create mode 100644 test/cases/detection/40_uninit_realloc_slots/prog.c create mode 100644 test/cases/detection/41_null_failed_malloc/prog.c create mode 100644 test/cases/detection/42_null_lookup/prog.c create mode 100644 test/cases/detection/43_null_getenv/prog.c create mode 100644 test/cases/detection/44_overlap_memcpy_remove/prog.c create mode 100644 test/cases/detection/45_overlap_strcpy_prefix/prog.c create mode 100644 test/cases/detection/46_fmt_unterminated_heap/prog.c create mode 100644 test/cases/detection/47_strlen_filled_stack/prog.c create mode 100644 test/cases/detection/48_asprintf_append/prog.c create mode 100644 test/cases/detection/49_strdup_strcat_bak/prog.c create mode 100644 test/cases/detection/50_getline_ptr_array/prog.c create mode 100644 test/cases/detection/50_getline_ptr_array/stdin.txt create mode 100644 test/cases/detection/51_tc_shape_factory/prog.c create mode 100644 test/cases/detection/52_tc_callback_ctx/prog.c create mode 100644 test/cases/detection/53_stack_ptr_array/prog.c create mode 100644 test/cases/detection/54_uaf_global_cache/prog.c create mode 100644 test/cases/detection/55_hof_realloc_shrink/prog.c create mode 100644 test/cases/detection/56_hof_xtu_sbuf/main.c create mode 100644 test/cases/detection/56_hof_xtu_sbuf/sbuf.c create mode 100644 test/cases/detection/56_hof_xtu_sbuf/sbuf.h create mode 100644 test/cases/detection/57_arena_internal/prog.c create mode 100644 test/cases/detection/58_fmt_unterminated_struct/prog.c create mode 100644 test/cases/detection/59_hof_nul_terminator/prog.c create mode 100644 test/cases/detection/59_hof_nul_terminator/stdin.txt create mode 100644 test/cases/detection/60_uaf_xtu_callee_frees/main.c create mode 100644 test/cases/detection/60_uaf_xtu_callee_frees/msg.c create mode 100644 test/cases/detection/60_uaf_xtu_callee_frees/msg.h create mode 100644 test/cases/detection/61_if_global_default/prog.c create mode 100644 test/cases/semantics/confirm/bounded-element-release.c create mode 100644 test/cases/semantics/confirm/const-shallow-callback-callee.c create mode 100644 test/cases/semantics/confirm/const-shallow-callback.c create mode 100644 test/cases/semantics/confirm/const-shallow-local-callee.c create mode 100644 test/cases/semantics/confirm/const-shallow-local.c create mode 100644 test/cases/semantics/confirm/dangling-hint-direct.c create mode 100644 test/cases/semantics/confirm/disequality-edges.c create mode 100644 test/cases/semantics/confirm/exclusive-out-params.c create mode 100644 test/cases/semantics/confirm/exclusive-result-or-out-param.c create mode 100644 test/cases/semantics/confirm/exclusive-switch-out-params.c create mode 100644 test/cases/semantics/confirm/loop-exit-release-break.c create mode 100644 test/cases/semantics/confirm/loop-exit-release-search.c create mode 100644 test/cases/semantics/confirm/loop-exit-release.c create mode 100644 test/cases/semantics/confirm/munmap-constant-pages.c create mode 100644 test/cases/semantics/confirm/munmap-hint-address.c create mode 100644 test/cases/semantics/confirm/munmap-partial-range.c create mode 100644 test/cases/semantics/confirm/munmap-whole-twice.c create mode 100644 test/cases/semantics/confirm/release-by-flag-stream.c create mode 100644 test/cases/semantics/confirm/release-by-flag.c create mode 100644 test/cases/semantics/confirm/shared-out-params.c create mode 100644 test/cases/semantics/confirm/sprintf-guard-fmt.c create mode 100644 test/cases/semantics/confirm/sprintf-guard.c create mode 100644 test/cases/semantics/confirm/unreachable-after-assert.c create mode 100644 test/cases/semantics/detect-probes/62_uaf_focus_alias/prog.c create mode 100644 test/cases/semantics/detect-probes/63_uaf_loop_next/prog.c create mode 100644 test/cases/semantics/detect-probes/64_arena_block_overflow/prog.c create mode 100644 test/cases/semantics/runtime/format-precision-dangling_bug.c create mode 100644 test/cases/semantics/runtime/format-precision-dangling_ok.c create mode 100644 test/cases/semantics/runtime/libcall-copy-source_bug.c create mode 100644 test/cases/semantics/runtime/libcall-copy-source_ok.c create mode 100644 test/cases/semantics/runtime/parameter-neighbours_ok.c create mode 100644 test/cases/semantics/runtime/term-signed-sum_bug.c create mode 100644 test/cases/semantics/runtime/term-signed-sum_ok.c create mode 100644 test/cases/semantics/runtime/wrapper-stpcpy_bug.c create mode 100644 test/cases/semantics/runtime/wrapper-stpcpy_ok.c create mode 100644 test/cases/semantics/runtime/wrapper-strcat_bug.c create mode 100644 test/cases/semantics/runtime/wrapper-strcat_ok.c create mode 100644 test/cases/semantics/runtime/wrapper-strcpy_bug.c create mode 100644 test/cases/semantics/runtime/wrapper-strcpy_ok.c create mode 100644 test/cases/semantics/runtime/wrapper-vsprintf_bug.c create mode 100644 test/cases/semantics/runtime/wrapper-vsprintf_ok.c create mode 100644 test/cases/soundness/Inputs/escaped-local-unknown-call-impl.c create mode 100644 test/cases/soundness/alias-cursor-several-arrays_bug.c create mode 100644 test/cases/soundness/alias-cursor-several-arrays_ok.c create mode 100644 test/cases/soundness/escaped-local-unknown-call_ok.c create mode 100644 test/corpus/bench/curl-bench.c create mode 100644 test/corpus/bench/janet-bench.janet create mode 100644 test/corpus/bench/libgit2-bench.c create mode 100644 test/corpus/bench/lmdb-bench.c create mode 100644 test/corpus/bench/quickjs-bench.js create mode 100644 test/corpus/support/cmark/cmark_export.h create mode 100644 test/corpus/support/cmark/cmark_version.h create mode 100644 test/corpus/support/curl/curl_config.h create mode 100644 test/corpus/support/flac/config.h create mode 100755 test/corpus/support/giflib/run-tests.sh create mode 100644 test/corpus/support/libgit2/experimental.h create mode 100644 test/corpus/support/libgit2/git2_features.h create mode 100644 test/corpus/support/libjpeg-turbo/jconfig.h create mode 100644 test/corpus/support/libjpeg-turbo/jconfigint.h create mode 100644 test/corpus/support/libjpeg-turbo/jversion.h create mode 100644 test/corpus/support/lmdb/fixed-seed.h create mode 100755 test/corpus/support/lmdb/run-tests.sh create mode 100644 test/corpus/support/opus/config.h create mode 100644 test/corpus/support/xz/config.h create mode 100644 test/corpus/support/zlib-ng/gzread_mangle.h create mode 100755 test/corpus/support/zlib-ng/round-trips.sh create mode 100644 test/corpus/support/zlib-ng/zconf.h create mode 100644 test/corpus/support/zlib-ng/zlib.h create mode 100644 test/corpus/support/zlib-ng/zlib_name_mangling.h diff --git a/.clang-tidy b/.clang-tidy index e940599e..b4cdd845 100644 --- a/.clang-tidy +++ b/.clang-tidy @@ -11,6 +11,7 @@ Checks: > cert-*, -cert-err58-cpp, clang-analyzer-*, + -clang-analyzer-security.ArrayBound, cppcoreguidelines-*, -cppcoreguidelines-avoid-magic-numbers, -cppcoreguidelines-non-private-member-variables-in-classes, @@ -55,6 +56,10 @@ Checks: > # llvm-use-ranges: lib/Core must not depend on LLVM ADT. # *-macro-to-enum: configuration macros live in generated headers. # readability-trailing-comma: conflicts with clang-format's bin-packing. +# clang-analyzer-security.ArrayBound: reports every operand access of an +# LLVM instruction the analyzed function creates as an access before its +# region (LLVM keeps a User's operands in front of the object), in the +# LLVM headers, where no NOLINT in our code reaches (the guard passes). WarningsAsErrors: '*' HeaderFilterRegex: '(include|lib|tools|unittests)/.*' diff --git a/AGENTS.md b/AGENTS.md index de620d48..7c027a47 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -40,7 +40,11 @@ witness rule for definite errors, raw pointers only from `WEAVEC_RAW`, the library table's portability rule, guards on the accessed address, the link modes (`-fweavec-link=records|analyze|none`), the per-unit budget and unit record format 31; its *Implementation amendments* override its body too. -There is no checked mode. +Then `0034-fast-enforcement.md`: guards as declared calls the LLVM passes +lower to inline shadow-memory checks, registration only where a guard can +reach, definite errors confirmed by a replay, and the work budget; its +*Implementation amendments* (the shadow encoding as built, among others) +override its body. There is no checked mode. ## Before touching the model or the checker @@ -123,7 +127,7 @@ cmake --preset dev && cmake --build --preset dev && ctest --preset dev | Change pointer kinds / how annotations become kinds | `lib/Core/PointerKind.cpp`, `lib/Analysis/AttributeReader.cpp`, `lib/Analysis/KindInference*.cpp`; what the engine takes from them: `lib/Analysis/EngineKinds.cpp` | | Change which checks are inserted | `lib/Analysis/CheckPlanner.cpp` (plan), `lib/Frontend/CheckEmitter.cpp` and `Prelude.cpp` (emission) | | Change which facets get a guard | `CheckPlanner::planGuards` in `lib/Analysis/CheckPlanner.cpp` (RFC 0032 §6); the need of a call argument's guard: `objectWitness` in `lib/Analysis/EngineLibrary.cpp`; possible findings dropped on guarded facets: `LedgerAdapter::dropGuardedPossible` | -| Change the guard helpers / range caches | `lib/Frontend/Prelude.cpp` (`GuardHelpers`, `RuntimeHelpers`, `RuntimeDeclarations`), `lib/Frontend/CheckEmitter.cpp` (`planCache`, `declareCaches`, `isQuietLoop`); oracle tests `test/Emission/runtime-oracle-*.c` | +| Change the guards' lowering / shadow checks | `lib/Frontend/GuardPasses.cpp` (`GuardCanonicalize`, `GuardMerge`, `GuardExpand`, `GlobalPadding`; RFC 0034 §1), the shadow encoding in `runtime/weavec_rt.h`, the prelude's declarations and stack helpers in `lib/Frontend/Prelude.cpp`; tests `test/Emission/guard-passes-*.c`, `runtime-oracle-*.c` | | Change stack / global object registration | `lib/Frontend/ObjectRegistration.cpp` (`planObjects`), `CheckEmitter::registerObjects` | | Change the runtime (allocator, object table, guards, reports) | `runtime/weavec_alloc.c`, `weavec_malloc.c`, `weavec_objects.c`, `weavec_report.c`, `weavec_rt.h` (the prelude declares the same entry points); its C test `runtime/test/rt_test.c` (CTest `runtime`); cases in `test/cases/semantics/runtime/` | | Change the runtime's link line and fallbacks | `lib/Frontend/Driver.cpp` (`addRuntimeLibraries`, `runtimeObstacle`, `allocatorDefinedBy`, `dropAllocatorIfDefined`); `test/Driver/runtime-*.c` | diff --git a/README.md b/README.md index ab617fde..219aa1b2 100644 --- a/README.md +++ b/README.md @@ -130,7 +130,7 @@ weavec-cc -c main.c -o main.o weavec-cc node.o main.o -o prog # checks the records against each other, then links ``` -A bug inside one file is reported when that file is compiled. By default the link step only reads the records: it checks declarations against definitions and the requirements of each exported function at the calls other files make, and analyses no file again. A bug that needs two files, such as a use after free whose `free` is in another file, is caught by its guard at run time; to report it at build time, link with `-fweavec-link=analyze` (which analyses the units again, within a time budget) or run `weavec --whole-program`. Link inputs without a WeaveC record (archives, shared libraries, objects from another compiler) are named in one `unanalyzed-input` warning. +A bug inside one file is reported when that file is compiled. By default the link step only reads the records: it checks declarations against definitions and the requirements of each exported function at the calls other files make, and analyses no file again. A bug that needs two files, such as a use after free whose `free` is in another file, is caught by its guard at run time; to report it at build time, link with `-fweavec-link=analyze` (which analyses the units again, within a time budget) or run `weavec --whole-program`. Link inputs without a WeaveC record (archives, shared libraries, objects from another compiler) are named in one `unanalyzed-input` warning; an archive whose objects `weavec-cc` built is named in a note instead. ### Checks @@ -210,7 +210,7 @@ For a translation unit compiled by `weavec-cc` in an enforcing mode (the default - **(N) Null.** If its null facet is proven or checked, it does not dereference null, or the program traps first. - **(T) Temporal.** If its temporal facet is proven, the object is still alive, and a release releases a live allocation once. - **(G) Guards.** If a facet is guarded (the default; not with `-fno-weavec-runtime`) and the bytes it accesses start inside an object the runtime tracks (a heap block from the runtime's allocator, a local whose address escapes, a global), the object is live and the access stays inside it, or the program traps first. A guarded release is of null or the start of a live heap block, or the program traps. -- **(V) Violations.** A definite violation never reaches the object unguarded: it fails the build, or, if lowered with `-Wno-error`, the site is guarded or checked, and traps unconditionally only where it can be neither. +- **(V) Violations.** A definite violation, confirmed on a feasible path, fails the build; an unconfirmed one is a warning. If lowered with `-Wno-error`, its site is guarded or checked as a possible finding, so it traps only if it happens; nothing traps unconditionally. These hold under six assumptions: @@ -230,22 +230,22 @@ If a memory-safety violation happens anyway, then a check trapped first, or the (G) is weaker than (S) and (T), which is why the ledger counts guarded facets separately from checked ones: - **Provenance is the address accessed.** A guard asks which object the bytes an access touches lie in *now*, at a subscript `p[i]` as at a dereference, so arithmetic that carries a pointer out of one tracked object and into another live one passes. (This is what lets a base formed outside a buffer, such as `base = src - start`, index back into it.) Two cases still trap: an index or field offset that reaches forwards from inside a live local or global into another one, since those lie next to each other with no gap, and an index or offset from a pointer into a live object that lands in memory nothing tracks. Between heap blocks there is always a byte that belongs to none, so a walk off a heap block traps at its first step. -- **Freed memory is recycled.** A freed heap block is caught only while it is in the quarantine (64 MiB by default); once its storage is reused, the guard sees the new object. +- **Freed memory is recycled.** A freed heap block is caught only while it is in the quarantine (16 MiB by default); once its storage is reused, the guard sees the new object. - **Untracked memory passes.** String literals, `alloca` blocks, and memory from other allocators or from code built without the runtime are not tracked; a guard passes on them unless an index carried the pointer there from a live tracked object. The full statement, including what is and is not caught, is in [the guarantees reference](docs/pages/reference/guarantees.md), [RFC 0030, *Soundness*](docs/rfcs/0030-prove-or-trap.md#soundness), [RFC 0032, *Soundness*](docs/rfcs/0032-runtime-enforcement.md#soundness) and [RFC 0033, *Soundness*](docs/rfcs/0033-drop-in-by-default.md#soundness). ## Performance -Guards run on every execution of the operations they cover, and the runtime's allocator replaces the system's. Measured on the corpus benchmarks as user CPU time and peak memory, relative to the same program built by the reference Clang ([RFC 0032](docs/rfcs/0032-runtime-enforcement.md#implementation-amendments), amendment 3): +Guards run on every execution of the operations they cover, and the runtime's allocator replaces the system's. A guard is an inline check of the runtime's shadow memory (one byte per 16 bytes) that the compiler merges and hoists like a load; only what the shadow cannot decide calls the runtime. Measured as user CPU time and peak memory, relative to the same program built by the reference Clang ([RFC 0034](docs/rfcs/0034-fast-enforcement.md#implementation-amendments), amendment 16): | Benchmark | Default (runtime) | `-fno-weavec-runtime` | Peak memory (default) | | --- | ---: | ---: | ---: | -| cJSON parse/print | 1.66× | 1.14× | 0.59× | -| zlib minigzip | 1.85× | 1.00× | 1.09× | -| Lua bench | 5.94× | 1.11× | 1.61× | +| cJSON parse/print | 1.59× | 1.15× | 0.37× | +| zlib minigzip | 1.62× | 1.00× | 1.26× | +| Lua bench | 2.43× | 1.09× | 1.54× | -Interpreters and tight loops over pointers pay the most: Lua's dispatch loop executes roughly one guard for every two instructions of the unguarded program. Code that cannot afford this can build with `-fno-weavec-runtime`; facets that would have been guarded are then `unresolved` and not enforced, and a use of a freed object is not caught at run time. +On ten more projects nobody tuned WeaveC on (QuickJS, LMDB, Janet, brotli, xz, libdeflate, zlib-ng, curl, cmark, libgit2), the default build runs their workloads at 1.5 to 4.0 times the reference compiler's CPU time, 2.55 on average (geometric mean), and every one of them builds and passes its own test suite. Interpreters and tight loops over pointers pay the most. Code that cannot afford this can build with `-fno-weavec-runtime`; facets that would have been guarded are then `unresolved` and not enforced, and a use of a freed object is not caught at run time. ## Building diff --git a/docs/architecture.md b/docs/architecture.md index aab7f27a..f11adc93 100644 --- a/docs/architecture.md +++ b/docs/architecture.md @@ -364,9 +364,25 @@ one raw on some paths is `rawSome`, guarded and never an error); a pointer read back from reinterpreted bits is `raw-cast`; a construct the engine does not evaluate yields unknown values and `unresolved(unanalysed)` for its sites. `memcpy`, `memmove` and record assignments copy leaf by leaf, every source cell read before any is -written. A body that transfers more blocks than `-fweavec-budget` (or visits -one block more than 64 times) stops: its facets take the defaults with -reason `budget`, and its summary is incomplete. +written. A run whose work (the sizes of the states it transfers and +joins) exceeds `-fweavec-budget`, whose entry states hold more than +1,000,000 symbols and objects, whose graph has more than 100,000 blocks, or +that visits one block more than its limit stops (RFC 0034 §7): its facets +take the defaults with reason `budget`, and its summary is incomplete. + +### Confirmation + +A definite finding of the authoritative run is a candidate +(`FunctionRun::confirmCandidates`, RFC 0034 §6). The function is replayed +in witness mode: a depth-first search along single paths with no joins +(at most 256 paths and 20,000 transfers), each block transferred with the +evidence its fixpoint entry state had, a loop left from its fixpoint state +after two turns, and an edge that refinement or a symbol's excluded +constants (`SymInfo::excluded`) empties ending the path. A candidate some +feasible path reaches, and that every such path decides alike, stays an +error; otherwise `LedgerAdapter::unconfirm` makes it a warning with the +note `not confirmed on a feasible path` and plans it as a possible +finding. ### Decisions @@ -504,9 +520,9 @@ checks, writes ledgers and unit records, and runs the link step. | --- | --- | | `FrontendAction.h` | `WeaveCAction`, an `ASTFrontendAction` for libTooling, and `createWeaveCConsumer`, which `weavec-cc` runs at the end of each unit; both run `UnitPipeline`. Every emitted function is analysed, including `static inline` functions from user headers (§5.6). | | `DeferredCodeGenConsumer` | Sits in front of CodeGen in every C code-generating action (§10.5). It forwards Sema set-up at once and records every other callback. At the end of the unit it runs the analysis and `CheckEmitter`, then replays the callbacks in order. Without deferral, CodeGen emits external functions before the analysis runs. It overrides every `ASTConsumer` and `SemaConsumer` virtual of LLVM 23, a list on the LLVM-upgrade checklist. | -| `CheckEmitter` | Applies the `CheckPlan` through Sema (§10.6): `BuildCallExpr` to the helper, `ImpCastExprToType` back to the operand's type so a dereference stays an lvalue, `BuildBinOp` with a comma for a check before a call. User expressions are never evaluated twice. A rewrite Sema rejects leaves the subtree unchanged and fails the compile with an internal error. It also applies the zero-initialisation lowering, gives the guards of a function their range cache (`planCache`, `declareCaches`; see *The runtime*), and registers the unit's stack and global objects (`registerObjects`). | +| `CheckEmitter` | Applies the `CheckPlan` through Sema (§10.6): `BuildCallExpr` to the helper, `ImpCastExprToType` back to the operand's type so a dereference stays an lvalue, `BuildBinOp` with a comma for a check before a call. User expressions are never evaluated twice. A rewrite Sema rejects leaves the subtree unchanged and fails the compile with an internal error. It also applies the zero-initialisation lowering and registers the unit's stack and global objects (`registerObjects`: a registered local is declared `aligned(16)` and entered inline by `__weavec_stack_enter`). | | `ObjectRegistration` | `planObjects` (RFC 0032 §4, §5): which locals and parameters of each emitted function escape and are entered into the runtime's stack list, which calls return twice and are wrapped, and which globals the unit defines and describes. The plan is pure; `CheckEmitter::registerObjects` applies it. | -| `Prelude` | The helpers the rewrites call, injected into the predefines buffer (§10.2): `static`, `always_inline`, `nodebug` functions for the six templates and their forms, term helpers that saturate toward failure, and the allocation wrappers. With the runtime it also declares the runtime's entry points and the arena descriptor, and defines the guard helpers (`object`, `object_c`, `object_n`, `object_s`, `object_l`, `live`, `live_c`, `release`) and the stack-object helpers. Trap mode calls `__builtin_verbose_trap("weavec",