Merge branch 'master' into armv8-ppx

.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

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
 	{

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 }

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,28 +129,26 @@ 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 *)
 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 := [];