Skip to content
Merged
Show file tree
Hide file tree
Changes from 2 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: 6 additions & 0 deletions .semgrep/let.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
rules:
- id: let-unit-in
pattern: let () = $E in ...
message: use ; instead
languages: [ocaml]
severity: WARNING
4 changes: 2 additions & 2 deletions src/analyses/apron/apronAnalysis.apron.ml
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ let () =
Printexc.register_printer
(function
| Apron.Manager.Error e ->
let () = Apron.Manager.print_exclog Format.str_formatter e in
Some(Printf.sprintf "Apron.Manager.Error\n %s" (Format.flush_str_formatter ()))
Apron.Manager.print_exclog Format.str_formatter e;
Some (Printf.sprintf "Apron.Manager.Error\n %s" (Format.flush_str_formatter ()))
| _ -> None (* for other exceptions *)
)
4 changes: 2 additions & 2 deletions src/analyses/memOutOfBounds.ml
Original file line number Diff line number Diff line change
Expand Up @@ -269,7 +269,7 @@ struct
| None -> ID.bot_of @@ Cilfacade.ptrdiff_ikind ()
end in
let e_size = get_size_of_ptr_target man e in
let () = begin match e_size with
begin match e_size with
| `Top ->
(set_mem_safety_flag InvalidDeref;
M.warn "Size of lval dereference expression %a is top. Out-of-bounds memory access may occur" d_exp e)
Expand Down Expand Up @@ -297,7 +297,7 @@ struct
(set_mem_safety_flag InvalidDeref;
M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Could not compare size of lval dereference expression (%a) (in bytes) with offset by (%a) (in bytes). Memory out-of-bounds access might occur" ID.pretty casted_es ID.pretty casted_offs)
end
end in
end;
begin match e with
| Lval (Var v, _) as lval_exp -> check_no_binop_deref man lval_exp
| BinOp (binop, e1, e2, t) when binop = PlusPI || binop = MinusPI || binop = IndexPI ->
Expand Down
4 changes: 2 additions & 2 deletions src/solver/sLRterm.ml
Original file line number Diff line number Diff line change
Expand Up @@ -49,13 +49,13 @@ module SLR3term =
let count = ref 0 in
let count_side = ref (max_int - 1) in

let () = print_solver_stats := fun () ->
print_solver_stats := (fun () ->
Logs.info "wpoint: %d, rho: %d, rho': %d, q: %d, count: %d, count_side: %d" (HM.length wpoint) (HM.length rho) (HPM.length rho') (H.size !q) (Int.neg !count) (max_int - !count_side);
let histo = Hashtbl.create 13 in (* histogram: node id -> number of contexts *)
HM.iter (fun k _ -> Hashtbl.modify_def 1 (S.Var.var_id k) ((+)1) histo) rho;
let vid,n = Hashtbl.fold (fun k v (k',v') -> if v > v' then k,v else k',v') histo (Obj.magic (), 0) in
Logs.info "max #contexts: %d for var_id %s" n vid
in
);

let init ?(side=false) x =
if not (HM.mem rho x) then begin
Expand Down
4 changes: 2 additions & 2 deletions src/solver/td3.ml
Original file line number Diff line number Diff line change
Expand Up @@ -287,11 +287,11 @@ module Base =
include WPS (EqS) (HM) (VS)
end in

let () = print_solver_stats := fun () ->
print_solver_stats := (fun () ->
print_data data;
Logs.info "|called|=%d" (HM.length called);
print_context_stats rho
in
);

if GobConfig.get_bool "incremental.load" then (
print_data_verbose data "Loaded data for incremental analysis";
Expand Down
10 changes: 5 additions & 5 deletions src/solver/td_simplified.ml
Original file line number Diff line number Diff line change
Expand Up @@ -24,14 +24,14 @@ module Base : GenericEqSolver =
let wpoint = HM.create 10 in
let stable = HM.create 10 in

let () = print_solver_stats := fun () ->
print_solver_stats := (fun () ->
Logs.debug "|rho|=%d" (HM.length rho);
Logs.debug "|stable|=%d" (HM.length stable);
Logs.debug "|infl|=%d" (HM.length infl);
Logs.debug "|wpoint|=%d" (HM.length wpoint);
Logs.info "|called|=%d" (HM.length called);
print_context_stats rho
in
);

let add_infl y x =
if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
Expand Down Expand Up @@ -122,7 +122,7 @@ module Base : GenericEqSolver =
if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
box old eqd)
in
if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
(* old != wpd *)
if tracing && not (S.Dom.is_bot old) then trace "update" "%a (wpx: %b): %a" S.Var.pretty_trace x (HM.mem wpoint x) S.Dom.pretty_diff (wpd, old);
update_var_event x old wpd;
Expand All @@ -132,7 +132,7 @@ module Base : GenericEqSolver =
(iterate[@tailcall]) x
) else (
(* old == wpd *)
if not (HM.mem stable x) then (
if not (HM.mem stable x) then (
(* value unchanged, but not stable, i.e. destabilized itself during rhs *)
if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
(iterate[@tailcall]) x
Expand Down Expand Up @@ -172,7 +172,7 @@ module Base : GenericEqSolver =
);
List.iter (fun x -> HM.replace called x ();
if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
iterate x;
iterate x;
HM.remove called x
) unstable_vs;
solver ();
Expand Down
18 changes: 9 additions & 9 deletions src/solver/td_simplified_ref.ml
Original file line number Diff line number Diff line change
Expand Up @@ -28,9 +28,9 @@ module Base : GenericEqSolver =
let solve st vs =
let (data : var_data ref HM.t) = HM.create 10 in

let () = print_solver_stats := fun () ->
print_solver_stats := (fun () ->
Logs.debug "|data|=%d" (HM.length data);
in
);

let add_infl y x =
if tracing then trace "infl" "add_infl %a %a" S.Var.pretty_trace y S.Var.pretty_trace x;
Expand All @@ -46,12 +46,12 @@ module Base : GenericEqSolver =
begin
new_var_event x;
if tracing then trace "init" "init %a" S.Var.pretty_trace x;
let data_x = ref {
let data_x = ref {
infl = VS.empty;
value = S.Dom.bot ();
wpoint = false;
stable = false;
called = false
called = false
} in
HM.replace data x data_x;
data_x
Expand Down Expand Up @@ -138,7 +138,7 @@ module Base : GenericEqSolver =
if M.tracing then M.trace "wpoint" "widen %a" S.Var.pretty_trace x;
box old eqd)
in
if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
if not (Timing.wrap "S.Dom.equal" (fun () -> S.Dom.equal old wpd) ()) then (
(* old != wpd *)
if tracing && not (S.Dom.is_bot old) && !x_ref.wpoint then trace "solchange" "%a (wpx: %b): %a" S.Var.pretty_trace x (!x_ref.wpoint) S.Dom.pretty_diff (wpd, old);
update_var_event x old wpd;
Expand All @@ -148,7 +148,7 @@ module Base : GenericEqSolver =
(iterate[@tailcall]) x
) else (
(* old == wpd *)
if not (!x_ref.stable) then (
if not (!x_ref.stable) then (
(* value unchanged, but not stable, i.e. destabilized itself during rhs *)
if tracing then trace "iter" "iterate still unstable %a" S.Var.pretty_trace x;
(iterate[@tailcall]) x
Expand Down Expand Up @@ -185,12 +185,12 @@ module Base : GenericEqSolver =
Logs.newline ();
flush_all ();
);
List.iter (fun x ->
List.iter (fun x ->
let x_ref = HM.find data x in
x_ref := { !x_ref with called = true };
if tracing then trace "multivar" "solving for %a" S.Var.pretty_trace x;
iterate x;
x_ref := { !x_ref with called = false }
iterate x;
x_ref := { !x_ref with called = false }
) unstable_vs;
solver ();
)
Expand Down
Loading