make sizes of primitive types configurable with current machine as default

[vogler]

Cil's defaults are generated from src/machdep-ml.c.in and then stored in _build/machdep.ml.

• [ ] make Machdep.theMachine configurable in goblint
• [ ] provide default configurations {intel, arm} {32bit, 64bit} {linux, macOS}

[vogler]

Some more context from other comments:

---

Current generated machdep.ml attached below. Remove the msvc stuff, gcc -> gcc_arm64_macos, generate and add the same for x86_64_linux etc. theMachine is already a reference, just need to set it from goblint to the current machine or option if provided (and then also pass it for preprocessing as mentioned by Michael above).

(* This module was generated automatically by code in Makefile and machdep-ml.c *)
type mach = {
  version_major: int;     (* Major version number *)
  version_minor: int;     (* Minor version number *)
  version: string;        (* gcc version string *)
  underscore_name: bool;  (* If assembly names have leading underscore *)
  sizeof_short: int;      (* Size of "short" *)
  sizeof_int: int;        (* Size of "int" *)
  sizeof_bool: int;       (* Size of "_Bool" *)
  sizeof_long: int ;      (* Size of "long" *)
  sizeof_longlong: int;   (* Size of "long long" *)
  sizeof_ptr: int;        (* Size of pointers *)
  sizeof_float: int;      (* Size of "float" *)
  sizeof_double: int;     (* Size of "double" *)
  sizeof_longdouble: int; (* Size of "long double" *)
  sizeof_floatcomplex: int;      (* Size of "float _Complex" *)
  sizeof_doublecomplex: int;     (* Size of "double _Complex" *)
  sizeof_longdoublecomplex: int; (* Size of "long double _Complex" *)
  sizeof_void: int;       (* Size of "void" *)
  sizeof_fun: int;        (* Size of function *)
  size_t: string;         (* Type of "sizeof(T)" *)
  wchar_t: string;        (* Type of "wchar_t" *)
  alignof_short: int;     (* Alignment of "short" *)
  alignof_int: int;       (* Alignment of "int" *)
  alignof_bool: int;      (* Alignment of "_Bool" *)
  alignof_long: int;      (* Alignment of "long" *)
  alignof_longlong: int;  (* Alignment of "long long" *)
  alignof_ptr: int;       (* Alignment of pointers *)
  alignof_enum: int;      (* Alignment of enum types *)
  alignof_float: int;     (* Alignment of "float" *)
  alignof_double: int;    (* Alignment of "double" *)
  alignof_longdouble: int;  (* Alignment of "long double" *)
  alignof_floatcomplex: int;     (* Alignment of "float _Complex" *)
  alignof_doublecomplex: int;    (* Alignment of "double _Complex" *)
  alignof_longdoublecomplex: int;  (* Alignment of "long double _Complex" *)
  alignof_str: int;       (* Alignment of strings *)
  alignof_fun: int;       (* Alignment of function *)
  alignof_aligned: int;   (* Alignment of anything with the "aligned" attribute *)
  char_is_unsigned: bool; (* Whether "char" is unsigned *)
  const_string_literals: bool; (* Whether string literals have const chars *)
  little_endian: bool; (* whether the machine is little endian *)
  __thread_is_keyword: bool; (* whether __thread is a keyword *)
  __builtin_va_list: bool; (* whether __builtin_va_list is builtin (gccism) *)
}
let gcc = {
(* Generated by code in src/machdep-ml.c *)
     version_major    = 11;
     version_minor    = 1;
     version          = "11.1.0";
     sizeof_short               = 2;
     sizeof_int                 = 4;
     sizeof_bool                = 1;
     sizeof_long                = 8;
     sizeof_longlong            = 8;
     sizeof_ptr                 = 8;
     sizeof_float               = 4;
     sizeof_double              = 8;
     sizeof_longdouble          = 8;
     sizeof_floatcomplex        = 8;
     sizeof_doublecomplex       = 16;
     sizeof_longdoublecomplex   = 16;
     sizeof_void                = 1;
     sizeof_fun                 = 1;
     size_t                     = "unsigned long";
     wchar_t                    = "int";
     alignof_short              = 2;
     alignof_int                = 4;
     alignof_bool               = 1;
     alignof_long               = 8;
     alignof_longlong           = 8;
     alignof_ptr                = 8;
     alignof_enum               = 4;
     alignof_float              = 4;
     alignof_double             = 8;
     alignof_longdouble         = 8;
     alignof_floatcomplex       = 4;
     alignof_doublecomplex      = 8;
     alignof_longdoublecomplex  = 8;
     alignof_str                = 1;
     alignof_fun                = 4;
     alignof_aligned            = 16;
     char_is_unsigned           = false;
     const_string_literals      = true;
     underscore_name            = false;
     __builtin_va_list          = true;
     __thread_is_keyword        = true;
     little_endian              = true;
}
let hasMSVC = false
let msvc = gcc
let theMachine : mach ref = ref gcc

Originally posted by @vogler in https://github.com/goblint/analyzer/issues/293#issuecomment-888518534

That is true. Didn't go through the record, but hopefully all those things (or the ones we care about) are determined by your combination of OS+Arch+GCC which can be detected.

Originally posted by @vogler in https://github.com/goblint/analyzer/issues/293#issuecomment-888529855

[sim642]

For future reference, Frama-C contains a bunch of machdep definitions for different architectures: https://git.frama-c.com/pub/frama-c/-/blob/master/src/kernel_internals/runtime/machdeps.ml.

[michael-schwarz]

Frama-C 27.0 Cobalt now has better support for machdep. We might consider switching the one that CIL currently uses with this new mechanism. Posting here as we don't have an issue for this on the CIL repo yet.

New machdep mechanism, based on YAML files New script for generating machdeps from a C11 compiler

[sim642]

Just using the YAML format instead of CIL's current one or even defining ILP32 and LP64 in OCaml directly (because they should be fully fixed) won't really make a difference. Except that using their mechanism would pull LGPLv2 code into Goblint, which we probably don't want.

For SV-COMP soundness, we just need two fixed Machdep record definitions in OCaml to use instead of the current machine one. An actual generic solution is far from so simple though, because it also requires headers for all the other architectures for preprocessing. That's not needed for SV-COMP where everything is (hopefully correctly) preprocessed.