Support for asm goto

[vesalvojdani]

Maybe we should document the set of GCC extensions that are supported at some point, but I'm more interested now in a demand-driven push to list stuff that are essential for compiling more recent versions of the Linux kernel. Maybe easiest to do that one at a time. I'm not 100% sure, but I think recent versions are not possible to analyze without asm goto. [Later update: Actually, this goto has been there for a long time and somehow our current headers manage to avoid it. Maybe this isn't essential, but I'll still post this issue in case it is needed.]

We can handle asm volatile, but this one also requires labels. Now, the grammar is a little bit hacky. Two alternatives and then "in the last form, asm-qualifiers contains goto (and in the first form, not)."

Here's the sort of code that needs to get through (from arch/x86/include/asm/jump_label.h):

#define __stringify_1(x...)	#x
#define __stringify(x...)	__stringify_1(x)

#define __ASM_FORM(x, ...)		" " __stringify(x,##__VA_ARGS__) " "
#define __ASM_SEL(a,b)		__ASM_FORM(b)

#define _ASM_PTR	__ASM_SEL(.long, .quad)
#define _ASM_ALIGN	__ASM_SEL(.balign 4, .balign 8)


#define JUMP_TABLE_ENTRY				\
	".pushsection __jump_table,  \"aw\" \n\t"	\
	_ASM_ALIGN "\n\t"				\
	".long 1b - . \n\t"				\
	".long %l[l_yes] - . \n\t"			\
	_ASM_PTR "%c0 + %c1 - .\n\t"			\
	".popsection \n\t"


#define __stringify_1(x...)	#x
#define __stringify(x...)	__stringify_1(x)

#define asm_volatile_goto(x...)      do { asm goto(x); asm (""); } while (0)

static int arch_static_branch(const int key, const int branch)
{
	asm_volatile_goto("1:"
		".byte " __stringify(BYTES_NOP5) "\n\t"
		JUMP_TABLE_ENTRY
		: :  "i" (key), "i" (branch) : : l_yes);

	return 0;
l_yes:
	return 1;
}

int main () {
	return 0;
}

[michael-schwarz]

We actually have a student on the Munich side (@bottbenj, chiefly advised by @jerhard ) who, for his Bachelor's thesis will enhance Goblint with:

• more reasonable support for inline assembly (relying on the annotations instead of just invalidating absolutely everything) and
• support for longjump/setjmp.

We already discussed assembly gotos as something we also want to be able to handle.

How time critical is this to you? If it is not urgently needed right now, I'd suggest we don't do it ourselves, but let our student do it.

[bottbenj]

Just parsing asm gotos is actually not that big of an issue (see https://github.com/bottbenj/cil/tree/feature/asm-analysis-v2, the analyzer changes this requires are pretty trivial) the issue for actually analyzing them is actually creating a CFG that includes the goto edges as currently ASM is a cil instruction and they can only have one successor, so ASM would have to be changed to be a statement directly, which requires changes in about 80 locations in CIL (probably more due to knock-on issues), so i am pushing that back to have time for the other parts of my thesis. As a quick work-around the a switch to the various jump targets could be inserted after the asm to effectively fix the CFG, but that would either breaks the actual execution semantics of the cil output (in a way that is not relevant for analysis) or require a variable the at runtime has a constant value but the analysis considers unknown.

Depending on the importance and requirements of this issue we could either:

• Merge those changes together with the minimal changes in the analyzer to make it compile -> asm goto can be parsed and will be ignored like all other asm
• Create the switch hack and merge that possibly together with better analysis of asm statements in general
• wait until i get around to handle asm gotos properly

[michael-schwarz]

@vesalvojdani For the benchmarks you were considering here, would it be enough to just ignore them? Because then I would suggest we merge the minimal fixes needed for parsing, and then wait until we have a proper implementation.
The switch approach sounds sorta hacky, so I am not too keen on having this in Goblint.

[sim642]

Regarding the control flow for asm goto, it might be worth looking at what CIL does with computed gotos. Because it seems like CIL already converts them to a switch (at least in the default configuration which Goblint uses):

cil/src/cil.mli

Lines 2034 to 2036 in 56f5f9a

	(** Whether to use GCC's computed gotos. By default, do not use them and
	* replace them by a switch. *)
	val useComputedGoto: bool ref

Thus it would actually be quite consistent to do the same for asm gotos. And it wouldn't introduce any hacks that aren't already there.

[michael-schwarz]

Yes, but that handling of computed gotos is ugly as hell, I'd suggest rather not pile on this ugliness if we can avoid it. 😊

[sim642]

This might get a big off-topic, but in what sense is that so ugly. The alternative is having to handle ComputedGoto inside Goblint directly, but how would you even construct a CFG, let alone transfer functions for that without more-or-less implementing the same construct of converting it to something switch-like.
For asm goto it would probably even be much simpler to construct that switch, since the targets are directly available instead of having to collect them elsewhere from the AST and whatnot. Thus it should be a very local change to just insert a directly constructed switch after the asm goto, as opposed to changing the entire AST to move ASM out of instr and into stmtkind directly. Seems to me like much less work to get it initially working.