To represent z->Empty and w->Universe.
Hello, I still have a superficial question. Consider the domain D:= Var-> Interval, where "Interval" contains two special intervals, " Empty " and " Universe " . I am now using Int_64 from PPL to model this domain. However I feel confused when I need to represent elements that " mixes the 'Empty' and 'Universe' " . One such element is, { x->[3,5], y->[4,7], z->empty, w->universe}. I find that, whenever a constraint like "z->empty" is added to a constraints_system, the constraints_system becomes "false". This seems reasonable because the constraint_system in PPL models a conjunction of constraints and thus one constraint is false make the whole constraint system unsatisfiable. However, I do not see how to represent elements like the one given above that mixes 'z->Empty' and 'w->Universe' . ( I would like to use 'z->empty' to mean 'z is not yet initialized', and 'w->universe' to mean that 'w is unknown' .) I probably misunderstand something basic here. What do you think? Thanks. Zell. p.s Due to the help of Enea and Roberto, I am not able to use PPL in my analysis. I really appreciate your help!!! By the way, I have been using the pseudo name "Zell" because I used to write my name as "Zell". For information, my passport name is "Zhoulai", which can be more or less pronounced as "zell".
Dear all, Added to my last email, I would like to know the possibilities from PPL to symbolically manipulate interval domains? The attachment is a slide of Yang Hongseok on the subject widening/narrowing. He gave an example to show that finite abstract domains are in general less powerful than widening/narrowing approaches. Could you please tell me how to use uniquely PPL's interval abstract domain to infer the relational properties indicated in the attached slide? Thanks a lot. Zell. On Sun, Aug 19, 2012 at 2:56 PM, Zell <zell08v@orange.fr> wrote:
Hello,
I still have a superficial question.
Consider the domain D:= Var-> Interval, where "Interval" contains two special intervals, " Empty " and " Universe " . I am now using Int_64 from PPL to model this domain. However I feel confused when I need to represent elements that " mixes the 'Empty' and 'Universe' " . One such element is, { x->[3,5], y->[4,7], z->empty, w->universe}.
I find that, whenever a constraint like "z->empty" is added to a constraints_system, the constraints_system becomes "false". This seems reasonable because the constraint_system in PPL models a conjunction of constraints and thus one constraint is false make the whole constraint system unsatisfiable. However, I do not see how to represent elements like the one given above that mixes 'z->Empty' and 'w->Universe' . ( I would like to use 'z->empty' to mean 'z is not yet initialized', and 'w->universe' to mean that 'w is unknown' .)
I probably misunderstand something basic here. What do you think?
Thanks. Zell.
p.s Due to the help of Enea and Roberto, I am not able to use PPL in my analysis. I really appreciate your help!!! By the way, I have been using the pseudo name "Zell" because I used to write my name as "Zell". For information, my passport name is "Zhoulai", which can be more or less pronounced as "zell".
On 08/19/2012 02:56 PM, Zell wrote:
I probably misunderstand something basic here. What do you think?
This is not a limitation of the interval domain. In every numerical abstract domain, as soon a constraint becomes "empty", all the abstract objects becomes empty, too. If x is initialized, you should assign it to the universe element, since you don't know which value it may assume. If you want to distinguish between non-initialized and unknown values, you should use an ad-hoc abstract domain. --gianluca amato
Dear all, I think I was not precise enough in my last email. Say I have two boxes of type Int64_box: box1 with one dimension, A->[1,1] box2 of two dimensions, A -> [10,10], B->[4,4] For example, let us analyze the merge point in the end of the snippet int a,b,c,d if (?) {A=1} else {A=10; B=4;} I use Int64_box as abstract domains, so that the if- part and else- part give box1 and box2 as shown above. To reason about the merge point, I use *add_dimension_and_embed *before *upper_bound_assign*. But that will extend box1 to A->[1,1],B->[-inf,+inf] so that the upper_bound_assign will give A->[1,10],* B->[-inf,+inf].* I realize that what I really wanted was to expand box1 to A->[1,1],* B->empty* so that the box1 joined with box2 gives A->[1,10], B->[4,4] I don't see how to extend box1 in that way, because if one dimension is empty, the whole int64_box becomes empty as well, which seems to be reasonable but does not go with my above example. Could you pls help me out from there? I certainly misunderstood something, yet the question should be (hopefully) much more clear now. Thanks a lot. Zell. On Sun, Aug 19, 2012 at 2:56 PM, Zell <zell08v@orange.fr> wrote:
Hello,
I still have a superficial question.
Consider the domain D:= Var-> Interval, where "Interval" contains two special intervals, " Empty " and " Universe " . I am now using Int_64 from PPL to model this domain. However I feel confused when I need to represent elements that " mixes the 'Empty' and 'Universe' " . One such element is, { x->[3,5], y->[4,7], z->empty, w->universe}.
I find that, whenever a constraint like "z->empty" is added to a constraints_system, the constraints_system becomes "false". This seems reasonable because the constraint_system in PPL models a conjunction of constraints and thus one constraint is false make the whole constraint system unsatisfiable. However, I do not see how to represent elements like the one given above that mixes 'z->Empty' and 'w->Universe' . ( I would like to use 'z->empty' to mean 'z is not yet initialized', and 'w->universe' to mean that 'w is unknown' .)
I probably misunderstand something basic here. What do you think?
Thanks. Zell.
p.s Due to the help of Enea and Roberto, I am not able to use PPL in my analysis. I really appreciate your help!!! By the way, I have been using the pseudo name "Zell" because I used to write my name as "Zell". For information, my passport name is "Zhoulai", which can be more or less pronounced as "zell".
On 08/23/2012 01:02 PM, Zell wrote:
I use Int64_box as abstract domains, so that the if- part and else- part give box1 and box2 as shown above. To reason about the merge point, I use *add_dimension_and_embed *before *upper_bound_assign*. But that will extend box1 to A->[1,1],B->[-inf,+inf] so that the upper_bound_assign will give A->[1,10],_B->[-inf,+inf]._
Why you do not like this result? It is the correct one. It means that you don't know anything about B. In other words, B may hold whatever value is there after initialization. In any case, there is no way to have an object like A->[1,1], B->empty with any of the standard numerical domains. --gianluca amato
participants (2)
-
Gianluca Amato -
Zell