martong added a comment.

In D79431#2265155 <https://reviews.llvm.org/D79431#2265155>, @Szelethus wrote:

> In D79431#2263693 <https://reviews.llvm.org/D79431#2263693>, @martong wrote:
>
>> In D79431#2263690 <https://reviews.llvm.org/D79431#2263690>, @martong wrote:
>>
>>> What if we'd add a `toString` method to the constraints and we'd add this 
>>> to `Msg`? This way we'd know the contents of the constraint, thus we we'd 
>>> know //how// the constraint is violated.
>>
>> I mean we'd know what is not satisfied. But, to know why exactly that is not 
>> satisfied we should dump the whole `State` but that's obviously not an 
>> option. Perhaps we could track which symbols and expressions are 
>> participating in the assumption related to the constraint and we could dump 
>> only those, but this seems to be a very complex approach.
>
> I realize that the //how// and //why// phrases in this context a bit too 
> vague :) What do you mean under having to dump the whole `State`? I didn't 
> mean to compress a bug path into a warning message, only what I mentioned in 
> D79431#2020951 <https://reviews.llvm.org/D79431#2020951>. In any case, I 
> think its okay to just move on with this patch. LGTM!

First, thanks for the review!

Second, "dumping the whole State" is an overstatement. What I meant is this: to 
properly explain to the user how the constraint is failed is a hard task. 
Because we should dig up all symbols and expressions that are related to the 
constraint and we should dump their values. E.g. consider the violation of a 
range constraint here,

  ssize_t send(int socket, const void *buffer, size_t length, int flags);
  void foo() {
    if (socket < 0)
      send(socket, buf, buflen, flags); // constraint violation for 'socket' it 
should be in [0, IntMax]
  }

We should print something like this: `'socket' it should be in [0, IntMax] but 
it is in [IntMin, -1]`
In this example, the related symbol is only `socket` but this could be more 
complex, e.g. if the constraint is related to a buffer size ...


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D79431/new/

https://reviews.llvm.org/D79431

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to