goblint/analyzer

make sizes of primitive types configurable with current machine as default

vogler opened this issue · 2 comments

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}

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 #293 (comment)

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 #293 (comment)

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.