holgerblasum Jun 8, 2010 at 11:43 AM Edited Jun 8, 2010 at 11:11 PM Dear all, while the discussion is at the user interface anyway it could be a good idea to give the verification engineer a more tight control over the function-local proof state. ("Nuts" in the title refers to some more persistent proof state object, "beans" was already taken ...). E.g. the following code with a lot of repetitive and hard-to-read asserts #include "vcc.h" typedef struct A_str { unsigned int dummy; invariant(dummy == 0); } A_t; void interfere(A_t *a1, A_t *a2) maintains(wrapped(a1)) maintains(wrapped(a2)) writes(a1) writes(a2); void test(A_t *a1, A_t *a2) maintains(wrapped(a1)) maintains(wrapped(a2)) writes(a1, a2) { interfere(a1, a2); assert(in_domain(a1,a1)); assert(in_domain(a2,a2)); assert(a1->dummy == 0 && a2->dummy == 0); interfere(a1, a2); assert(in_domain(a1,a1)); assert(in_domain(a2,a2)); assert(a1->dummy == 0 && a2->dummy == 0); interfere(a1, a2); assert(in_domain(a1,a1)); assert(in_domain(a2,a2)); assert(a1->dummy == 0 && a2->dummy == 0); interfere(a1, a2); assert(in_domain(a1,a1)); assert(in_domain(a2,a2)); assert(a1->dummy == 0 && a2->dummy == 0); }  can be generated  from the (I think, more human-readable containing "nuts"): #include "vcc.h" typedef struct A_str { unsigned int dummy; invariant(dummy == 0); } A_t; void interfere(A_t *a1, A_t *a2) maintains(wrapped(a1)) maintains(wrapped(a2)) writes(a1) writes(a2); void test(A_t *a1, A_t *a2) maintains(wrapped(a1)) maintains(wrapped(a2)) writes(a1, a2) { nut_t n; nut_store(n, "assert(in_domain(a1,a1));"); //store this into proof state nut_store(n, "assert(in_domain(a2,a2));"); //store this into proof state interfere(a1, a2); nut_load(n); //recall proof state assert(a1->dummy == 0 && a2->dummy == 0); interfere(a1, a2); nut_load(n); assert(a1->dummy == 0 && a2->dummy == 0); interfere(a1, a2); nut_load(n); assert(a1->dummy == 0 && a2->dummy == 0); interfere(a1, a2); nut_load(n); assert(a1->dummy == 0 && a2->dummy == 0); }  by simple preprocessing (e.g. the following would do the job): #!/usr/bin/perl use strict; my %domain; while (my $line = ) { if ($line =~ /^\s*nut_t\s+(\w+);/) { $domain{$1} = ""; next; } if ($line =~ /^\s*nut_store\((\w+),\s*"([^"]*)"/) {$domain{$1} .= " " .$2 . "\n"; next; } if ($line =~ /^\s*nut_load\((\w+)/) { print$domain{$1}; next; } print$line; }  However, having sth like this directly into VCCs UI might be a good idea ... Cheers, Holger MichalMoskal Jun 10, 2010 at 6:21 AM You can use something like: _(logic both_domain(obj_t a, obj_t b) = a \in \domain(a) && b \in \domain(b); ) ... _(assert both_domain(a, b)); (logic function is called specmacro in old syntax). Alternatively you can use C preprocessor. I’m not so happy about another textual preprocessing mechanism, unless more usefulness is demonstrated. We had an idea to introduce a syntax for a chain of in_domains() (which wouldn’t help much in your case, but would in some other). _(in_domain a, b, c) could translate into: _(assert a \in \domain(a)) _(assert b \in \domain(a)) _(assert c \in \domain(a)) Actually, thinking more about it, we already have type-checked macros with nice error messages for function specifications. Maybe we should also have macros for annotations placed in the running code. void \macro_in_domain(obj_t a) { _(assert a \in \domain(a)) } void \macro_in_domain(obj_t a, obj_t b) { _(assert a \in \domain(a)) _(assert b \in \domain(a)) } ... Up to 5 or 10. Of course it would be nicer to have some iteration mechanism, but I think this is good enough. Then you could use: void \macro_both_domain(obj_t a, obj_t b) { _(assert a \in \domain(a) && b \in \domain(b)) } and then _(both_domain a, b) instead of _(assert both_domain(a, b)). This should be relatively simple to implement, I might take a shot at it. Michal holgerblasum Jun 13, 2010 at 10:45 AM Dear Michal, I understand that yet another preprocessing mechanism is not desirable (I just posted the code as proof-of-concept: if it can be done by preprocessing it's (often) not hard to do it in a clean way) and in this particular case I also was not really aware that logic functions might be a good idea for this use case (side-note: in a future version of the tutorial, plan a chapter for "managing large proofs" or so addressing common pitfalls of carrying too much state around explicitly...). I also agree that the "assert(in_domain(&a, &a)); assert(in_domain(&a->b, a)); assert(in_domain(&a->b->c, a));" stuff is maybe the more painful part and from my side I would suggest that "assert(in_domain(&x->y->z, x));" should just obtain the semantics that all parent domains (x,y in this case) are automatically asserted if that has not already done yet (actually I had hacked up some preprocessing for that too at time ...). Maybe simply the syntax "assert(in_domain(&x->y->z))" omitting any "upstream" domain would be enough. Nonetheless, I think that psychologically it might be beneficial for the adoption of VCC if the verification engineer feels less micromanaged: that proof state is automatically forgotten on function boundaries seems an arbitrary imposition to me (it might have been technically motivated by VCC's function boundary rewriting model (that by the way you now have very well explained in the tutorial), but again this is something that can be circumvented already at the preprocessing stage ...) and there should be at least a flag ("/remember" ?) to disable that feature. Now you would argue that at long functions there will be to much interfering stuff in the knowledge base for the automatic prover to find its proofs but there is again an easy solution for that: simply allow the verification engineer to manually forget about certain domains (e.g. "forget(in_domain(&x->y->z))"). Cheers, Holger MichalMoskal Jun 14, 2010 at 8:04 PM > I would suggest that "assert(in_domain(&x->y->z, x));" should just obtain the semantics that all parent domains (x,y in this case) are automatically asserted if that has not already done yet (actually I had hacked up some preprocessing for that too at time ...). In case the domains happen to be x and x->y then it is simple. However, it doesn’t have to be that way (ownership doesn’t have to follow pointer structures). One annotation we were thinking about was something like: struct A { _(keeps) struct B *p; }; which would be the same as stating _(invariant keeps(p)). If y and z would be such pointers, we would be able to figure out the appropriate in_domains. > Nonetheless, I think that psychologically it might be beneficial for the adoption of VCC if the verification engineer feels less micromanaged: that proof state is automatically forgotten on function boundaries seems an arbitrary imposition to me (it might have been technically motivated by VCC's function boundary rewriting model (that by the way you now have very well explained in the tutorial), but again this is something that can be circumvented already at the preprocessing stage ...) and there should be at least a flag ("/remember" ?) to disable that feature. Are you referring to the fact that when you call a function with a writes clause, VCC forgets information? Or about the fact that we verify one function at a time? Neither of these can be changed without fairly deep changes in VCC verification methodology... Michal holgerblasum Jun 18, 2010 at 9:46 AM Hi Michal, to follow up on this one: I am referring to the fact that when I call a function with a writes clause, VCC forgets information. I was suggesting especially to keep track of what the verification engineer had asserted manually before the function call via "(assert(in_domain(...,...))" tracking of which even can be done by preprocessing in the above example (so it wouldn't necessarily be a fairly deep change to VCC verification methodology). Cheers, Holger