SRI-CSL / yices2 / 25266440890

67%

master: 69%

Build Type

Pull #614

github

Committed by disteph

Commit Message

Add stress regression for MCSAT curried function model int_hmap resize

tests/regress/mcsat/arrays/issue613_many_curried.smt2 declares 25
curried arrays of type (Array Int (Array Int Int)) and asserts
  (select (select a_i i) i) = 100 + i
for each. The model builder's builder->function_value int_hmap
accumulates roughly 2 * 25 = 50 entries during
uf_plugin_build_model -> uf_model_builder_get_function_value, which
reliably crosses the default load-factor threshold and triggers
int_hmap_extend during one of the recursive calls.

On master, this reproduces the original issue #613 (heap-buffer-overflow
in vtbl_mk_function) under ASan.

On the PR branch without the use-after-free fix in
uf_model_builder_get_function_value, the same test triggers:

  ERROR: AddressSanitizer: heap-use-after-free
  WRITE of size 4 at 0x61100001fca4
    #0 uf_model_builder_get_function_value (stale find->val write)
  freed by thread T0:
    #1 int_hmap_extend int_hash_map.c:173
    #2 int_hmap_get   int_hash_map.c:265
    #3 uf_model_builder_get_function_value (recursive)

On the fixed PR branch, the test passes cleanly both in debug and under
ASan+UBSan. The .gold fixes the expected (get-value ...) outputs for
three representative indices (1, 13, 25) so the test exercises curried
`select (select ...)` model extraction end-to-end.

This complements the existing issue613_model_print.smt2, which covers a
single curried array but does not accumulate enough function_value
entries to force an int_hmap resize during recursion.

Pull Request Pull Request #614: Fix #613 MCSAT curried function model reconstruction

Coverage Stats

179 of 195 new or added lines in 4 files covered. (91.79%)

9 existing lines in 6 files now uncovered.

83429 of 125109 relevant lines covered (66.69%)

1700929.47 hits per line