| 1892 | } |
| 1893 | |
| 1894 | Memory::CallState |
| 1895 | Memory::mkCallState(const string &fnname, bool nofree, unsigned num_ptr_args, |
| 1896 | const SMTMemoryAccess &access) { |
| 1897 | assert(has_fncall); |
| 1898 | CallState st; |
| 1899 | st.non_local_liveness = mk_liveness_array(); |
| 1900 | st.frees_block = expr::mkUInt(0, st.non_local_liveness); |
| 1901 | |
| 1902 | { |
| 1903 | unsigned num_blocks = 1; |
| 1904 | unsigned limit = num_nonlocals_src - num_inaccessiblememonly_fns; |
| 1905 | for (unsigned i = 0; i < limit; ++i) { |
| 1906 | if (!always_nowrite(i, true, true)) |
| 1907 | ++num_blocks; |
| 1908 | } |
| 1909 | st.writes_block = expr::mkUInt(0, num_blocks); |
| 1910 | } |
| 1911 | |
| 1912 | if (access.canWriteSomething().isFalse()) { |
| 1913 | st.writes_args = expr::mkUInt(0, num_ptr_args); |
| 1914 | return st; |
| 1915 | } |
| 1916 | |
| 1917 | // TODO: handle havoc of local blocks |
| 1918 | |
| 1919 | // inaccessible memory block |
| 1920 | unsigned innaccess_bid = num_nonlocals_src - 1; |
| 1921 | st.non_local_block_val.emplace_back( |
| 1922 | expr::mkFreshVar("blk_val", non_local_block_val[innaccess_bid].val)); |
| 1923 | |
| 1924 | expr only_write_inaccess = access.canOnlyWrite(MemoryAccess::Inaccessible); |
| 1925 | |
| 1926 | if (!only_write_inaccess.isTrue()) { |
| 1927 | unsigned limit = num_nonlocals_src - num_inaccessiblememonly_fns; |
| 1928 | for (unsigned i = 0; i < limit; ++i) { |
| 1929 | if (always_nowrite(i, true, true)) |
| 1930 | continue; |
| 1931 | st.non_local_block_val.emplace_back( |
| 1932 | expr::mkFreshVar("blk_val", mk_block_val_array(i))); |
| 1933 | } |
| 1934 | st.writes_block = expr::mkFreshVar("writes_block", st.writes_block); |
| 1935 | assert(st.writes_block.bits() == st.non_local_block_val.size()); |
| 1936 | } |
| 1937 | else if (!only_write_inaccess.isFalse()) { |
| 1938 | auto var = expr::mkFreshVar("writes_block", expr::mkUInt(0, 1)); |
| 1939 | if (st.writes_block.bits() > 1) |
| 1940 | st.writes_block = expr::mkUInt(0, st.writes_block.bits()-1).concat(var); |
| 1941 | else |
| 1942 | st.writes_block = std::move(var); |
| 1943 | } |
| 1944 | |
| 1945 | st.writes_args |
| 1946 | = expr::mkFreshVar("writes_args", expr::mkUInt(0, num_ptr_args)); |
| 1947 | |
| 1948 | if (num_nonlocals_src && !nofree) { |
| 1949 | auto may_free = access.canAccess(MemoryAccess::Other) || |
| 1950 | access.canAccess(MemoryAccess::Inaccessible); |
| 1951 | st.frees_block |
no test coverage detected