Integration of Z3 for constraint solving [r299463]

classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|

Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
Hi,

I just noticed that Z3 was integrated into the clang frontend to solve
some kind of constraints: https://reviews.llvm.org/rL299463

What kinds of constraints are these, i.e. which problem are they
solving, and is there a possibility of running into an exponential runtime?

Kind regards,
--
Paulo Matos
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
This is for the clang static analyzer, when performing symbolic
execution on input C code. Since the variables are all fixed-width
bitvectors, and there are no existential/universal quantifiers, in
practice the performance is decent, although still slower than the
current range-based constraint manager. However, it allows for reasoning
over more complex queries, e.g. involving multiple symbolic variables,
symbolic truncation/extension, and symbolic floating-point expressions
(these are all follow-up patches that have not yet been merged). There's
a longer discussion and more concrete performance numbers starting
around comment https://reviews.llvm.org/D28952#652510 .

Thanks,

Dominic

On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
> Hi,
>
> I just noticed that Z3 was integrated into the clang frontend to solve
> some kind of constraints: https://reviews.llvm.org/rL299463
>
> What kinds of constraints are these, i.e. which problem are they
> solving, and is there a possibility of running into an exponential runtime?
>
> Kind regards,


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
Just realized I meant input code, there's nothing specific to just C.

Dominic

On 4/10/2017 3:21 PM, Dominic Chen wrote:

> This is for the clang static analyzer, when performing symbolic
> execution on input C code. Since the variables are all fixed-width
> bitvectors, and there are no existential/universal quantifiers, in
> practice the performance is decent, although still slower than the
> current range-based constraint manager. However, it allows for reasoning
> over more complex queries, e.g. involving multiple symbolic variables,
> symbolic truncation/extension, and symbolic floating-point expressions
> (these are all follow-up patches that have not yet been merged). There's
> a longer discussion and more concrete performance numbers starting
> around comment https://reviews.llvm.org/D28952#652510 .
>
> Thanks,
>
> Dominic
>
> On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
>> Hi,
>>
>> I just noticed that Z3 was integrated into the clang frontend to solve
>> some kind of constraints: https://reviews.llvm.org/rL299463
>>
>> What kinds of constraints are these, i.e. which problem are they
>> solving, and is there a possibility of running into an exponential runtime?
>>
>> Kind regards,
>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
In reply to this post by Alex Denisov via cfe-dev


On 10/04/17 21:21, Dominic Chen wrote:

> This is for the clang static analyzer, when performing symbolic
> execution on input C code. Since the variables are all fixed-width
> bitvectors, and there are no existential/universal quantifiers, in
> practice the performance is decent, although still slower than the
> current range-based constraint manager. However, it allows for reasoning
> over more complex queries, e.g. involving multiple symbolic variables,
> symbolic truncation/extension, and symbolic floating-point expressions
> (these are all follow-up patches that have not yet been merged). There's
> a longer discussion and more concrete performance numbers starting
> around comment https://reviews.llvm.org/D28952#652510 .
>

Ah, interesting. Thanks for the explanation. That's what I needed to know.

--
Paulo Matos
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
In reply to this post by Alex Denisov via cfe-dev
Do you want to add something about this in the release notes?

On Mon, Apr 10, 2017 at 12:21 PM, Dominic Chen via cfe-dev
<[hidden email]> wrote:

> This is for the clang static analyzer, when performing symbolic
> execution on input C code. Since the variables are all fixed-width
> bitvectors, and there are no existential/universal quantifiers, in
> practice the performance is decent, although still slower than the
> current range-based constraint manager. However, it allows for reasoning
> over more complex queries, e.g. involving multiple symbolic variables,
> symbolic truncation/extension, and symbolic floating-point expressions
> (these are all follow-up patches that have not yet been merged). There's
> a longer discussion and more concrete performance numbers starting
> around comment https://reviews.llvm.org/D28952#652510 .
>
> Thanks,
>
> Dominic
>
> On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
>> Hi,
>>
>> I just noticed that Z3 was integrated into the clang frontend to solve
>> some kind of constraints: https://reviews.llvm.org/rL299463
>>
>> What kinds of constraints are these, i.e. which problem are they
>> solving, and is there a possibility of running into an exponential runtime?
>>
>> Kind regards,
>
>
> _______________________________________________
> cfe-dev mailing list
> [hidden email]
> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
Is a short summary sufficient? For example, "The static analyzer now
supports using the z3 theorem prover from Microsoft Research as an
external constraint solver. This allows reasoning over more complex
queries, but performance is ~15x slower than the default range-based
constraint solver. To enable the z3 solver backend, clang must be built
with the `CLANG_ANALYZER_BUILD_Z3=ON` option, and the `-Xanalyzer
-analyzer-constraints=z3` arguments passed at runtime."

Thanks,

Dominic

On 8/18/2017 6:30 PM, Hans Wennborg wrote:

> Do you want to add something about this in the release notes?
>
> On Mon, Apr 10, 2017 at 12:21 PM, Dominic Chen via cfe-dev
> <[hidden email]> wrote:
>> This is for the clang static analyzer, when performing symbolic
>> execution on input C code. Since the variables are all fixed-width
>> bitvectors, and there are no existential/universal quantifiers, in
>> practice the performance is decent, although still slower than the
>> current range-based constraint manager. However, it allows for reasoning
>> over more complex queries, e.g. involving multiple symbolic variables,
>> symbolic truncation/extension, and symbolic floating-point expressions
>> (these are all follow-up patches that have not yet been merged). There's
>> a longer discussion and more concrete performance numbers starting
>> around comment https://reviews.llvm.org/D28952#652510 .
>>
>> Thanks,
>>
>> Dominic
>>
>> On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
>>> Hi,
>>>
>>> I just noticed that Z3 was integrated into the clang frontend to solve
>>> some kind of constraints: https://reviews.llvm.org/rL299463
>>>
>>> What kinds of constraints are these, i.e. which problem are they
>>> solving, and is there a possibility of running into an exponential runtime?
>>>
>>> Kind regards,
>>
>> _______________________________________________
>> cfe-dev mailing list
>> [hidden email]
>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
Yes, that's excellent.

Would you like to commit that, or would you like me to do it for you?

Thanks,
Hans

On Fri, Aug 18, 2017 at 3:47 PM, Dominic Chen <[hidden email]> wrote:

> Is a short summary sufficient? For example, "The static analyzer now
> supports using the z3 theorem prover from Microsoft Research as an
> external constraint solver. This allows reasoning over more complex
> queries, but performance is ~15x slower than the default range-based
> constraint solver. To enable the z3 solver backend, clang must be built
> with the `CLANG_ANALYZER_BUILD_Z3=ON` option, and the `-Xanalyzer
> -analyzer-constraints=z3` arguments passed at runtime."
>
> Thanks,
>
> Dominic
>
> On 8/18/2017 6:30 PM, Hans Wennborg wrote:
>> Do you want to add something about this in the release notes?
>>
>> On Mon, Apr 10, 2017 at 12:21 PM, Dominic Chen via cfe-dev
>> <[hidden email]> wrote:
>>> This is for the clang static analyzer, when performing symbolic
>>> execution on input C code. Since the variables are all fixed-width
>>> bitvectors, and there are no existential/universal quantifiers, in
>>> practice the performance is decent, although still slower than the
>>> current range-based constraint manager. However, it allows for reasoning
>>> over more complex queries, e.g. involving multiple symbolic variables,
>>> symbolic truncation/extension, and symbolic floating-point expressions
>>> (these are all follow-up patches that have not yet been merged). There's
>>> a longer discussion and more concrete performance numbers starting
>>> around comment https://reviews.llvm.org/D28952#652510 .
>>>
>>> Thanks,
>>>
>>> Dominic
>>>
>>> On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
>>>> Hi,
>>>>
>>>> I just noticed that Z3 was integrated into the clang frontend to solve
>>>> some kind of constraints: https://reviews.llvm.org/rL299463
>>>>
>>>> What kinds of constraints are these, i.e. which problem are they
>>>> solving, and is there a possibility of running into an exponential runtime?
>>>>
>>>> Kind regards,
>>>
>>> _______________________________________________
>>> cfe-dev mailing list
>>> [hidden email]
>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>
>
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
It should be committed in rL311213.

Thanks,

Dominic

> On Aug 18, 2017, at 7:13 PM, Hans Wennborg <[hidden email]> wrote:
>
> Yes, that's excellent.
>
> Would you like to commit that, or would you like me to do it for you?
>
> Thanks,
> Hans
>
> On Fri, Aug 18, 2017 at 3:47 PM, Dominic Chen <[hidden email]> wrote:
>> Is a short summary sufficient? For example, "The static analyzer now
>> supports using the z3 theorem prover from Microsoft Research as an
>> external constraint solver. This allows reasoning over more complex
>> queries, but performance is ~15x slower than the default range-based
>> constraint solver. To enable the z3 solver backend, clang must be built
>> with the `CLANG_ANALYZER_BUILD_Z3=ON` option, and the `-Xanalyzer
>> -analyzer-constraints=z3` arguments passed at runtime."
>>
>> Thanks,
>>
>> Dominic
>>
>> On 8/18/2017 6:30 PM, Hans Wennborg wrote:
>>> Do you want to add something about this in the release notes?
>>>
>>> On Mon, Apr 10, 2017 at 12:21 PM, Dominic Chen via cfe-dev
>>> <[hidden email]> wrote:
>>>> This is for the clang static analyzer, when performing symbolic
>>>> execution on input C code. Since the variables are all fixed-width
>>>> bitvectors, and there are no existential/universal quantifiers, in
>>>> practice the performance is decent, although still slower than the
>>>> current range-based constraint manager. However, it allows for reasoning
>>>> over more complex queries, e.g. involving multiple symbolic variables,
>>>> symbolic truncation/extension, and symbolic floating-point expressions
>>>> (these are all follow-up patches that have not yet been merged). There's
>>>> a longer discussion and more concrete performance numbers starting
>>>> around comment https://reviews.llvm.org/D28952#652510 .
>>>>
>>>> Thanks,
>>>>
>>>> Dominic
>>>>
>>>> On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
>>>>> Hi,
>>>>>
>>>>> I just noticed that Z3 was integrated into the clang frontend to solve
>>>>> some kind of constraints: https://reviews.llvm.org/rL299463
>>>>>
>>>>> What kinds of constraints are these, i.e. which problem are they
>>>>> solving, and is there a possibility of running into an exponential runtime?
>>>>>
>>>>> Kind regards,
>>>>
>>>> _______________________________________________
>>>> cfe-dev mailing list
>>>> [hidden email]
>>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>
>>

_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: Integration of Z3 for constraint solving [r299463]

Alex Denisov via cfe-dev
Perfect, thanks!

On Fri, Aug 18, 2017 at 5:11 PM, Dominic Chen <[hidden email]> wrote:

> It should be committed in rL311213.
>
> Thanks,
>
> Dominic
>
>> On Aug 18, 2017, at 7:13 PM, Hans Wennborg <[hidden email]> wrote:
>>
>> Yes, that's excellent.
>>
>> Would you like to commit that, or would you like me to do it for you?
>>
>> Thanks,
>> Hans
>>
>> On Fri, Aug 18, 2017 at 3:47 PM, Dominic Chen <[hidden email]> wrote:
>>> Is a short summary sufficient? For example, "The static analyzer now
>>> supports using the z3 theorem prover from Microsoft Research as an
>>> external constraint solver. This allows reasoning over more complex
>>> queries, but performance is ~15x slower than the default range-based
>>> constraint solver. To enable the z3 solver backend, clang must be built
>>> with the `CLANG_ANALYZER_BUILD_Z3=ON` option, and the `-Xanalyzer
>>> -analyzer-constraints=z3` arguments passed at runtime."
>>>
>>> Thanks,
>>>
>>> Dominic
>>>
>>> On 8/18/2017 6:30 PM, Hans Wennborg wrote:
>>>> Do you want to add something about this in the release notes?
>>>>
>>>> On Mon, Apr 10, 2017 at 12:21 PM, Dominic Chen via cfe-dev
>>>> <[hidden email]> wrote:
>>>>> This is for the clang static analyzer, when performing symbolic
>>>>> execution on input C code. Since the variables are all fixed-width
>>>>> bitvectors, and there are no existential/universal quantifiers, in
>>>>> practice the performance is decent, although still slower than the
>>>>> current range-based constraint manager. However, it allows for reasoning
>>>>> over more complex queries, e.g. involving multiple symbolic variables,
>>>>> symbolic truncation/extension, and symbolic floating-point expressions
>>>>> (these are all follow-up patches that have not yet been merged). There's
>>>>> a longer discussion and more concrete performance numbers starting
>>>>> around comment https://reviews.llvm.org/D28952#652510 .
>>>>>
>>>>> Thanks,
>>>>>
>>>>> Dominic
>>>>>
>>>>> On 4/10/2017 10:01 AM, Paulo Matos via cfe-dev wrote:
>>>>>> Hi,
>>>>>>
>>>>>> I just noticed that Z3 was integrated into the clang frontend to solve
>>>>>> some kind of constraints: https://reviews.llvm.org/rL299463
>>>>>>
>>>>>> What kinds of constraints are these, i.e. which problem are they
>>>>>> solving, and is there a possibility of running into an exponential runtime?
>>>>>>
>>>>>> Kind regards,
>>>>>
>>>>> _______________________________________________
>>>>> cfe-dev mailing list
>>>>> [hidden email]
>>>>> http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>>
>>>
>
_______________________________________________
cfe-dev mailing list
[hidden email]
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev