steakhal wrote: > > At which point do you expect it to simplify the symbolic expression? > > Digging a little deeper with the help of Claude Opus, I think I discovered > the root issue here. I cite it verbatim as it checks out. > > Opus: > > > 1. assumeSym (line 26) calls Sym = simplify(State, S1 & 8). > > 2. Inside simplify, simplifyToSVal → SValBuilder::simplifySVal performs the > > exact substitution you'd expect: S1 is pinned to the > > concrete 2, so S1 & 8 folds all the way to the concrete integer 0 > > (nonloc::ConcreteInt). This is the same machinery the C++ > > cast uses — and it works here too. > > 3. But simplify's return type is SymbolRef. It only keeps the simplified > > result if (SimplifiedVal.getAsSymbol()). A ConcreteInt > > has no underlying symbol, so getAsSymbol() returns null. > > 4. So simplify discards the folded 0 and returns the original, unsimplified > > symbol S1 & 8.
This sounds plausible and also very disappointing. We do all of that complicated work just to throw it away. So much waste. Is there a way to make it work? I recall, some of the simplify* fns should return SVal. That can represent concrete ints - the outcome of the perfect constrained symbols. -- I just looked it up and `SimpleSValBuilder::simplifySVal` for example, returns SVals, just like `simplifyUntilFixpoint`. So what API do you refer to exactly? What is the flow for dropping this concrete value? https://github.com/llvm/llvm-project/pull/210912 _______________________________________________ cfe-commits mailing list [email protected] https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
