Yes, I can see how "false" preconditions would do the job and would be easier to work with then 'does not return' semantics.
And I was looking at the post-processed code, so presumably "fail" expanded to "halt" by the time I saw it (and the line numbers may have changed). Thanks, Dave On Sat, Jan 24, 2015 at 10:59 PM, Gerwin Klein <[email protected]> wrote: > Hi David, > > are you referring to line 208 in seL4/src/object/objecttype.c? > https://github.com/seL4/seL4/blob/master/src/object/objecttype.c#L208 > > (As far as I can see, this is the only case in that function that > syntactically does not have a return statement). > > The procedure recycleCap is indeed not obviously type safe, but it is > non-obviously safe ;-) > > We prove that "fail" in C never gets called, i.e. in this case that it > is impossible for recycleCap to be called with a NullCap. This can be for > complex reasons that we would not expect a static analyser to be able to > find, although those cases should be rare. > > In terms of semantics, fail and halt are left without body, and > specified to execute only with precondition "False". > > The actual procedure for proving that fail/halt-statements in C are > never called is somewhat roundabout: we prove that the semantic > representation of the C program refines the design specification under the > assumption that C may do anything it likes wherever there is a "fail" > statement in the design specification (including executing statements with > precondition False, which is only possible in this trivial sense). We then > prove in the design-to-abstract refinement that the design specification > never fails. Together this implies that none of the trivial cases occur in > C. The reason for this roundabout way is that we did that last step first, > before the C proof. > > In this specific case, the requirement "cap ~= cap.NullCap" is mentioned > in the preconditions of lemma recycle_cap_corres in the design-to-abstract > refinement proof: > https://github.com/seL4/l4v/blob/master/proof/refine/Finalise_R.thy#L3877 > > Cheers, > Gerwin > > On 24.01.2015, at 02:27, David Greve <[email protected]> > wrote: > > > I ran the sel4 kernel source through the CIL infrastructure front end: > > http://kerneis.github.io/cil/ > > CIL reported two warnings: > > ../../../../seL4/src/object/cnode.c:867: Warning: Body of function > isMDBParentOf falls-through. Adding a return statement > ../../../../seL4/src/object/objecttype.c:261: Warning: Body of function > recycleCap falls-through and cannot find an appropriate return value > > The first warning looks like a weakness in CIL code analysis .. every > branch of the condition has a return so the procedure doesn't need a > fall-through return. > > The same is not true for the second .. the first branch halt()'s but it > doesn't return .. thus the procedure is not "obviously" type safe. > > I'm curious about the this from a reasoning perspective. > > Perhaps the argument is that halt() never terminates (or it "exits"), > thus it is OK if the procedure doesn't return a value in that case. But > that argument only works if the logic somehow captures the semantics of > halt(). > > Are halt() semantics baked into the correctness proofs? If not, how > is this procedure justified? > > Thanks, > Dave > _______________________________________________ > Devel mailing list > [email protected] > https://sel4.systems/lists/listinfo/devel > > > > ------------------------------ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. >
_______________________________________________ Devel mailing list [email protected] https://sel4.systems/lists/listinfo/devel
