Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 0 additions & 6 deletions src/check.ml
Original file line number Diff line number Diff line change
Expand Up @@ -51,12 +51,6 @@ type checkFlags =
let checkGlobalIds = ref true
let ignoreInstr = ref (fun i -> false)

(* Attributes must be sorted *)
type ctxAttr =
CALocal (* Attribute of a local variable *)
| CAGlobal (* Attribute of a global variable *)
| CAType (* Attribute of a type *)

let valid = ref true

let warn fmt =
Expand Down
9 changes: 0 additions & 9 deletions src/cil.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1969,11 +1969,6 @@ let rec typeOf (e: exp) : typ =
| _ -> E.s (E.bug "typeOf: StartOf on a non-array")
end

and typeOfInit (i: init) : typ =
match i with
SingleInit e -> typeOf e
| CompoundInit (t, _) -> t

and typeOfLval = function
Var vi, off -> typeOffset vi.vtype off
| Mem addr, off -> begin
Expand Down Expand Up @@ -6839,10 +6834,6 @@ let getVarsInGlobal (g : global) : varinfo list =
ignore (visitCilGlobal v g);
!pacc

let hasPrefix p s =
let pl = String.length p in
(String.length s >= pl) && String.sub s 0 pl = p

let pushGlobal (g: global)
~(types:global list ref)
~(variables: global list ref) =
Expand Down
2 changes: 0 additions & 2 deletions src/cilint.ml
Original file line number Diff line number Diff line change
Expand Up @@ -43,8 +43,6 @@ let mod_cilint = mod_big_int
let compare_cilint = compare_big_int
let is_zero_cilint (c:cilint) : bool = sign_big_int c = 0

let negative_cilint (c:cilint) : bool = sign_big_int c < 0

let cilint_of_int = big_int_of_int
let int_of_cilint = int_of_big_int

Expand Down
2 changes: 1 addition & 1 deletion src/dune
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,6 @@

(env
(dev
(flags (:standard -warn-error -A -w -27-32-34-37-38)) ; https://dune.readthedocs.io/en/stable/faq.html#how-to-make-warnings-non-fatal
(flags (:standard -warn-error -A -w -unused-var-strict)) ; https://dune.readthedocs.io/en/stable/faq.html#how-to-make-warnings-non-fatal
)
)
46 changes: 0 additions & 46 deletions src/ext/pta/golf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -366,13 +366,6 @@ let get_stamp (t : tau) : int =
| Pair p -> p.p_stamp
| Fun f -> f.f_stamp

(** Negate a polarity. *)
let negate (p : polarity) : polarity =
match p with
Pos -> Neg
| Neg -> Pos
| Sub -> die "negate"

(** Consistency checks for inferred types *)
let pair_or_var (t : tau) =
match find t with
Expand Down Expand Up @@ -585,18 +578,6 @@ let print_path (p : lblinfo path) : unit =
(string_of_label p.tail)
(PathHash.hash p)

(** Print a list of tau elements, comma separated *)
let print_tau_list (l : tau list) : unit =
let rec print_t_strings = function
h :: [] -> print_endline h
| h :: t ->
print_string h;
print_string ", ";
print_t_strings t
| [] -> ()
in
print_t_strings (Util.list_map string_of_tau l)

let print_constraint (c : tconstraint) =
match c with
Unification (t, t') ->
Expand Down Expand Up @@ -720,28 +701,6 @@ let copy_toplevel (t : tau) : tau =
| _ -> die "copy_toplevel"


let has_same_structure (t : tau) (t' : tau) =
match find t, find t' with
Pair _, Pair _ -> true
| Ref _, Ref _ -> true
| Fun _, Fun _ -> true
| Var _, Var _ -> true
| _ -> false


let pad_args (f, f' : finfo * finfo) : unit =
let padding = ref ((List.length f.args) - (List.length f'.args))
in
if !padding == 0 then ()
else
let to_pad =
if !padding > 0 then f' else (padding := -(!padding); f)
in
for _ = 1 to !padding do
to_pad.args <- to_pad.args @ [fresh_var false]
done


let pad_args2 (fi, tlr : finfo * tau list ref) : unit =
let padding = ref (List.length fi.args - List.length !tlr)
in
Expand Down Expand Up @@ -1129,11 +1088,6 @@ let proj_fun (t : tau) : tau =
f
| _ -> raise WellFormed

let get_args (t : tau) : tau list =
match U.deref t with
Fun f -> f.args
| _ -> raise WellFormed

let get_finfo (t : tau) : finfo =
match U.deref t with
Fun f -> f
Expand Down
77 changes: 0 additions & 77 deletions src/ext/pta/olf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -42,14 +42,10 @@
exception Inconsistent (* raised if constraint system is inconsistent *)
exception WellFormed (* raised if types are not well-formed *)
exception NoContents
exception APFound (* raised if an alias pair is found, a control
flow exception *)
exception ReachedTop (* raised if top (from an undefined function)
flows to a c_absloc during the flow step *)
exception UnknownLocation

let solve_constraints () = () (* only for compatability with Golf *)

open Cil

module U = Uref
Expand Down Expand Up @@ -205,9 +201,6 @@ let debug = ref false
(** Just debug all the constraints (including induced) *)
let debug_constraints = ref false

(** Debug the flow step *)
let debug_flow_step = ref false

(** Compatibility with GOLF *)
let debug_aliases = ref false
let smart_aliases = ref false
Expand All @@ -223,9 +216,6 @@ let eq_worklist : tconstraint Q.t = Q.create ()
(** A list of leq constraints. *)
let leq_worklist : tconstraint Q.t = Q.create ()

(** A hashtable containing stamp pairs of c_abslocs that must be aliased. *)
let cached_aliases : (int * int, unit) H.t = H.create 64

(** A hashtable mapping pairs of tau's to their join node. *)
let join_cache : (int * int, tau) H.t = H.create 64

Expand Down Expand Up @@ -265,14 +255,6 @@ let finished_constraints () =

let find = U.deref

(** return the prefix of the list up to and including the first
element satisfying p. if no element satisfies p, return the empty
list *)
let rec keep_until p l =
match l with
[] -> []
| x :: xs -> if p x then [x] else x :: keep_until p xs


(** Generate a unique integer. *)
let fresh_index : (unit -> int) =
Expand Down Expand Up @@ -477,18 +459,6 @@ let string_of_lvalue (lv : lvalue) : string =
(* do a consistency check *)
Printf.sprintf "[%s]^(%s)" contents l

(** Print a list of tau elements, comma separated *)
let print_tau_list (l : tau list) : unit =
let rec print_t_strings = function
[] -> ()
| h :: [] -> print_endline h
| h :: t ->
print_string h;
print_string ", ";
print_t_strings t
in
print_t_strings (Util.list_map string_of_tau l)

let print_constraint (c : tconstraint) =
match c with
Unification (t, t') ->
Expand Down Expand Up @@ -587,14 +557,6 @@ let copy_toplevel (t : tau) : tau =
fresh_var_i false)
| _ -> die "copy_toplevel"

let has_same_structure (t : tau) (t' : tau) =
match find t, find t' with
Pair _, Pair _ -> true
| Ref _, Ref _ -> true
| Fun _, Fun _ -> true
| Var _, Var _ -> true
| _ -> false

let pad_args (fi, tlr : finfo * tau list ref) : unit =
let padding = List.length fi.args - List.length !tlr
in
Expand Down Expand Up @@ -892,11 +854,6 @@ let proj_fun (t : tau) : tau =
f
| _ -> raise WellFormed

let get_args (t : tau) : tau list =
match find t with
Fun f -> f.args
| _ -> raise WellFormed

let get_finfo (t : tau) : finfo =
match find t with
Fun f -> f
Expand Down Expand Up @@ -987,40 +944,6 @@ module IntHash = Hashtbl.Make (struct
let hash x = x
end)

(** todo : reached_top !! *)
let collect_ptset_fast (l : c_absloc) : abslocset =
let onpath : unit IntHash.t = IntHash.create 101 in
let path : c_absloc list ref = ref [] in
let compute_path (i : int) =
keep_until (fun l -> i = get_c_absloc_stamp l) !path in
let collapse_cycle (cycle : c_absloc list) =
match cycle with
l :: ls ->
List.iter (fun l' -> unify_c_abslocs (l, l')) ls;
C.empty
| [] -> die "collapse cycle" in
let rec flow_step (l : c_absloc) : abslocset =
let stamp = get_c_absloc_stamp l in
if IntHash.mem onpath stamp then (* already seen *)
collapse_cycle (compute_path stamp)
else
let li = find l in
IntHash.add onpath stamp ();
path := l :: !path;
B.iter
(fun lb -> li.aliases <- C.union li.aliases (flow_step lb.info))
li.lbounds;
path := List.tl !path;
IntHash.remove onpath stamp;
li.aliases
in
insist (can_query_graph ()) "collect_ptset_fast can't query graph";
if get_flow_computed l then get_aliases l
else
begin
set_flow_computed l;
flow_step l
end

(** this is a quadratic flow step. keep it for debugging the fast
version above. *)
Expand Down
13 changes: 1 addition & 12 deletions src/ext/pta/ptranal.ml
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,6 @@
*)

exception Bad_return
exception Bad_function


open Cil
Expand Down Expand Up @@ -375,14 +374,9 @@ let analyze_file (f : file) : unit =
(***********************************************************************)

(* Same as analyze_expr, but no constraints. *)
let rec traverse_expr (e : exp) : A.tau =
let traverse_expr (e : exp) : A.tau =
H.find expressions e

and traverse_expr_as_lval (e : exp) : A.lvalue =
match e with
| Lval l -> traverse_lval l
| _ -> assert false (* todo -- other kinds of expressions? *)

and traverse_lval (lv : lval ) : A.lvalue =
H.find lvalues lv

Expand Down Expand Up @@ -418,11 +412,6 @@ let resolve_funptr (e : exp) : fundec list =
[]
varinfos

let count_hash_elts h =
let result = ref 0 in
H.iter (fun _ -> fun _ -> incr result) lvalue_hash;
!result

let compute_may_aliases (b : bool) : unit =
let rec compute_may_aliases_aux (exps : exp list) =
match exps with
Expand Down
Loading