From a07f15d4c68019b57cf333a4f3e1de7cff9b3444 Mon Sep 17 00:00:00 2001 From: Jasper Haag Date: Wed, 14 Oct 2026 16:26:05 -0400 Subject: [PATCH 1/2] feat(vector): specs for data, empty Specify `std::vector::empty() const` and both `data()` overloads against `spineR`: `empty` returns whether the size is zero, `data` returns the base pointer, which is null for a vector that never allocated. Both are total; using `data()`'s result needs ownership of the elements, as with `operator[]`. TestDataEmpty verifies writes and reads through `data()`. The UB clients in data_ub.cpp (a read one past the last element, and `*v.data()` on an empty vector) get stuck on the missing element ownership; the stuck goals are recorded in data_ub_proof.expected. Co-Authored-By: Claude Opus 5.5 (1M context) --- rocq-brick-libstdcpp/proof/vector/spec.v | 36 ++++++ rocq-brick-libstdcpp/test/dune.inc | 12 ++ rocq-brick-libstdcpp/test/vector/data_ub.cpp | 26 ++++ .../test/vector/data_ub_proof.expected | 120 ++++++++++++++++++ .../test/vector/data_ub_proof.v | 33 +++++ rocq-brick-libstdcpp/test/vector/test.cpp | 16 +++ .../test/vector/test_cpp_proof.v | 11 ++ 7 files changed, 254 insertions(+) create mode 100644 rocq-brick-libstdcpp/test/vector/data_ub.cpp create mode 100644 rocq-brick-libstdcpp/test/vector/data_ub_proof.expected create mode 100644 rocq-brick-libstdcpp/test/vector/data_ub_proof.v diff --git a/rocq-brick-libstdcpp/proof/vector/spec.v b/rocq-brick-libstdcpp/proof/vector/spec.v index 88581712..95d4d51a 100644 --- a/rocq-brick-libstdcpp/proof/vector/spec.v +++ b/rocq-brick-libstdcpp/proof/vector/spec.v @@ -770,6 +770,40 @@ NES.Begin std. Definition SpecFor_erase_range := RegisterSpec erase_range. #[global] Existing Instance SpecFor_erase_range. + (** <> + + -- whether <>. + Total: it only reads the spine. *) + Definition empty := + let qf := function_qualifiers.Nc in + specify.template.method vector "empty" qf Tbool [] $ + \this this + \with q size st + \prepost this |-> spineR q size st + \post[Vbool (bool_decide (size = 0))] emp. + #[global] Hint Opaque empty : sl_opacity. + #[global] Arguments empty : simpl never. + Definition SpecFor_empty := RegisterSpec empty. + #[global] Existing Instance SpecFor_empty. + + (** <> and <> + + -- the base pointer of the + elements, which is null for a vector that never allocated. Total; + using the result needs ownership of the elements, as with + <>. *) + Definition data c := + let qf := function_qualifiers.mk c false Prvalue in + specify.template.method vector "data" qf (Tptr (Tconst_if c ty)) [] $ + \this this + \with q size st + \prepost this |-> spineR q size st + \post[Vptr (base_pointer st)] emp. + #[global] Hint Opaque data : sl_opacity. + #[global] Arguments data : simpl never. + Definition SpecFor_data := RegisterSpec data. + #[global] Existing Instance SpecFor_data. + Definition size `{!IsAllocator alloc_ty} := let qf := function_qualifiers.Nc in specify.template.method vector "size" qf size_type [] $ @@ -857,6 +891,8 @@ NES.Begin std. resize_default ** resize ** size ** + empty ** + MaybeConst data ** MaybeConst begin_spec ** MaybeConst end_spec. #[global] Hint Opaque specs : typeclass_instances sl_opacity. diff --git a/rocq-brick-libstdcpp/test/dune.inc b/rocq-brick-libstdcpp/test/dune.inc index a1db32be..43e3a819 100644 --- a/rocq-brick-libstdcpp/test/dune.inc +++ b/rocq-brick-libstdcpp/test/dune.inc @@ -395,6 +395,18 @@ (with-stderr-to test_cpp.v.stderr (run cpp2v -v %{input} -o test_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) (alias (name srcs) (deps test.cpp)) ) +(subdir vector + (rule + (targets data_ub_cpp.v.stderr data_ub_cpp.v) + (alias test_ast) + (deps + (:input data_ub.cpp) + (env_var CPP2V_DOCKER_ENABLED) + (glob_files_rec ../*.hpp)) + (action + (with-stderr-to data_ub_cpp.v.stderr (run cpp2v -v %{input} -o data_ub_cpp.v --no-elaborate -- -std=c++20 -stdlib=libstdc++ )))) + (alias (name srcs) (deps data_ub.cpp)) +) (subdir vector (rule (targets erase_ub_cpp.v.stderr erase_ub_cpp.v) diff --git a/rocq-brick-libstdcpp/test/vector/data_ub.cpp b/rocq-brick-libstdcpp/test/vector/data_ub.cpp new file mode 100644 index 00000000..3be86b83 --- /dev/null +++ b/rocq-brick-libstdcpp/test/vector/data_ub.cpp @@ -0,0 +1,26 @@ +/* + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + */ +// Accesses through vector::data() outside the elements. +// +// These are undefined behavior: data() points to the vector's elements +// ([vector.data]), and reading past them is an out-of-bounds access +// ([expr.add]/4), as is dereferencing the null data() of an empty vector +// ([expr.unary.op]/1). ASan reports both. +// data_ub_proof.v shows that the vector specs reject each one; +// data_ub_proof.expected records where the proofs get stuck. +// Their UB-free twins are in TestDataEmpty in test.cpp. +#include + +int data_past_end() { + std::vector v; + v.push_back(1); + return v.data()[v.size()]; +} + +int data_empty() { + std::vector v; + return *v.data(); +} diff --git a/rocq-brick-libstdcpp/test/vector/data_ub_proof.expected b/rocq-brick-libstdcpp/test/vector/data_ub_proof.expected new file mode 100644 index 00000000..77a197bf --- /dev/null +++ b/rocq-brick-libstdcpp/test/vector/data_ub_proof.expected @@ -0,0 +1,120 @@ +1 goal + + thread_info : biIndex + _Σ : gFunctors + Σ : cpp_logic thread_info _Σ + σ : genv + _H_ : source ⊧ σ + _PostPred_ : ptr → mpred + PostCond : PostCondition + v_addr : ptr + st' : std.vector.InternalState + GUARDS : GWs.GUARDS + _x_ : valid<"int"> 1 + _H_0 : 0 < 0 + 1 + _H_1 : 0 ≤ 0 + 1 + _H_2 : list.ListSizeZ [1] (0 + 1 - 0) + p : ptr + ============================ + _ : denoteModule source + _ : std.vector.default_ctor "int" "std::allocator" + _ : std.vector.ctor_with_alloc "int" "std::allocator" + _ : std.vector.sized_ctor "int" "std::allocator" + _ : std.vector.init_ctor "int" "std::allocator" + _ : std.vector.copy_alloc_ctor "int" "std::allocator" + _ : std.vector.move_alloc_ctor "int" "std::allocator" + _ : std.vector.copy_ctor "int" "std::allocator" + _ : std.vector.move_ctor "int" "std::allocator" + _ : std.vector.dtor "int" "std::allocator" + _ : std.vector.subscript "int" "std::allocator" true + _ : std.vector.subscript "int" "std::allocator" false + _ : std.vector.push_back_copy "int" "std::allocator" + _ : std.vector.push_back_move "int" "std::allocator" + _ : std.vector.pop_back "int" "std::allocator" + _ : std.vector.front "int" "std::allocator" true + _ : std.vector.front "int" "std::allocator" false + _ : std.vector.back "int" "std::allocator" true + _ : std.vector.back "int" "std::allocator" false + _ : std.vector.clear "int" "std::allocator" + _ : std.vector.resize_default "int" "std::allocator" + _ : std.vector.resize "int" "std::allocator" + _ : std.vector.size "int" "std::allocator" + _ : std.vector.empty "int" "std::allocator" + _ : std.vector.data "int" "std::allocator" true + _ : std.vector.data "int" "std::allocator" false + _ : std.vector.begin_spec "int" "std::allocator" true + _ : std.vector.begin_spec "int" "std::allocator" false + _ : std.vector.end_spec "int" "std::allocator" true + _ : std.vector.end_spec "int" "std::allocator" false + _ : std.allocator.ctor "int" + _ : std.allocator.dtor "int" + _ : type_ptr "std::vector>" v_addr + _ : type_ptr "int" (std.vector.base_pointer st' .[ "int" ! 0 ]) + _ : valid_ptr (std.vector.base_pointer st') + _ : validP<"int*"> (Vptr (std.vector.base_pointer st')) + --------------------------------------□ + _ : PostCond + _ : std.vector.base_pointer st' .[ "int" ! 0 ] |-> intR 1$m 1 + _ : v_addr + |-> std.vector.spineR "int" "std::allocator" 1$m (0 + 1) st' + --------------------------------------∗ + ∃ (v : val) (q : cQp.t), + std.vector.base_pointer st' .[ "int" ! 1 ] |-> primR "int" q v ∗ + (std.vector.base_pointer st' .[ "int" ! 1 ] |-> primR "int" q v -∗ + p |-> primR "int" 1$m v -∗ ::interp { (1 >*> 1) >*> (1 >*> 1) }) +1 goal + + thread_info : biIndex + _Σ : gFunctors + Σ : cpp_logic thread_info _Σ + σ : genv + _H_ : source ⊧ σ + _PostPred_ : ptr → mpred + PostCond : PostCondition + v_addr : ptr + GUARDS : GWs.GUARDS + p : ptr + ============================ + _ : denoteModule source + _ : std.vector.default_ctor "int" "std::allocator" + _ : std.vector.ctor_with_alloc "int" "std::allocator" + _ : std.vector.sized_ctor "int" "std::allocator" + _ : std.vector.init_ctor "int" "std::allocator" + _ : std.vector.copy_alloc_ctor "int" "std::allocator" + _ : std.vector.move_alloc_ctor "int" "std::allocator" + _ : std.vector.copy_ctor "int" "std::allocator" + _ : std.vector.move_ctor "int" "std::allocator" + _ : std.vector.dtor "int" "std::allocator" + _ : std.vector.subscript "int" "std::allocator" true + _ : std.vector.subscript "int" "std::allocator" false + _ : std.vector.push_back_copy "int" "std::allocator" + _ : std.vector.push_back_move "int" "std::allocator" + _ : std.vector.pop_back "int" "std::allocator" + _ : std.vector.front "int" "std::allocator" true + _ : std.vector.front "int" "std::allocator" false + _ : std.vector.back "int" "std::allocator" true + _ : std.vector.back "int" "std::allocator" false + _ : std.vector.clear "int" "std::allocator" + _ : std.vector.resize_default "int" "std::allocator" + _ : std.vector.resize "int" "std::allocator" + _ : std.vector.size "int" "std::allocator" + _ : std.vector.empty "int" "std::allocator" + _ : std.vector.data "int" "std::allocator" true + _ : std.vector.data "int" "std::allocator" false + _ : std.vector.begin_spec "int" "std::allocator" true + _ : std.vector.begin_spec "int" "std::allocator" false + _ : std.vector.end_spec "int" "std::allocator" true + _ : std.vector.end_spec "int" "std::allocator" false + _ : std.allocator.ctor "int" + _ : std.allocator.dtor "int" + _ : type_ptr "std::vector>" v_addr + _ : valid_ptr nullptr + _ : validP<"int*"> (Vptr nullptr) + --------------------------------------□ + _ : PostCond + _ : v_addr |-> std.vector.R_null "int" "std::allocator" 1$m + --------------------------------------∗ + ∃ (v : val) (q : cQp.t), reference_to "int" nullptr ∗ + nullptr |-> primR "int" q v ∗ + (nullptr |-> primR "int" q v -∗ + p |-> primR "int" 1$m v -∗ ::interp { 1 >*> 1 }) diff --git a/rocq-brick-libstdcpp/test/vector/data_ub_proof.v b/rocq-brick-libstdcpp/test/vector/data_ub_proof.v new file mode 100644 index 00000000..6475a6fb --- /dev/null +++ b/rocq-brick-libstdcpp/test/vector/data_ub_proof.v @@ -0,0 +1,33 @@ +(* + * Copyright (c) 2026 SkyLabs AI, Inc. + * This software is distributed under the terms of the BedRock Open-Source License. + * See the LICENSE-BedRock file in the repository root for details. + *) +Require Import skylabs.auto.cpp.prelude.proof. +Require Import skylabs.brick.libstdcpp.allocator.spec. +Require Import skylabs.brick.libstdcpp.vector.spec. + +Require Import skylabs.brick.libstdcpp.test.vector.data_ub_cpp. + +(** * The vector specs reject accesses through [data()] outside the elements + + Each client in [data_ub.cpp] gets stuck reading an element that the vector + does not own; see data_ub_proof.expected. *) + +Section with_cpp. + Context `{Σ : cpp_logic} {σ : genv}. + + cpp.spec "data_past_end()" from source as data_past_end_spec with ( + \prepost std.vector.specs "int" (std.allocator.T "int") + \prepost std.allocator.specs "int" + \post{v}[Vint v] emp). + Lemma data_past_end_ok : verify[source] data_past_end_spec. + Proof. verify_spec; rewrite /std.vector.specs /std.allocator.specs; go. Show. Fail Qed. Abort. + + cpp.spec "data_empty()" from source as data_empty_spec with ( + \prepost std.vector.specs "int" (std.allocator.T "int") + \prepost std.allocator.specs "int" + \post{v}[Vint v] emp). + Lemma data_empty_ok : verify[source] data_empty_spec. + Proof. verify_spec; rewrite /std.vector.specs /std.allocator.specs; go. Show. Fail Qed. Abort. +End with_cpp. diff --git a/rocq-brick-libstdcpp/test/vector/test.cpp b/rocq-brick-libstdcpp/test/vector/test.cpp index e03b97b9..5a888fe8 100644 --- a/rocq-brick-libstdcpp/test/vector/test.cpp +++ b/rocq-brick-libstdcpp/test/vector/test.cpp @@ -125,6 +125,21 @@ TestErase() { test(v.size() == 0); } +void +TestDataEmpty() { + vector v; + test(v.empty()); + v.push_back(1); + v.push_back(2); + test(!v.empty()); + int* p = v.data(); + p[0] = 5; + test(v[0] == 5); + const vector& cv = v; + test(cv.data() == p); + test(cv.data()[1] == 2); +} + int main() { TestBasic(); @@ -133,5 +148,6 @@ main() { TestForEach(); TestAllocCtor(); TestErase(); + TestDataEmpty(); return 0; } diff --git a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v index 648aca3a..54126f2a 100644 --- a/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v +++ b/rocq-brick-libstdcpp/test/vector/test_cpp_proof.v @@ -188,6 +188,9 @@ Section with_cpp. cpp.spec "TestErase()" as test_erase with (\post emp). + cpp.spec "TestDataEmpty()" as test_data_empty with + (\post emp). + cpp.spec "main()" as main with (\post[Vint 0] emp). @@ -286,6 +289,14 @@ Section with_cpp. Definition test_erase_B := [LINK] test_erase_ok. #[local] Hint Resolve test_erase_B : sl_opacity. + Lemma test_data_empty_ok : verify[ source ] test_data_empty. + Proof using MOD. + verify_spec. + go. + Qed. + Definition test_data_empty_B := [LINK] test_data_empty_ok. + #[local] Hint Resolve test_data_empty_B : sl_opacity. + Lemma test_ok : verify[ source ] test_spec. Proof using MOD. verify_spec. From 4fd1d7116b9744822ebaf4b62ff2116990b29faa Mon Sep 17 00:00:00 2001 From: Simon Hudon Date: Tue, 27 Oct 2026 16:09:33 -0400 Subject: [PATCH 2/2] update test output --- .../test/vector/data_ub_proof.expected | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/rocq-brick-libstdcpp/test/vector/data_ub_proof.expected b/rocq-brick-libstdcpp/test/vector/data_ub_proof.expected index 77a197bf..aa9918ff 100644 --- a/rocq-brick-libstdcpp/test/vector/data_ub_proof.expected +++ b/rocq-brick-libstdcpp/test/vector/data_ub_proof.expected @@ -11,9 +11,9 @@ st' : std.vector.InternalState GUARDS : GWs.GUARDS _x_ : valid<"int"> 1 - _H_0 : 0 < 0 + 1 - _H_1 : 0 ≤ 0 + 1 - _H_2 : list.ListSizeZ [1] (0 + 1 - 0) + _H_0 : 0 ≤ 0 + 1 + _H_1 : list.ListSizeZ [1] (0 + 1 - 0) + _H_2 : 0 < 0 + 1 p : ptr ============================ _ : denoteModule source @@ -36,6 +36,8 @@ _ : std.vector.back "int" "std::allocator" true _ : std.vector.back "int" "std::allocator" false _ : std.vector.clear "int" "std::allocator" + _ : std.vector.erase_one "int" "std::allocator" + _ : std.vector.erase_range "int" "std::allocator" _ : std.vector.resize_default "int" "std::allocator" _ : std.vector.resize "int" "std::allocator" _ : std.vector.size "int" "std::allocator" @@ -49,7 +51,7 @@ _ : std.allocator.ctor "int" _ : std.allocator.dtor "int" _ : type_ptr "std::vector>" v_addr - _ : type_ptr "int" (std.vector.base_pointer st' .[ "int" ! 0 ]) + _ : std.vector.base_pointer st' |-> typed_sliceR "int" 0 (0 + 1) _ : valid_ptr (std.vector.base_pointer st') _ : validP<"int*"> (Vptr (std.vector.base_pointer st')) --------------------------------------□ @@ -95,6 +97,8 @@ _ : std.vector.back "int" "std::allocator" true _ : std.vector.back "int" "std::allocator" false _ : std.vector.clear "int" "std::allocator" + _ : std.vector.erase_one "int" "std::allocator" + _ : std.vector.erase_range "int" "std::allocator" _ : std.vector.resize_default "int" "std::allocator" _ : std.vector.resize "int" "std::allocator" _ : std.vector.size "int" "std::allocator"