ableC extension ideas

[remexre]

Making a discussion for this because Slack #ideas disappears after a while...

[remexre]

ableC-contracts:

On declarations:

// whatever.h
int foo(int x) with preconditions {
	x > 0;
	x < 20;
} with postconditions {
	return > x;
};

// whatever.c
int foo(int x) { return x * 2; }

On definitions:

int bar(int x) {
	return x;
} with preconditions {
	x != 3;
}

These would get transformed to something like (when building with contracts; we'd probably want something like NDEBUG too):

// whatever.h

int _ableC_contracts__real_foo(int x);

static inline int foo(int x) {
	_ableC_contracts__assert(x > 0, "x > 0", "whatever.h", 13 /* line */, 4 /* col */);
	_ableC_contracts__assert(x < 20, "x < 20", "whatever.h", 16, 20);
	int _ableC_contracts__return = _ableC_contracts__real_foo(x);
	_ableC_contracts__assert(_ableC_contracts__return > x, "return > x", "whatever.h", 16, 4);
	return _ableC_contracts__return;
}

// whatever.c

int _ableC_contracts__real_foo(int x) {
	return x * 2;
}

---

It might make sense for whoever implements this to read thru the discussion about C++'s contracts proposal; I'm not too familiar with the details, but I think one of the points of contention is whether some contracts should be checked at compile-time only, runtime-only, or at both runtime and compile-time. There are almost certainly more design questions that they've explored, though.

For the compile-time vs run-time one, it might make sense to parameterize contracts?

_Bool is_even_parity(int x);

int bar(int x) with precondition(assert) {
	x > 0;
} with precondition(fancy_bounded_model_checking_solver_thing) {
	is_even_parity(x);
}

As perhaps hinted by fancy_bounded_model_checking_solver_thing, this'd also be a cool way to try and integrate with work from people doing e.g. symbolic execution of C.

---

Other things:

• Should side-effects in contracts still happen when building NDEBUG? I'm tbh divided on this; in an ideal world it'd be a compiler error to have side-effects in a contract... On the one hand, it'd be unfortunate if an expensive computation couldn't be proven to be side-effect free (e.g. because GCC can't prove an assertion never occurs), but "this side-effect only happens in debug builds" sounds bad too...
• Should we do something to make it possible (e.g. with a script) to see how many assertions were left in the program after GCC's optimizer runs? I've heard (I think in the context of Midori) that modern compilers are really good at removing >90% of contract-related assertions from programs written in the design-by-contract style (e.g. every function has explicit null checks in its contracts)
• Is the translation I wrote above actually optimal for being able to eliminate contracts, keeping in mind LTO and outlining?
• with invariants { $E } => with preconditions { $E } with postconditions { $E } shorthand?
• shorter syntax? int foo(int x) pre { x > 0; x < 20; } post { return > x; }?

[remexre]

"compiled" ableC-regex

Instead of bool b = /foo/ ~= s; compiling to bool b = match("foo", s);, we could compile it to the actual C code that does the matching. Section 5 of Brzozowski's Derivatives of Regular Expressions goes through the process of doing this with derivatives; basically:

• compute every "reachable" derivative modulo a very simple similarity relation (Definition 5.2), those are your states
• D_{ch}(S1) = S2 -> there's a transition from S1 to S2 on the character ch
• \delta(S) -> S is an accept state

To compile this:

• make a goto label for each state
• in each body, (pseudo-Silver w/ silver-ableC)

  ${top.label}:
    switch(*s++) {
    case '\0':
        return ${top.isAccept};
    ${transitions.map(\(ch, label) -> $ableC_Stmt{ case ${ch}: goto ${label}; })}

This is probably a good undergrad project.

-- Me, who has demonstrated an inability to scope undergrad projects.

Section 6 of the Brzozowski paper goes through turning this into a proper lexer. Nice syntax for that might be like:

// I like this taking a char** or string* better because
// it makes it more obvious that this changes what s is
// pointing to.
lex switch(&s) {
case "if": return TOK_IF;
case /[a-zA-Z][a-zA-Z0-9]*/: return TOK_ID;
}

Prior art here is OCaml's sedlex. Though, that syntax might not respect case order because of maximal-munch (idk if sedlex does) which might be surprising.

logos would be the other option; syntax for that might be like:

lexable
enum token {
  TOK_IF ~= "if",
  TOK_ID ~= /[a-zA-Z][a-zA-Z0-9]*/,
};

[remexre]

ableC-modules

It would be nice to have a real module system, to get rid of #include.

One possible design, that pretends other preprocessor usage has magically disappeared:

• Somewhere, you list the .xc and .c files composing your module.
• Translate each foo.xc to foo.xcmoi (MOdule Interface): this is approximately "compute a header file and serialize it."
• Combine the .xcmoi files into a single mymodule.xcmod: maybe this is just cat
• Translate each foo.xc with the mymodule.xcmod (and any dependencies' .xcmods) into foo.xcmoe (MOdule Environment): This just filters "what does foo.xc actually need from the .xcmods" out, and is so that build systems don't need to rebuild every .xc file on every change, only those that depended on the change. The contents of this probably don't actually matter, so long as they change when the parts of the .xcmod the .xc depend on have changed -- it might be simplest to make it the same format as the .xcmod itself, so that this step can be optional.
• Translate each foo.xc with the foo.xcmoe into foo.o: Finally, this is the actual compilation step.

This is probably way slower without Nailgun or something else that improves our start-up time...