Remove ARINC analyses

[michael-schwarz]

This removes the ARINC analyses from the current version of Goblint, they will remain available in the last release.

References #811

[sim642]

On top of my head, I remember there are these (de)obfuscations related to ARINC as well: #460 (comment) and #460 (comment).

[michael-schwarz]

The second one was already removed before, I also removed the first now.

[sim642]

The second one was already removed before, I also removed the first now.

Unless I'm mistaken, it's still there on the current master:

analyzer/src/util/goblintutil.ml

Lines 121 to 135 in 26fd6ce

	let scrambled = try Sys.getenv "scrambled" = "true" with Not_found -> false
	(* typedef struct {
	PROCESS_NAME_TYPE NAME;
	SYSTEM_ADDRESS_TYPE ENTRY_POINT;
	STACK_SIZE_TYPE STACK_SIZE;
	PRIORITY_TYPE BASE_PRIORITY;
	SYSTEM_TIME_TYPE PERIOD;
	SYSTEM_TIME_TYPE TIME_CAPACITY;
	DEADLINE_TYPE DEADLINE;
	} PROCESS_ATTRIBUTE_TYPE; *)
	let arinc_name = if scrambled then "M161" else "NAME"
	let arinc_entry_point = if scrambled then "M162" else "ENTRY_POINT"
	let arinc_base_priority = if scrambled then "M164" else "BASE_PRIORITY"
	let arinc_period = if scrambled then "M165" else "PERIOD"
	let arinc_time_capacity = if scrambled then "M166" else "TIME_CAPACITY"

[michael-schwarz]

Before your comment is what I meant by before 😉

[sim642]

Ah, sorry, right.

The test fails on MacOS. I guess it's because memcpy might be a wrapper/macro for some other internal (fortified?) function there. The solution probably is to handle some extra name variant of it (not sure what exactly).
It's odd though because #391 also contains a similar change, but doesn't show a similar failure.

[michael-schwarz]

Yes, it looks like it should be __builtin___memcpy_chk. However, for some reason than the assert succeeds instead of definitely failing, so there still is something fishy going on.

[michael-schwarz]

Actually, the memcpy is a bit insane. It is broken if you pull out the AddrOf to somewhere else as it does not in fact dereference its argument 🙃.

void test_memcpy_two() {
  int dest = 0;
  int src = 1;

  int* destp = &dest;
  int* srcp = &src;

  memcpy(destp, srcp, sizeof(int));

  __goblint_check(dest == 0); //FAIL
  __goblint_check(src == 1);
}

[sim642]

However, for some reason than the assert succeeds instead of definitely failing, so there still is something fishy going on.

It was actually unknown instead of fail, which makes sense, because it fell back to the unknown function handling via LibraryFunctions, which handles __builtin___memcpy_chk by completely invalidating the destination. The result of that could also be 0 then.

It is broken if you pull out the AddrOf to somewhere else as it does not in fact dereference its argument upside_down_face.

That's what #729 also fixed but it's still just on interactive.

[sim642]

There's also src/extract/pml_arinc.ml.