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 Gerwin.Klein@nicta.com.au 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 david.greve@rockwellcollins.com 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 Devel@sel4.systems 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.