506303 - IPDL: Use protocol specifications to generate C++ unit tests

Status: RESOLVED WONTFIX

(Core :: IPC, defect)

Description

[Chris Jones [:cjones] inactive; ni?/f?/r? if you need me]

IPDL specifications define all the messages allowed to be passed between two actors and, with protocol state machines, in what sequence these messages may be passed.  This is a rich store of information we can use to automatically check C++ implementations of IPDL actors.

The WMO URL will be the most up-to-date spec for this task, but essentially we want to generate tests that force actors into all their possible states, perhaps multiple times for messages that be sent any number of times.  We also want to force actors to handle protocol-level errors: unexpected values in messages and messages not allowed by particular protocol states.  These tests will check IPDL's infrastructure as well.

Comment 1

[(no longer active)]

Can model checking techniques be used here?  I think ideally we'd end up with a tool to translate IPDL into a model syntax (such as NuSMV) and then have the model checker statically analyze the model for the desired properties.  I'm asking this because the below paragraph seems to be describing a model checker tool :-)

> essentially we
> want to generate tests that force actors into all their possible states,
> perhaps multiple times for messages that be sent any number of times.  We also
> want to force actors to handle protocol-level errors: unexpected values in
> messages and messages not allowed by particular protocol states.

Comment 2

[Chris Jones [:cjones] inactive; ni?/f?/r? if you need me]

Ehsan, what you describe is approximately something I want to do in a separate, complementary project.  This project is literally to generate "unit tests" --- run simply for the sake of increasing the code coverage of the C++ code implementing IPDL specs.  For example, if from C++ I send SetValue("foo", "bar") then I receive "bar" from GetValue("foo").  IPDL can't (and won't) express that property.  I don't know of any model checkers that are good tools for this job; closest is the "concolic" family of checkers, but they have no chance of scaling to Gecko's codebase.

Comment 3

[(no longer active)]

Thanks for the clarification.  Yes, unit tests are definitely needed here as well.  Is there a bug on file for the model checking project?

Comment 4

[Chris Jones [:cjones] inactive; ni?/f?/r? if you need me]

Not yet, but it's listed here: https://wiki.mozilla.org/Content_Processes/Tasks .  It's not near the front of my work queue at the moment.

Comment 5

[Michael Kohler [:mkohler]]

This is a mass change. Every comment has "assigned-to-new" in it.

I didn't look through the bugs, so I'm sorry if I change a bug which shouldn't be changed. But I guess these bugs are just bugs that were once assigned and people forgot to change the Status back when unassigning.

Comment 6

[Jed Davis [:jld] ⟨⏰|UTC-8⟩ ⟦he/him⟧]

This probably won't happen in anything like the form proposed. Protocol state machines no longer exist, and the more general problem of “force actors into all their possible states” now has a collection of practical approaches in the form of coverage-directed fuzzing, which also work for the other use cases in comment #0 (invalid values, messages out of sequence, testing the IPC/serialization infrastructure). Note in particular that comment #2's reference to symbolic execution predates the first public release of AFL by 4 years.