Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

add linux-headers/arch/arm64 since we only have x86 #312

Open
Tracked by #311
vogler opened this issue Aug 3, 2021 · 6 comments
Open
Tracked by #311

add linux-headers/arch/arm64 since we only have x86 #312

vogler opened this issue Aug 3, 2021 · 6 comments
Labels

Comments

@vogler
Copy link
Collaborator

vogler commented Aug 3, 2021

On Apple M1 many regression tests fail due to the wrongly used x86 headers:

goblint/analyzer/linux-headers/arch/x86/include/asm/pvclock.h:56:2: error: #error implement me!
  -    56 | #error implement me!
  -       |  ^~~~~
  - Goblint: Preprocessing failed.

pvclock.h:

#ifdef __i386__
	__asm__ (
		"mul  %5       ; "
		"mov  %4,%%eax ; "
		"mov  %%edx,%4 ; "
		"mul  %5       ; "
		"xor  %5,%5    ; "
		"add  %4,%%eax ; "
		"adc  %5,%%edx ; "
		: "=A" (product), "=r" (tmp1), "=r" (tmp2)
		: "a" ((u32)delta), "1" ((u32)(delta >> 32)), "2" (mul_frac) );
#elif defined(__x86_64__)
	__asm__ (
		"mulq %[mul_frac] ; shrd $32, %[hi], %[lo]"
		: [lo]"=a"(product),
		  [hi]"=d"(tmp)
		: "0"(delta),
		  [mul_frac]"rm"((u64)mul_frac));
#else
#error implement me!
#endif

I think these headers are pretty old, maybe it's also a good idea to update them.

@michael-schwarz
Copy link
Member

maybe it's also a good idea to update them.

If CIL can parse the newer ones, absolutely!

@vogler
Copy link
Collaborator Author

vogler commented Sep 10, 2021

@vesalvojdani I tried to use a newer kernel, but config fails on my machine:

$ mv linux-headers linux-headers-old
$ wget https://cdn.kernel.org/pub/linux/kernel/v5.x/linux-5.14.2.tar.xz
$ tar xf linux-5.14.2.tar.xz
$ mv linux-5.14.2 linux-headers
$ make test
Testing 00/14 sanity/startstate	 Status: 1 (error)
  - /Users/voglerr/goblint/analyzer/linux-headers/include/linux/kconfig.h:5:10: fatal error: generated/autoconf.h: No such file or directory
  -     5 | #include <generated/autoconf.h>
  -       |          ^~~~~~~~~~~~~~~~~~~~~~
  - compilation terminated.
  - Goblint: Preprocessing failed.
$ cd linux-headers
$ make
***
*** Configuration file ".config" not found!
***
*** Please run some configurator (e.g. "make oldconfig" or
*** "make menuconfig" or "make xconfig").
***
$ make menuconfig
gcc -no-integrated-as --prefix= -Werror=unknown-warning-option: unknown assembler invoked
scripts/Kconfig.include:50: Sorry, this assembler is not supported.
make[2]: *** [menuconfig] Error 1
make[1]: *** [menuconfig] Error 2
make: *** [__sub-make] Error 2
$ cp ../linux-headers-old/config.txt .config
$ make oldconfig
gcc -no-integrated-as --prefix= -Werror=unknown-warning-option: unknown assembler invoked
scripts/Kconfig.include:50: Sorry, this assembler is not supported.

@sim642
Copy link
Member

sim642 commented Sep 10, 2021

I think @vesalvojdani tried something (on non-M1 Mac I guess), but then found out that newer kernels use some C11 features like _Generic, which CIL (and Goblint) don't currently support (goblint/cil#13, goblint/cil#24).

@sim642 sim642 added the feature label Sep 10, 2021
@vogler
Copy link
Collaborator Author

vogler commented Sep 10, 2021

We can also use an older version (our config.txt says Linux/x86 4.0.0), but idk if the introduction of those C11 features happened before arch/arm64 was added.

@vogler
Copy link
Collaborator Author

vogler commented Sep 10, 2021

Also tried make headers_install ARCH=arm64 INSTALL_HDR_PATH=usr (doc) which needs no config, but that's not enough: analyzer/linux-headers/include/linux/kconfig.h: No such file or directory.

@vogler
Copy link
Collaborator Author

vogler commented Sep 10, 2021

let arch_dir = kernel_root ^ "/arch/x86/include" in

This (and #54) would then be determined by an option arch defaulting to the current machine's arch.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

3 participants