shadow mem instruction missing for read-only nodes when only reachable from ret cell

[igcontreras]

$ seahorn --sea-dsa-stats --horn-nondet-undef --keep-shadows=true --sea-dsa-type-aware --sea-dsa=cs -horn-inter-proc -horn-sem-lvl=mem --horn-step=large --horn-solve --horn-global-constraints=true --horn-stats --horn-singleton-aliases=true --horn-pdr-contexts=600 --horn-ignore-calloc=true --horn-ignore-memset=true --horn-shadow-mem-optimize=false --horn-iuc=1 --horn-iuc-arith=1 --horn-weak-abs=true --horn-use-mbqi=true only-ret.bc --sim-dot
$ dot -Tpdf find_anchor_wl_entry.mem.dot -o find_anchor_wl_entry.mem.dot.pdf

In that graph you can see a node only reachable from the return cell that is only read in function find_anchor_wl_entry.

But no shadow mem annotation:

_1502:                                            ; preds = %_1496
  %_1503 = getelementptr inbounds %struct.ubi_device, %struct.ubi_device* %.0460, i64 0, i32 36
  %_1504 = tail call fastcc %struct.ubi_wl_entry* @find_anchor_wl_entry() #9
  %_1505 = icmp eq %struct.ubi_wl_entry* %_1504, null
  br i1 %_1505, label %ubi_wl_get_fm_peb.exit969, label %_1506

Sources: only-ret.zip

[caballa]

@arie: The problem seems simple. We don't create a shadow.mem.out annotation if the created new memory is read-only but I think we should because like in this case, the function allocates memory and returns and some caller will do something with this.

The fix is just to comment these two lines: https://github.com/seahorn/sea-dsa/blob/master/src/ShadowMem.cc#L905 https://github.com/seahorn/sea-dsa/blob/master/src/ShadowMem.cc#L1094

[caballa]

This has been fixed in commit a393e0e43214f8a30d1241a08f2fe00983371948