From b632d4f283654b8c002d7f50b21d8485ac4471c9 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 14 Oct 2019 00:54:00 -0700 Subject: [PATCH] [sledge] Check the input datalayout agrees with assumptions Summary: The analyzer (currently) hard-codes some assumptions about sizes of basic types such as Typ.bool, Typ.siz, etc. Check that these assumptions are satisfied by the input llvm datalayout, and give reasonable error messages otherwise. Reviewed By: ngorogiannis Differential Revision: D17801941 fbshipit-source-id: 4fe484ee0 --- sledge/src/llair/frontend.ml | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/sledge/src/llair/frontend.ml b/sledge/src/llair/frontend.ml index 9219f4305..01116c3cb 100644 --- a/sledge/src/llair/frontend.ml +++ b/sledge/src/llair/frontend.ml @@ -1368,6 +1368,23 @@ let link_in : Llvm.llcontext -> Llvm.lllinker -> string -> unit = fun llcontext link_ctx bc_file -> Llvm_linker.link_in link_ctx (read_and_parse llcontext bc_file) +let check_datalayout llcontext lldatalayout = + let check_size llt typ = + let llsiz = + Int64.to_int_exn (Llvm_target.DataLayout.abi_size llt lldatalayout) + in + let siz = Typ.size_of typ in + if llsiz != siz then + todo "size_of %a = %i != %i" Typ.pp typ llsiz siz () + in + check_size (Llvm.i1_type llcontext) Typ.bool ; + check_size (Llvm.i8_type llcontext) Typ.byt ; + check_size (Llvm.i32_type llcontext) Typ.int ; + check_size (Llvm.i64_type llcontext) Typ.siz ; + check_size + (Llvm_target.DataLayout.intptr_type llcontext lldatalayout) + Typ.ptr + let translate ~models ~fuzzer ~internalize : string list -> Llair.t = fun inputs -> [%Trace.call fun {pf} -> @@ -1395,6 +1412,7 @@ let translate ~models ~fuzzer ~internalize : string list -> Llair.t = let lldatalayout = Llvm_target.DataLayout.of_string (Llvm.data_layout llmodule) in + check_datalayout llcontext lldatalayout ; let x = {llcontext; llmodule; lldatalayout} in let globals = Llvm.fold_left_globals