SRI-CSL / yices2
67%
master: 69%

LAST BUILD BRANCH: issue-621-plan-a-diff-witness
DEFAULT BRANCH: master
Repo Added
Files 496
Badge
Embed ▾
README BADGES
x

If you need to use a raster PNG badge, change the '.svg' to '.png' in the link

Markdown

Textile

RDoc

HTML

Rst

LAST BUILD ON BRANCH issue-613-mcsat-curried-function-model
branch: issue-613-mcsat-curried-function-model
CHANGE BRANCH
x

coverage: 66.685% (+0.1%) from 66.539%
25266440890

Pull #614

github

disteph 
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 #614: Fix #613 MCSAT curried function model reconstruction

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

Relevant lines Covered
125109 RELEVANT LINES 83429 COVERED LINES
1700929.47 HITS PER LINE
Source Files on issue-613-mcsat-curried-function-model

Recent builds

Builds Branch Commit Type Ran Committer Via Coverage
25266440890 issue-613-mcsat-curried-function-model 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... Pull #614 disteph github
66.69
25262386950 issue-613-mcsat-curried-function-model Add MCSAT SMT2 regression for issue 613 Pull #614 disteph github
66.68
23882458613 issue-613-mcsat-curried-function-model Merge branch 'master' into issue-613-mcsat-curried-function-model Pull #614 web-flow github
66.68
22981281920 issue-613-mcsat-curried-function-model Enable asserts in curried MCSAT API test Pull #614 disteph github
66.68
See All Builds (2069)