facebook / infer

A static analyzer for Java, C, C++, and Objective-C
http://fbinfer.com/
MIT License
14.8k stars 2k forks source link

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

Open master-q opened 11 months ago

master-q commented 11 months ago

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

jvillard commented 3 months ago

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?

master-q commented 3 months ago

Yes. It's a good idea!