Integration of Z3 for constraint solving [r299463]

classic Classic list List threaded Threaded
4 messages Options
Reply | Threaded
Open this post in threaded view
|  
Report Content as Inappropriate

Integration of Z3 for constraint solving [r299463]

Richard Pennington 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
|  
Report Content as Inappropriate

Re: Integration of Z3 for constraint solving [r299463]

Richard Pennington 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
|  
Report Content as Inappropriate

Re: Integration of Z3 for constraint solving [r299463]

Richard Pennington 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
|  
Report Content as Inappropriate

Re: Integration of Z3 for constraint solving [r299463]

Richard Pennington via cfe-dev
In reply to this post by Richard Pennington 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
Loading...