@cella-lang/cfamily

The C family's core for the Cella proof checker, as a compiled module pack: C11 and C++17 as a deep embedding. A program is a data value (the JSON of its syntax tree), and its type checking and execution are ordinary functions on that value.

The core has no entries of its own. Use one of its three branches, each a package with its own verdict, type query and debugger; a branch lists this package in its index.json and loads it first.

The packages depend on each other as machine <- cfamily <- c, cpp <- arduino.

Programs

A program is the JSON of cfamily.syntax: {"k": "prog", "n": "<node>", "lang": …, "items": […]}, with "board" and the host's inputs over time ("inputs") for a board. Every constructor carries the node label of the editor that made it ("n"), and a verdict, a stop of the debugger or a type error names the node.

Text is Unicode on the host's side and UTF-8 bytes in the program, as with clang and gcc: string literals, the input and the debugger's fed input are encoded ("é" is two bytes, sizeof("é") is 3); the output is the bytes the program wrote, decoded, with U+FFFD for an invalid sequence.

Verdicts

A branch's verdict src input fuel returns:

{"verdict": "reject", "basis": "computed", "exit": null, "out": "",
 "problems": [{"kind": "ubOverflow", "category": "error", "at": "<node>", "clause": "C++17 [expr]p4", "reason": "signed overflow",
               "params": {}, "structured": false}]}

• verdict: accept; reject (a type error, or undefined behavior); unknown (the standard allows results that change the output, a construct the model does not have yet, or the step limit); or invalid (the JSON is not a program, or not one for this branch: a C program for a board, a C++ program sent to c).
• basis: computed when the verdict comes from running the semantics, kernel when both kernels proved it (kernel_verdict_in in cella-lang, with the branch's verdict: kernel_verdict_in("cpp", "cpp.verdict", …)).
• exit: the exit status, or null when the program did not end.
• out: standard output.
• problems: what decided a reject or an unknown, each with its kind, category, node, the standard's clause (C11 for C programs, C++17 for C++ ones; the C library is C11's in both) and reason. The category is one of six, by which a host shows the problem: error (the program did not check, or reached undefined behavior), unsupported (a construct the model does not have yet), indeterminate (the step limit, an unspecified result), termination (abort, an uncaught exception), incomplete (an empty slot) and invalid (the JSON is not a program). A problem also has params, its details as strings and booleans (an integer in decimal; a detail not known is absent), and structured: a structured problem's reason is made from its kind and params (a developer's log; a host reads the params), one not structured yet has "params": {} and "structured": false. The kinds, whether each is structured, and the params of the structured ones are listed in verdict-kinds.json (shipped with this package; the C, C++ and Arduino branches share it). An undeclared name is undeclared with name, what (variable, function or name) and, when a standard header declares it, header. Two calls in an unspecified order (C11 6.5.2.2p10, C++17 [intro.execution]p11) whose effects could conflict are run in both orders and the states compared: a difference is ubOrder with difference (output: what the two orders wrote differs, output being what the order run, left to right as clang, wrote at that point and otherOutput the other's; state: the same output, other values left; end: one of them did not end normally). orderUncompared is an order that may matter but was not compared: why is budget (comparing ran past its budget, half the fuel) or access (a call's effect could change an access outside the calls, as x + f() with f writing x). The verdict's quantifier is this input: each point where the order matters, its two orders with the others left to right (a recursive call meeting the point again inside its own comparison is not compared again).
• assumes (always there, empty when nothing is assumed): the implementation's choices the result depends on, [{implementation, choice}]. The library makes them as libc++ does (vector.growth: capacity and when push_back reallocates; library.what: the text of what()); a choice of another implementation names it (gcc:union.typePunning).
• A program on a board adds the pins, the environment and the clock (see @cella-lang/arduino).

Type query

A branch's types src candidates answers what a block editor asks of a program that may have holes. A hole is {"k": "eHole", "n": "<node>#<slot>"} (or sHole where the syntax needs a statement); a program with holes has the verdict unknown with a hole problem. candidates is a JSON array of types written as C or C++ ("int", "double", "char *", "std::string", "struct S"), the same way the result prints them.

{"nodes": {"<node>": "int"},
 "slots": {"<node>#<slot>": {"display": "expects int", "expects": "int",
                             "fits": {"double": {"level": "narrowing"}, "char *": {"level": "no", "reason": "…"}}}},
 "errors": [{"at": "<node>", "reason": "…"}]}

• nodes: the type of each expression and declaration, before implicit conversions.
• fits: exact (no conversion), convert (an implicit conversion without loss), narrowing (with loss), no (rejected, with the reason). The type checker decides: the hole stands for a value of the candidate type, and the level comes from the conversions it puts around it, so overloads, auto and std::cout << ? follow the real rules.
• expects: the slot's target type when every type that fits is converted to the same one (int x = ?, a parameter, return ?); null when the slot takes anything or depends on the candidate (std::cout << ?, ? + 1, an overloaded call). display is for developers.
• errors: statements that do not check. Checking goes on after them, so the other nodes still get their types.

Modules

Changes

See CHANGES.md.