From fb55a4cda6f6ff6b9a68bc21adaafcff25f8f45a Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 11:52:03 +0100 Subject: [PATCH 1/8] replace deprecated Array.create, String.set and String.uppercase with modern equivalents --- src/cil.ml | 4 ++-- src/ext/partial/heap.ml | 2 +- src/frontc/cabs2cil.ml | 4 ++-- src/ocamlutil/bitmap.ml | 2 +- src/ocamlutil/errormsg.ml | 4 ++-- src/ocamlutil/inthash.ml | 2 +- src/ocamlutil/longarray.ml | 2 +- src/ocamlutil/pretty.ml | 6 +++--- 8 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index 63da92793..bd3920744 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -2713,7 +2713,7 @@ let parseInt (str: string) : exp = let l = String.length str in fun s -> let ls = String.length s in - l >= ls && s = String.uppercase (String.sub str (l - ls) ls) + l >= ls && s = String.uppercase_ascii (String.sub str (l - ls) ls) in let l = String.length str in (* See if it is octal or hex *) @@ -5090,7 +5090,7 @@ let makeValidSymbolName (s: string) = | _ -> false in if isinvalid then - String.set s i '_'; + Bytes.set s i '_'; done; s diff --git a/src/ext/partial/heap.ml b/src/ext/partial/heap.ml index 10f48a045..5fbbe372c 100644 --- a/src/ext/partial/heap.ml +++ b/src/ext/partial/heap.ml @@ -9,7 +9,7 @@ type ('a) t = { } let create size = { - elements = Array.create (size+1) (max_int,None) ; + elements = Array.make (size+1) (max_int,None) ; size = 0 ; capacity = size ; } diff --git a/src/frontc/cabs2cil.ml b/src/frontc/cabs2cil.ml index dc185e133..61721cd7d 100644 --- a/src/frontc/cabs2cil.ml +++ b/src/frontc/cabs2cil.ml @@ -1924,7 +1924,7 @@ let rec setOneInit (this: preInit) let pMaxIdx, pArray = match this with NoInitPre -> (* No initializer so far here *) - ref idx, ref (Array.create (max 32 (idx + 1)) NoInitPre) + ref idx, ref (Array.make (max 32 (idx + 1)) NoInitPre) | CompoundPre (pMaxIdx, pArray) -> if !pMaxIdx < idx then begin @@ -3417,7 +3417,7 @@ and doExp (asconst: bool) (* This expression is used as a constant *) let l = String.length str in fun s -> let ls = String.length s in - l >= ls && s = String.uppercase (String.sub str (l - ls) ls) + l >= ls && s = String.uppercase_ascii (String.sub str (l - ls) ls) in match ct with A.CONST_INT str -> begin diff --git a/src/ocamlutil/bitmap.ml b/src/ocamlutil/bitmap.ml index 14d26a08b..33f5f9aea 100644 --- a/src/ocamlutil/bitmap.ml +++ b/src/ocamlutil/bitmap.ml @@ -10,7 +10,7 @@ type t = { mutable nrWords : int; let enlarge b newWords = let newbitmap = if newWords > b.nrWords then - let a = Array.create newWords Int32.zero in + let a = Array.make newWords Int32.zero in Array.blit b.bitmap 0 a 0 b.nrWords; a else diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index 2ffee51cf..857d62b5c 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -217,9 +217,9 @@ let cleanFileName str = else let c = String.get str1 i in if c <> '\\' then begin - String.set str1 copyto c; loop (copyto + 1) (i + 1) + Bytes.set str1 copyto c; loop (copyto + 1) (i + 1) end else begin - String.set str1 copyto '/'; + Bytes.set str1 copyto '/'; if i < l - 2 && String.get str1 (i + 1) = '\\' then loop (copyto + 1) (i + 2) else diff --git a/src/ocamlutil/inthash.ml b/src/ocamlutil/inthash.ml index 8d5bd32af..a6253b9b6 100644 --- a/src/ocamlutil/inthash.ml +++ b/src/ocamlutil/inthash.ml @@ -34,7 +34,7 @@ let resize tbl = let osize = Array.length odata in let nsize = min (2 * osize + 1) Sys.max_array_length in if nsize <> osize then begin - let ndata = Array.create nsize Empty in + let ndata = Array.make nsize Empty in let rec insert_bucket = function Empty -> () | Cons(key, data, rest) -> diff --git a/src/ocamlutil/longarray.ml b/src/ocamlutil/longarray.ml index ed9f533b1..0cdef6154 100644 --- a/src/ocamlutil/longarray.ml +++ b/src/ocamlutil/longarray.ml @@ -24,7 +24,7 @@ let split_idx (idx: int) : int option = let rec create (len: int) (init: 'a) : 'a t = let len1, len2 = split_len len in - (Array.create len1 init) :: (if len2 > 0 then create len2 init else []) + (Array.make len1 init) :: (if len2 > 0 then create len2 init else []) let rec init (len: int) (fn: int -> 'a) : 'a t = let len1, len2 = split_len len in diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml index 41180974f..ce889d356 100644 --- a/src/ocamlutil/pretty.ml +++ b/src/ocamlutil/pretty.ml @@ -726,7 +726,7 @@ let gprintf (finish : doc -> 'b) ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) let format_spec = "% " in - String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc (Int64.format format_spec n)) @@ -736,7 +736,7 @@ let gprintf (finish : doc -> 'b) ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) let format_spec = "% " in - String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc (Int32.format format_spec n)) @@ -746,7 +746,7 @@ let gprintf (finish : doc -> 'b) ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) let format_spec = "% " in - String.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) + Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc (Nativeint.format format_spec n)) From 3220ccb3d744bc33df9f81cd84d1334bd88c1fae Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 11:55:49 +0100 Subject: [PATCH 2/8] Change improper usage of String.copy (deprecated; Strings are immutable) to use Bytes instead --- src/cil.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cil.ml b/src/cil.ml index bd3920744..64e60bb0b 100755 --- a/src/cil.ml +++ b/src/cil.ml @@ -5080,10 +5080,10 @@ let loadBinaryFile (filename : string) : file = (* Take the name of a file and make a valid symbol name out of it. There are * a few characters that are not valid in symbols *) let makeValidSymbolName (s: string) = - let s = String.copy s in (* So that we can update in place *) - let l = String.length s in + let s = Bytes.of_string s in (* strings are immutable; convert to mutable Bytes *) + let l = Bytes.length s in for i = 0 to l - 1 do - let c = String.get s i in + let c = Bytes.get s i in let isinvalid = match c with '-' | '.' -> true @@ -5092,7 +5092,7 @@ let makeValidSymbolName (s: string) = if isinvalid then Bytes.set s i '_'; done; - s + Bytes.to_string s let rec addOffset (toadd: offset) (off: offset) : offset = match off with From a9db4135189f81329cf2c332249a3703c3ee7023 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 13:08:01 +0100 Subject: [PATCH 3/8] update one more secret use of String.set to Bytes --- src/formatlex.mll | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/formatlex.mll b/src/formatlex.mll index 584a060d5..93d7ee61e 100644 --- a/src/formatlex.mll +++ b/src/formatlex.mll @@ -145,11 +145,11 @@ let scan_oct_escape str = * We convert L"Hi" to "H\000i\000" *) let wbtowc wstr = let len = String.length wstr in - let dest = String.make (len * 2) '\000' in + let dest = Bytes.make (len * 2) '\000' in for i = 0 to len-1 do dest.[i*2] <- wstr.[i] ; done ; - dest + Bytes.to_string dest (* This function converst the "Hi" in L"Hi" to { L'H', L'i', L'\0' } *) let wstr_to_warray wstr = From 2bfc2db81863486a74a65cdb24e03019ebb02832 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 16:27:56 +0100 Subject: [PATCH 4/8] update treatment of Strings to Bytes in errormsg module; should have same behavior with previous versions of OCaml, while fixing compilation failure on 4.06 --- src/ocamlutil/errormsg.ml | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/ocamlutil/errormsg.ml b/src/ocamlutil/errormsg.ml index 857d62b5c..6b6ef06d6 100644 --- a/src/ocamlutil/errormsg.ml +++ b/src/ocamlutil/errormsg.ml @@ -205,28 +205,29 @@ let setHFile (f: string) : unit = let rem_quotes str = String.sub str 1 ((String.length str) - 2) +(* Change \ into / in file names. To avoid complications with escapes *) (* Change \ into / in file names. To avoid complications with escapes *) let cleanFileName str = let str1 = if str <> "" && String.get str 0 = '"' (* '"' ( *) - then rem_quotes str else str in - let l = String.length str1 in + then Bytes.of_string (rem_quotes str) else Bytes.of_string str in + let l = Bytes.length str1 in let rec loop (copyto: int) (i: int) = if i >= l then - String.sub str1 0 copyto + Bytes.sub str1 0 copyto else - let c = String.get str1 i in + let c = Bytes.get str1 i in if c <> '\\' then begin Bytes.set str1 copyto c; loop (copyto + 1) (i + 1) end else begin Bytes.set str1 copyto '/'; - if i < l - 2 && String.get str1 (i + 1) = '\\' then + if i < l - 2 && Bytes.get str1 (i + 1) = '\\' then loop (copyto + 1) (i + 2) else loop (copyto + 1) (i + 1) end in - loop 0 0 + Bytes.to_string (loop 0 0) let readingFromStdin = ref false From 20b04da92583cd5526054c2f0a26b76ea1776c45 Mon Sep 17 00:00:00 2001 From: Claire Date: Thu, 1 Feb 2018 16:34:24 +0100 Subject: [PATCH 5/8] update treatment of Strings to Bytes in Pretty; should have same behavior with previous versions of OCaml, while fixing compilation failure on 4.06 --- src/ocamlutil/pretty.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml index ce889d356..0076361d6 100644 --- a/src/ocamlutil/pretty.ml +++ b/src/ocamlutil/pretty.ml @@ -725,31 +725,31 @@ let gprintf (finish : doc -> 'b) invalid_arg ("dprintf: unimplemented format " ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) - let format_spec = "% " in + let format_spec = Bytes.of_string "% " in Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc - (Int64.format format_spec n)) + (Int64.format (Bytes.to_string format_spec) n)) (succ j')) | 'l' -> if j != i + 1 then invalid_arg ("dprintf: unimplemented format " ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) - let format_spec = "% " in + let format_spec = Bytes.of_string "% " in Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc - (Int32.format format_spec n)) + (Int32.format (Bytes.to_string format_spec) n)) (succ j')) | 'n' -> if j != i + 1 then invalid_arg ("dprintf: unimplemented format " ^ (String.sub format i (j-i+1))); let j' = succ j in (* eat the d,i,x etc. *) - let format_spec = "% " in + let format_spec = Bytes.of_string "% " in Bytes.set format_spec 1 (fget j'); (* format_spec = "%x", etc. *) Obj.magic(fun n -> collect (dctext1 acc - (Nativeint.format format_spec n)) + (Nativeint.format (Bytes.to_string format_spec) n)) (succ j')) | 'f' | 'e' | 'E' | 'g' | 'G' -> Obj.magic(fun f -> From e8c62645e19b71f01ed94172a0c670f55e50c514 Mon Sep 17 00:00:00 2001 From: Claire Le Goues Date: Tue, 31 Aug 2021 11:41:02 -0400 Subject: [PATCH 6/8] replace golf with whatever Wes did in 2013 genprog --- src/ext/pta/golf.ml | 51 ++++++++++++++++++++++++++++++++++++--------- 1 file changed, 41 insertions(+), 10 deletions(-) diff --git a/src/ext/pta/golf.ml b/src/ext/pta/golf.ml index 69c94abe4..73806df0a 100644 --- a/src/ext/pta/golf.ml +++ b/src/ext/pta/golf.ml @@ -1,6 +1,10 @@ +(* Tue Apr 23 10:16:43 EDT 2013 WRW -- this is a copy of 'golf.ml' from + * CIL 1.6.0 copied locally and adapted to work with Genprog (e.g., for + * handling the strong update problem when computing dataflow analyses). *) + (* * - * Copyright (c) 2001-2002, + * Copyright (c) 2001-2017, * John Kodumal * All rights reserved. * @@ -332,6 +336,33 @@ let join_cache : (int * int, tau) H.t = H.create 64 (* Utility Functions *) (* *) (***********************************************************************) +let list_array_map f l = + Array.to_list (Array.map f (Array.of_list l)) + +let rec count_map f l ctr = + match l with + | [] -> [] + | [x] -> [f x] + | [x;y] -> + (* order matters! *) + let x' = f x in + let y' = f y in + [x'; y'] + | [x;y;z] -> + let x' = f x in + let y' = f y in + let z' = f z in + [x'; y'; z'] + | x :: y :: z :: w :: tl -> + let x' = f x in + let y' = f y in + let z' = f z in + let w' = f w in + x' :: y' :: z' :: w' :: + (if ctr > 500 then list_array_map f tl + else count_map f tl (ctr + 1)) + +let list_map f l = count_map f l 0 let find = U.deref @@ -595,7 +626,7 @@ let rec print_tau_list (l : tau list) : unit = print_t_strings t | [] -> () in - print_t_strings (Util.list_map string_of_tau l) + print_t_strings (list_map string_of_tau l) let print_constraint (c : tconstraint) = match c with @@ -716,7 +747,7 @@ let copy_toplevel (t : tau) : tau = | Fun f -> let fresh_fn = fun _ -> fresh_var_i false in make_fun (fresh_label false, - Util.list_map fresh_fn f.args, fresh_var_i false) + list_map fresh_fn f.args, fresh_var_i false) | _ -> die "copy_toplevel" @@ -1151,7 +1182,7 @@ let apply (t : tau) (al : tau list) : (tau * int) = | Var v -> let new_l, new_ret, new_args = fresh_label false, fresh_var false, - Util.list_map (function _ -> fresh_var false) !actuals + list_map (function _ -> fresh_var false) !actuals in let new_fun = make_fun (new_l, new_args, new_ret) in add_toplev_constraint (Unification (new_fun, f)); @@ -1169,7 +1200,7 @@ let apply (t : tau) (al : tau list) : (tau * int) = [formals], and return value [ret]. Adds no constraints. *) let make_function (name : string) (formals : lvalue list) (ret : tau) : tau = let f = make_fun (make_label false name None, - Util.list_map (fun x -> rvalue x) formals, + list_map (fun x -> rvalue x) formals, ret) in make_pair (fresh_var false, f) @@ -1403,7 +1434,7 @@ let points_to_aux (t : tau) : constant list = with NoContents -> [] let points_to_names (lv : lvalue) : string list = - Util.list_map (fun (_, str, _) -> str) (points_to_aux lv.contents) + list_map (fun (_, str, _) -> str) (points_to_aux lv.contents) let points_to (lv : lvalue) : Cil.varinfo list = let rec get_vinfos l : Cil.varinfo list = match l with @@ -1537,9 +1568,9 @@ let may_alias (t1 : tau) (t2 : tau) : bool = let alias_query (b : bool) (lvl : lvalue list) : int * int = let naive_count = ref 0 in let smart_count = ref 0 in - let lbls = Util.list_map extract_ptlabel lvl in (* label option list *) + let lbls = list_map extract_ptlabel lvl in (* label option list *) let ptsets = - Util.list_map + list_map (function Some l -> collect_ptsets l | None -> C.empty) @@ -1576,9 +1607,9 @@ let alias_frequency (lvl : (lvalue * bool) list) : int * int = let extract_lbl (lv, b : lvalue * bool) = (lv.l, b) in let naive_count = ref 0 in let smart_count = ref 0 in - let lbls = Util.list_map extract_lbl lvl in + let lbls = list_map extract_lbl lvl in let ptsets = - Util.list_map + list_map (fun (lbl, b) -> if b then (find lbl).loc (* symbol access *) else collect_ptsets lbl) From c671bd6edadc21b7c5fa405e1014f17d24316602 Mon Sep 17 00:00:00 2001 From: Claire Le Goues Date: Tue, 31 Aug 2021 11:44:33 -0400 Subject: [PATCH 7/8] moves Wes's changes to ptranal for genprog to main cil src --- src/ext/pta/ptranal.ml | 38 +++++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 15 deletions(-) diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml index e3a3be266..df2817b64 100644 --- a/src/ext/pta/ptranal.ml +++ b/src/ext/pta/ptranal.ml @@ -1,6 +1,10 @@ +(* Tue Apr 23 10:16:43 EDT 2013 WRW -- this is a copy of 'ptranal.ml' from + * CIL 1.6.0 copied locally and adapted to work with Genprog (e.g., for + * handling the strong update problem when computing dataflow analyses). *) + (* * - * Copyright (c) 2001-2002, + * Copyright (c) 2001-2017, * John Kodumal * All rights reserved. * @@ -38,11 +42,10 @@ exception Bad_function open Cil -open Feature module H = Hashtbl -module A = Olf +module A = Golf exception UnknownLocation = A.UnknownLocation type access = A.lvalue * bool @@ -245,13 +248,17 @@ and analyze_expr (e : exp ) : A.tau = | AlignOf _ -> A.bottom () | UnOp (op, e, t) -> analyze_expr e | BinOp (op, e, e', t) -> A.join (analyze_expr e) (analyze_expr e') + (* | Question (_, e, e', _) -> A.join (analyze_expr e) (analyze_expr e') + *) | CastE (t, e) -> analyze_expr e | AddrOf l -> if !fun_ptrs_as_funs && isFunctionType (typeOfLval l) then A.rvalue (analyze_lval l) else A.address (analyze_lval l) + (* | AddrOfLabel _ -> failwith "not implemented yet" (* XXX *) + *) | StartOf l -> A.address (analyze_lval l) | AlignOfE _ -> A.bottom () | SizeOfE _ -> A.bottom () @@ -265,7 +272,7 @@ let rec analyze_init (i : init ) : A.tau = match i with SingleInit e -> analyze_expr e | CompoundInit (t, oi) -> - A.join_inits (Util.list_map (function (_, i) -> analyze_init i) oi) + A.join_inits (Golf.list_map (function (_, i) -> analyze_init i) oi) let analyze_instr (i : instr ) : unit = match i with @@ -285,10 +292,10 @@ let analyze_instr (i : instr ) : unit = List.iter (fun e -> ignore (analyze_expr e)) actuals else (* todo : check to see if the thing is an undefined function *) let fnres, site = - if is_undefined_fun fexpr && !conservative_undefineds then - A.apply_undefined (Util.list_map analyze_expr actuals) + if is_undefined_fun fexpr & !conservative_undefineds then + A.apply_undefined (Golf.list_map analyze_expr actuals) else - A.apply (analyze_expr fexpr) (Util.list_map analyze_expr actuals) + A.apply (analyze_expr fexpr) (Golf.list_map analyze_expr actuals) in begin match res with @@ -316,7 +323,9 @@ let rec analyze_stmt (s : stmt ) : unit = | None -> () end | Goto (s', l) -> () (* analyze_stmt(!s') *) + (* | ComputedGoto (e, l) -> () + *) | If (e, b, b', l) -> (* ignore the expression e; expressions can't be side-effecting *) analyze_block b; @@ -343,7 +352,7 @@ and analyze_block (b : block ) : unit = let analyze_function (f : fundec ) : unit = let oldlv = analyze_var_decl f.svar in let ret = A.make_fresh (f.svar.vname ^ "_ret") in - let formals = Util.list_map analyze_var_decl f.sformals in + let formals = Golf.list_map analyze_var_decl f.sformals in let newf = A.make_function f.svar.vname formals ret in if !show_progress then Printf.printf "Analyzing function %s\n" f.svar.vname; @@ -433,7 +442,7 @@ let compute_may_aliases (b : bool) : unit = match exps with [] -> () | h :: t -> - ignore (Util.list_map (may_alias h) t); + ignore (Golf.list_map (may_alias h) t); compute_may_aliases_aux t and exprs : exp list ref = ref [] in H.iter (fun e -> fun _ -> exprs := e :: !exprs) expressions; @@ -545,7 +554,7 @@ let absloc_lval_aliases lv = let absloc_e_transitive_points_to (e : Cil.exp) : absloc list = let rec lv_trans_ptsto (worklist : varinfo list) (acc : varinfo list) : absloc list = match worklist with - [] -> Util.list_map absloc_of_varinfo acc + [] -> Golf.list_map absloc_of_varinfo acc | vi :: wklst'' -> if List.mem vi acc then lv_trans_ptsto wklst'' acc else @@ -562,15 +571,16 @@ let absloc_eq a b = A.absloc_eq (a, b) let d_absloc: unit -> absloc -> Pretty.doc = A.d_absloc +let ptrAnalysis = ref false let ptrResults = ref false let ptrTypes = ref false (** Turn this into a CIL feature *) -let feature = { - fd_name = "ptranal"; - fd_enabled = false; +let feature = { + Feature.fd_name = "ptranal"; + Feature.fd_enabled = !ptrAnalysis; fd_description = "alias analysis"; fd_extraopt = [ ("--ptr_may_aliases", @@ -596,5 +606,3 @@ let feature = { if !ptrTypes then print_types ()); fd_post_check = false (* No changes *) } - -let () = Feature.register feature From 037c0fd51f1b9846bbb545e1e367fb53ddb861aa Mon Sep 17 00:00:00 2001 From: Claire Le Goues Date: Tue, 31 Aug 2021 12:47:11 -0400 Subject: [PATCH 8/8] undoes some of Wes's changes to golf --- src/ext/pta/golf.ml | 45 +++++++++--------------------------------- src/ext/pta/ptranal.ml | 19 ++++++++++-------- 2 files changed, 20 insertions(+), 44 deletions(-) diff --git a/src/ext/pta/golf.ml b/src/ext/pta/golf.ml index 73806df0a..233ee7ce4 100644 --- a/src/ext/pta/golf.ml +++ b/src/ext/pta/golf.ml @@ -336,33 +336,6 @@ let join_cache : (int * int, tau) H.t = H.create 64 (* Utility Functions *) (* *) (***********************************************************************) -let list_array_map f l = - Array.to_list (Array.map f (Array.of_list l)) - -let rec count_map f l ctr = - match l with - | [] -> [] - | [x] -> [f x] - | [x;y] -> - (* order matters! *) - let x' = f x in - let y' = f y in - [x'; y'] - | [x;y;z] -> - let x' = f x in - let y' = f y in - let z' = f z in - [x'; y'; z'] - | x :: y :: z :: w :: tl -> - let x' = f x in - let y' = f y in - let z' = f z in - let w' = f w in - x' :: y' :: z' :: w' :: - (if ctr > 500 then list_array_map f tl - else count_map f tl (ctr + 1)) - -let list_map f l = count_map f l 0 let find = U.deref @@ -626,7 +599,7 @@ let rec print_tau_list (l : tau list) : unit = print_t_strings t | [] -> () in - print_t_strings (list_map string_of_tau l) + print_t_strings (Util.list_map string_of_tau l) let print_constraint (c : tconstraint) = match c with @@ -747,7 +720,7 @@ let copy_toplevel (t : tau) : tau = | Fun f -> let fresh_fn = fun _ -> fresh_var_i false in make_fun (fresh_label false, - list_map fresh_fn f.args, fresh_var_i false) + Util.list_map fresh_fn f.args, fresh_var_i false) | _ -> die "copy_toplevel" @@ -1182,7 +1155,7 @@ let apply (t : tau) (al : tau list) : (tau * int) = | Var v -> let new_l, new_ret, new_args = fresh_label false, fresh_var false, - list_map (function _ -> fresh_var false) !actuals + Util.list_map (function _ -> fresh_var false) !actuals in let new_fun = make_fun (new_l, new_args, new_ret) in add_toplev_constraint (Unification (new_fun, f)); @@ -1200,7 +1173,7 @@ let apply (t : tau) (al : tau list) : (tau * int) = [formals], and return value [ret]. Adds no constraints. *) let make_function (name : string) (formals : lvalue list) (ret : tau) : tau = let f = make_fun (make_label false name None, - list_map (fun x -> rvalue x) formals, + Util.list_map (fun x -> rvalue x) formals, ret) in make_pair (fresh_var false, f) @@ -1434,7 +1407,7 @@ let points_to_aux (t : tau) : constant list = with NoContents -> [] let points_to_names (lv : lvalue) : string list = - list_map (fun (_, str, _) -> str) (points_to_aux lv.contents) + Util.list_map (fun (_, str, _) -> str) (points_to_aux lv.contents) let points_to (lv : lvalue) : Cil.varinfo list = let rec get_vinfos l : Cil.varinfo list = match l with @@ -1568,9 +1541,9 @@ let may_alias (t1 : tau) (t2 : tau) : bool = let alias_query (b : bool) (lvl : lvalue list) : int * int = let naive_count = ref 0 in let smart_count = ref 0 in - let lbls = list_map extract_ptlabel lvl in (* label option list *) + let lbls = Util.list_map extract_ptlabel lvl in (* label option list *) let ptsets = - list_map + Util.list_map (function Some l -> collect_ptsets l | None -> C.empty) @@ -1607,9 +1580,9 @@ let alias_frequency (lvl : (lvalue * bool) list) : int * int = let extract_lbl (lv, b : lvalue * bool) = (lv.l, b) in let naive_count = ref 0 in let smart_count = ref 0 in - let lbls = list_map extract_lbl lvl in + let lbls = Util.list_map extract_lbl lvl in let ptsets = - list_map + Util.list_map (fun (lbl, b) -> if b then (find lbl).loc (* symbol access *) else collect_ptsets lbl) diff --git a/src/ext/pta/ptranal.ml b/src/ext/pta/ptranal.ml index df2817b64..a11c36779 100644 --- a/src/ext/pta/ptranal.ml +++ b/src/ext/pta/ptranal.ml @@ -42,6 +42,7 @@ exception Bad_function open Cil +open Feature module H = Hashtbl @@ -272,7 +273,7 @@ let rec analyze_init (i : init ) : A.tau = match i with SingleInit e -> analyze_expr e | CompoundInit (t, oi) -> - A.join_inits (Golf.list_map (function (_, i) -> analyze_init i) oi) + A.join_inits (Util.list_map (function (_, i) -> analyze_init i) oi) let analyze_instr (i : instr ) : unit = match i with @@ -293,9 +294,9 @@ let analyze_instr (i : instr ) : unit = else (* todo : check to see if the thing is an undefined function *) let fnres, site = if is_undefined_fun fexpr & !conservative_undefineds then - A.apply_undefined (Golf.list_map analyze_expr actuals) + A.apply_undefined (Util.list_map analyze_expr actuals) else - A.apply (analyze_expr fexpr) (Golf.list_map analyze_expr actuals) + A.apply (analyze_expr fexpr) (Util.list_map analyze_expr actuals) in begin match res with @@ -352,7 +353,7 @@ and analyze_block (b : block ) : unit = let analyze_function (f : fundec ) : unit = let oldlv = analyze_var_decl f.svar in let ret = A.make_fresh (f.svar.vname ^ "_ret") in - let formals = Golf.list_map analyze_var_decl f.sformals in + let formals = Util.list_map analyze_var_decl f.sformals in let newf = A.make_function f.svar.vname formals ret in if !show_progress then Printf.printf "Analyzing function %s\n" f.svar.vname; @@ -442,7 +443,7 @@ let compute_may_aliases (b : bool) : unit = match exps with [] -> () | h :: t -> - ignore (Golf.list_map (may_alias h) t); + ignore (Util.list_map (may_alias h) t); compute_may_aliases_aux t and exprs : exp list ref = ref [] in H.iter (fun e -> fun _ -> exprs := e :: !exprs) expressions; @@ -554,7 +555,7 @@ let absloc_lval_aliases lv = let absloc_e_transitive_points_to (e : Cil.exp) : absloc list = let rec lv_trans_ptsto (worklist : varinfo list) (acc : varinfo list) : absloc list = match worklist with - [] -> Golf.list_map absloc_of_varinfo acc + [] -> Util.list_map absloc_of_varinfo acc | vi :: wklst'' -> if List.mem vi acc then lv_trans_ptsto wklst'' acc else @@ -579,8 +580,8 @@ let ptrTypes = ref false (** Turn this into a CIL feature *) let feature = { - Feature.fd_name = "ptranal"; - Feature.fd_enabled = !ptrAnalysis; + fd_name = "ptranal"; + fd_enabled = !ptrAnalysis; fd_description = "alias analysis"; fd_extraopt = [ ("--ptr_may_aliases", @@ -606,3 +607,5 @@ let feature = { if !ptrTypes then print_types ()); fd_post_check = false (* No changes *) } + +let () = Feature.register feature