infer icon indicating copy to clipboard operation
infer copied to clipboard

Run clang with original optimizer, which is needed to verify Linux kernel

Open master-q opened this issue 2 years ago • 3 comments

Infer used -O0 option to build AST and foo.o file. But on Linux kernel, the source code is written to be used -O2 optimizer level. We had failure on verifing Linux kernel code with Infer as following:

$ infer -- make CC=clang -j`nproc`
--snip--
  LD      vmlinux.o
  OBJCOPY modules.builtin.modinfo
  GEN     modules.builtin
  MODPOST Module.symvers
WARNING: modpost: vmlinux.o: section mismatch in reference: startup_64_load_idt (section: .text) -> vc_no_ghcb (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: pgtable_init (section: .text) -> pgtable_cache_init (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: real_mode_size_needed (section: .text) -> real_mode_blob (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: real_mode_size_needed (section: .text) -> real_mode_blob_end (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: find_smp_config (section: .text) -> x86_init (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: get_smp_config (section: .text) -> x86_init (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: __get_mem_config_intel (section: .text) -> thread_throttle_mode_init (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: __set_percpu_decrypted (section: .text) -> early_set_memory_decrypted (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: early_get_smp_config (section: .text) -> x86_init (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: real_mode_size_needed (section: .text) -> real_mode_blob (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: real_mode_size_needed (section: .text) -> real_mode_blob_end (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: memblock_alloc_low (section: .text) -> memblock_alloc_try_nid (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: memblock_alloc_from (section: .text) -> memblock_alloc_try_nid (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: memblock_alloc_raw (section: .text) -> memblock_alloc_try_nid_raw (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: memblock_alloc_node (section: .text) -> memblock_alloc_try_nid (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: acpi_arch_set_root_pointer (section: .text) -> x86_init (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: acpi_arch_get_root_pointer (section: .text) -> x86_init (section: .init.data)
WARNING: modpost: vmlinux.o: section mismatch in reference: acpi_sleep_suspend_setup (section: .text) -> acpi_s2idle_setup (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: dmar_fault.rs (section: .data) -> dmar_parse_one_rmrr (section: .init.text)
WARNING: modpost: vmlinux.o: section mismatch in reference: dmar_fault.rs (section: .data) -> dmar_parse_one_andd (section: .init.text)
WARNING: modpost: arch/x86/kvm/kvm-amd.o: section mismatch in reference: svm_hv_hardware_setup (section: .text) -> (unknown) (section: .init.data)
WARNING: modpost: arch/x86/kvm/kvm-amd.o: section mismatch in reference: svm_hv_hardware_setup (section: .text) -> (unknown) (section: .init.data)
WARNING: modpost: arch/x86/kvm/kvm-amd.o: section mismatch in reference: svm_hv_hardware_setup (section: .text) -> (unknown) (section: .init.data)
WARNING: modpost: drivers/platform/x86/thinkpad_acpi.o: section mismatch in reference: volume_set_software_mute (section: .text) -> tpacpi_is_lenovo (section: .init.text)
ERROR: modpost: "kvm_xen_update_runstate_guest" [arch/x86/kvm/kvm.ko] undefined!
ERROR: modpost: "kvm_xen_hypercall" [arch/x86/kvm/kvm.ko] undefined!
ERROR: modpost: "__ubifs_hash_get_desc" [fs/ubifs/ubifs.ko] undefined!
ERROR: modpost: "ubifs_bad_hash" [fs/ubifs/ubifs.ko] undefined!
ERROR: modpost: "__ubifs_node_calc_hash" [fs/ubifs/ubifs.ko] undefined!
ERROR: modpost: "__ubifs_node_verify_hmac" [fs/ubifs/ubifs.ko] undefined!
ERROR: modpost: "ubifs_hmac_wkm" [fs/ubifs/ubifs.ko] undefined!
ERROR: modpost: "ubifs_prepare_auth_node" [fs/ubifs/ubifs.ko] undefined!
ERROR: modpost: "__ubifs_exit_authentication" [fs/ubifs/ubifs.ko] undefined!
ERROR: modpost: "__ubifs_node_insert_hmac" [fs/ubifs/ubifs.ko] undefined!
WARNING: modpost: suppressed 9 unresolved symbol warnings because there were too many)
make[1]: *** [scripts/Makefile.modpost:126: Module.symvers] Error 1

Infer can verify Linux kernel code with this patch and some patches for kernel as following:

https://gist.github.com/master-q/4b3e09e664a15187290f0f22d1bcb3c6

master-q avatar Jul 16 '23 23:07 master-q

Thanks for the report and the patches! This will run clang twice on every file that infer analyses, which could be expensive. Would it be ok to gate this behind an option like --also-run-original-compilation-command?

jvillard avatar Apr 02 '24 09:04 jvillard

Yes. It's a good idea!

master-q avatar Apr 02 '24 10:04 master-q