diff --git a/.gitignore b/.gitignore index b2722714..b8c2e8d1 100644 --- a/.gitignore +++ b/.gitignore @@ -18,9 +18,10 @@ doc/generated *.egg-info *.swp *.egg -python/test/** +test/** tags ocaml/src/bincat_native ocaml/test/.cache ocaml/src/bincat_ver.ml ocaml/src/armv8A_ppx +*.no diff --git a/ocaml/src/disassembly/cfa.ml b/ocaml/src/disassembly/cfa.ml index 5c80497d..7b266b93 100644 --- a/ocaml/src/disassembly/cfa.ml +++ b/ocaml/src/disassembly/cfa.ml @@ -226,26 +226,28 @@ struct (* main function to initialize memory locations (Global/Stack/Heap) both for content and tainting *) - (* this filling is done by iterating on corresponding tables in Config *) - let init_mem domain region content_tbl = - Hashtbl.fold (fun (addr, nb) content domain -> - let addr' = Data.Address.of_int region addr !Config.address_sz in - Domain.set_memory_from_config addr' Data.Address.Global content nb domain - ) content_tbl domain - (* end of init utilities *) - (*************************) - - (* CFA creation. - Return the abstract value generated from the Config module *) - let init_abstract_value () = - let d = List.fold_left (fun d r -> Domain.add_register r d) (Domain.init()) (Register.used()) in + (* this filling is done by iterating on corresponding lists in Config *) + let init_mem domain region content_list = + List.fold_left (fun domain entry -> let addr, nb = fst entry in + let content = snd entry in + L.debug (fun p->p "init: %x" (Z.to_int addr)); + let addr' = Data.Address.of_int region addr !Config.address_sz in + Domain.set_memory_from_config addr' Data.Address.Global content nb domain + ) domain (List.rev content_list) + (* end of init utilities *) + (*************************) + + (** CFA creation. + Return the abstract value generated from the Config module *) + let init_abstract_value () = + let d = List.fold_left (fun d r -> Domain.add_register r d) (Domain.init()) (Register.used()) in (* initialisation of Global memory + registers *) - let d' = init_mem (init_registers d) Data.Address.Global Config.memory_content in + let d' = init_mem (init_registers d) Data.Address.Global !Config.memory_content in (* init of the Stack memory *) - let d' = init_mem d' Data.Address.Stack Config.stack_content in + let d' = init_mem d' Data.Address.Stack !Config.stack_content in (* init of the Heap memory *) - init_mem d' Data.Address.Heap Config.heap_content - + init_mem d' Data.Address.Heap !Config.heap_content + let init_state (ip: Data.Address.t): State.t = let d' = init_abstract_value () in { diff --git a/ocaml/src/frontend/parser.mly b/ocaml/src/frontend/parser.mly index 2f93d2c3..034f4c04 100644 --- a/ocaml/src/frontend/parser.mly +++ b/ocaml/src/frontend/parser.mly @@ -386,9 +386,9 @@ state_item: | REG LEFT_SQ_BRACKET r=STRING RIGHT_SQ_BRACKET EQUAL v=init { init_register r v } - | MEM LEFT_SQ_BRACKET m=repeat RIGHT_SQ_BRACKET EQUAL v=init { Hashtbl.add Config.memory_content m v } - | STACK LEFT_SQ_BRACKET m=repeat RIGHT_SQ_BRACKET EQUAL v=init { Hashtbl.add Config.stack_content m v } - | HEAP LEFT_SQ_BRACKET m=repeat RIGHT_SQ_BRACKET EQUAL v=init { Hashtbl.add Config.heap_content m v } + | MEM LEFT_SQ_BRACKET m=repeat RIGHT_SQ_BRACKET EQUAL v=init { Config.memory_content := (m, v) :: !Config.memory_content } + | STACK LEFT_SQ_BRACKET m=repeat RIGHT_SQ_BRACKET EQUAL v=init { Config.stack_content := (m, v) :: !Config.stack_content } + | HEAP LEFT_SQ_BRACKET m=repeat RIGHT_SQ_BRACKET EQUAL v=init { Config.heap_content := (m, v) :: !Config.heap_content } repeat: | i=INT { i, 1 } diff --git a/ocaml/src/utils/config.ml b/ocaml/src/utils/config.ml index 52a27e41..185a4add 100644 --- a/ocaml/src/utils/config.ml +++ b/ocaml/src/utils/config.ml @@ -21,7 +21,6 @@ let fun_unroll = ref 50;; let loglevel = ref 3;; let module_loglevel: (string, int) Hashtbl.t = Hashtbl.create 5;; - (* set of values that will not be explored as values of the instruction pointer *) module SAddresses = Set.Make(Z) let blackAddresses = ref SAddresses.empty @@ -68,7 +67,7 @@ let mode = ref Protected let in_mcfa_file = ref "";; let out_mcfa_file = ref "";; - + let load_mcfa = ref false;; let store_mcfa = ref false;; @@ -113,9 +112,9 @@ let fs = ref Z.zero let gs = ref Z.zero (* if true then an interleave of backward then forward analysis from a CFA will be processed *) -(** after the first forward analysis from binary has been performed *) +(** after the first forward analysis from binary has been performed *) let interleave = ref false - + type tvalue = | Taint of Z.t | TMask of Z.t * Z.t (* second element is a mask on the first one *) @@ -130,20 +129,19 @@ let reg_override: (Z.t, ((string * (Register.t -> tvalue)) list)) Hashtbl.t = Ha let mem_override: (Z.t, (Z.t * tvalue) list) Hashtbl.t = Hashtbl.create 5 let stack_override: (Z.t, (Z.t * tvalue) list) Hashtbl.t = Hashtbl.create 5 let heap_override: (Z.t, (Z.t * tvalue) list) Hashtbl.t = Hashtbl.create 5 - - -(* tables for the initialisation of the global memory, stack and heap *) -(* first element in the key is the address ; second one is the number of repetition *) -type ctbl = (Z.t * int, cvalue * (tvalue option)) Hashtbl.t + +(* lists for the initialisation of the global memory, stack and heap *) +(* first element is the key is the address ; second one is the number of repetition *) +type mem_init_t = ((Z.t * int) * (cvalue * (tvalue option))) list let register_content: (string, (Register.t -> cvalue * tvalue option)) Hashtbl.t = Hashtbl.create 10 -let memory_content: ctbl = Hashtbl.create 10 -let stack_content: ctbl = Hashtbl.create 10 -let heap_content: ctbl = Hashtbl.create 10 +let memory_content: mem_init_t ref = ref [] +let stack_content: mem_init_t ref = ref [] +let heap_content: mem_init_t ref = ref [] type sec_t = (Z.t * Z.t * Z.t * Z.t * string) list ref let sections: sec_t = ref [] - + let import_tbl: (Z.t, (string * string)) Hashtbl.t = Hashtbl.create 5 (* tainting and typing rules for functions *) @@ -151,7 +149,6 @@ type taint_t = | No_taint | Buf_taint | Addr_taint - (** data stuctures for the assertions *) let assert_untainted_functions: (Z.t, taint_t list) Hashtbl.t = Hashtbl.create 5 @@ -167,11 +164,11 @@ let typing_rules : (string, TypedC.ftyp) Hashtbl.t = Hashtbl.create 5 let clear_tables () = Hashtbl.clear assert_untainted_functions; Hashtbl.clear assert_tainted_functions; - Hashtbl.clear memory_content; - Hashtbl.clear stack_content; - Hashtbl.clear heap_content; Hashtbl.clear import_tbl; Hashtbl.clear reg_override; Hashtbl.clear mem_override; Hashtbl.clear stack_override; - Hashtbl.clear heap_override + Hashtbl.clear heap_override; + memory_content := []; + stack_content := []; + heap_content := [];