SRI-CSL / yices2 / 25267023082

69%

Build Type

push

github

Committed by web-flow

Commit Message

Fix #613 MCSAT curried function model reconstruction (#614)

* Fix MCSAT curried function model reconstruction

* Fix both-regression baseline solver invocation

* Make curried MCSAT API test NDEBUG-safe

* Enable asserts in curried MCSAT API test

* Add MCSAT SMT2 regression for issue 613

* Fix use-after-free and related issues in MCSAT curried function model

Builds on b2c49c80 (Fix MCSAT curried function model reconstruction) with
several independent fixes in uf_model_builder_get_function_value,
uf_plugin_build_model, and the concrete-value printer.

1. uf_model_builder_get_function_value: use-after-free on int_hmap_pair_t*

   The function cached `find = int_hmap_get(function_value, fid)` before
   recursing into uf_model_builder_get_term_value, then wrote
   `find->val = f_value` after the recursion returned. The recursive call
   can reach int_hmap_get again for a different function id; when that
   call crosses the load-factor threshold, int_hmap_extend reallocates
   (and free()s) the bucket array, invalidating any previously held
   int_hmap_pair_t*. Writing through the stale pointer is a classic
   heap-use-after-free.

   ASan confirms this on tests/regress/mcsat/arrays/issue613_many_curried.smt2:

     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 call)

   Fix: after the recursion, re-fetch the pair with int_hmap_get and
   assign directly; null out the stale `find` to document the invariant
   and prevent future reuse.

2. uf_model_builder_get_function_value: finite-domain null_value assert

   make_fresh_function can legitimately return null_value when the
   domain/range types are both finite and already saturated in the
   value table. The previous code had as... (continued)

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%)

1695673.88 hits per line