| 1966 | } |
| 1967 | |
| 1968 | void Memory::setState(const Memory::CallState &st, |
| 1969 | const SMTMemoryAccess &access, |
| 1970 | const vector<PtrInput> &ptr_inputs, |
| 1971 | unsigned inaccessible_bid) { |
| 1972 | assert(has_fncall); |
| 1973 | |
| 1974 | if (access.canWriteSomething().isFalse()) |
| 1975 | return; |
| 1976 | |
| 1977 | // 1) Havoc memory |
| 1978 | |
| 1979 | expr only_write_inaccess = access.canOnlyWrite(MemoryAccess::Inaccessible); |
| 1980 | if (!only_write_inaccess.isFalse()) { |
| 1981 | assert(inaccessible_bid != -1u); |
| 1982 | assert(st.non_local_block_val.size() >= 1); |
| 1983 | unsigned bid |
| 1984 | = num_nonlocals_src - num_inaccessiblememonly_fns + inaccessible_bid; |
| 1985 | assert(is_fncall_mem(bid)); |
| 1986 | assert(non_local_block_val[bid].undef.empty()); |
| 1987 | auto &cur_val = non_local_block_val[bid].val; |
| 1988 | cur_val = mk_block_if(only_write_inaccess && st.writes(0), |
| 1989 | st.non_local_block_val[0], cur_val); |
| 1990 | } |
| 1991 | |
| 1992 | // TODO: MemoryAccess::Errno |
| 1993 | |
| 1994 | if (!only_write_inaccess.isTrue()) { |
| 1995 | unsigned idx = 1; |
| 1996 | unsigned limit = num_nonlocals_src - num_inaccessiblememonly_fns; |
| 1997 | const auto written_blocks = st.non_local_block_val.size(); |
| 1998 | for (unsigned bid = 0; bid < limit && idx < written_blocks; ++bid) { |
| 1999 | if (always_nowrite(bid, true, true)) |
| 2000 | continue; |
| 2001 | |
| 2002 | expr modifies = access.canWrite(MemoryAccess::Other) && st.writes(idx); |
| 2003 | |
| 2004 | if (!is_fncall_mem(bid)) { |
| 2005 | unsigned arg_idx = 0; |
| 2006 | for (auto &ptr_in : ptr_inputs) { |
| 2007 | if (bid < next_nonlocal_bid) { |
| 2008 | expr writes = st.writes_args.extract(arg_idx, arg_idx) == 1; |
| 2009 | expr cond = !ptr_in.nowrite && |
| 2010 | ptr_in.byval == 0 && |
| 2011 | access.canWrite(MemoryAccess::Args) && |
| 2012 | writes; |
| 2013 | |
| 2014 | Pointer ptr(*this, ptr_in.val.value); |
| 2015 | modifies |= cond && |
| 2016 | !ptr.isNull() && |
| 2017 | ptr.getBid() == bid; |
| 2018 | state->addUB(cond.implies(ptr_in.val.non_poison)); |
| 2019 | state->addUB(ptr_in.nowrite.implies(!writes)); |
| 2020 | ++arg_idx; |
| 2021 | } |
| 2022 | } |
| 2023 | } |
| 2024 | |
| 2025 | auto &cur_val = non_local_block_val[bid].val; |
no test coverage detected