Skip to content

Migrate from CIL's Pretty to OCaml's Format (initial pass) #1994

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
Copilot wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

Migrate from CIL's Pretty to OCaml's Format (initial pass) #1994

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
b8bf693
Initial plan
Copilot Apr 12, 2026
ed977a3
Add pp implementations to modules implementing Printable.S
Copilot Apr 12, 2026
635fa36
Migrate tracing system from Pretty to Format, add pp to domain files
Copilot Apr 12, 2026
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
4 changes: 2 additions & 2 deletions src/analyses/accessAnalysis.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ struct
emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated || List.mem (UseAfterFree.Spec.name ()) activated (* TODO: some of these don't have access as dependency *)

let do_access (man: (D.t, G.t, C.t, V.t) man) (kind:AccessKind.t) (reach:bool) (e:exp) =
if M.tracing then M.trace "access" "do_access %a %a %B" d_exp e AccessKind.pretty kind reach;
if M.tracing then M.trace "access" "do_access %a %a %B" CilType.Exp.pp e AccessKind.pp kind reach;
let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in
let ad = man.ask reach_or_mpt in
man.emit (Access {exp=e; ad; kind; reach})
Expand All @@ -42,7 +42,7 @@ struct
+ [deref=true], [reach=false] - Access [exp] by dereferencing once (may-point-to), used for lval writes and shallow special accesses.
+ [deref=true], [reach=true] - Access [exp] by dereferencing transitively (reachable), used for deep special accesses. *)
let access_one_top ?(force=false) ?(deref=false) man (kind: AccessKind.t) reach exp =
if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)" CilType.Exp.pretty exp AccessKind.pretty kind reach deref;
if M.tracing then M.traceli "access" "access_one_top %a (kind = %a, reach = %B, deref = %B)" CilType.Exp.pp exp AccessKind.pp kind reach deref;
if force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_man man) then (
if deref && Cil.isPointerType (Cilfacade.typeOf exp) then (* avoid dereferencing integers to unknown pointers, which cause many spurious type-based accesses *)
do_access man kind reach exp;
Expand Down
44 changes: 22 additions & 22 deletions src/analyses/apron/relationAnalysis.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -89,7 +89,7 @@ struct
let e' = visitCilExpr visitor e in
let rel = RD.add_vars st.rel (List.map RV.local (VH.to_seq_values v_ins |> List.of_seq)) in (* add temporary g#in-s *)
let rel' = VH.fold (fun v v_in rel ->
if M.tracing then M.trace "relation" "read_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_in;
if M.tracing then M.trace "relation" "read_global %a %a" CilType.Varinfo.pp v CilType.Varinfo.pp v_in;
read_global ask getg {st with rel} v v_in (* g#in = g; *)
) v_ins rel
in
Expand Down Expand Up @@ -124,7 +124,7 @@ struct

let assign_from_globals_wrapper ask getg st e f =
let (rel', e', v_ins) = read_globals_to_locals ask getg st e in
if M.tracing then M.trace "relation" "assign_from_globals_wrapper %a" d_exp e';
if M.tracing then M.trace "relation" "assign_from_globals_wrapper %a" CilType.Exp.pp e';
let rel' = f rel' e' in (* x = e; *)
let rel'' = RD.remove_vars rel' (List.map RV.local (VH.to_seq_values v_ins |> List.of_seq)) in (* remove temporary g#in-s *)
rel''
Expand Down Expand Up @@ -155,7 +155,7 @@ struct
v_out.vattr <- v.vattr; (*copy the attributes because the tracking may depend on them. Otherwise an assertion fails *)
let st = {st with rel = RD.add_vars st.rel [RV.local v_out]} in (* add temporary g#out *)
let st' = {st with rel = f st v_out} in (* g#out = e; *)
if M.tracing then M.trace "relation" "write_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_out;
if M.tracing then M.trace "relation" "write_global %a %a" CilType.Varinfo.pp v CilType.Varinfo.pp v_out;
let st' = write_global ask getg sideg st' v v_out in (* g = g#out; *)
let rel'' = RD.remove_vars st'.rel [RV.local v_out] in (* remove temporary g#out *)
{st' with rel = rel''}
Expand Down Expand Up @@ -192,7 +192,7 @@ struct

let no_overflow man exp = lazy (
let res = no_overflow man exp in
if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res d_exp exp;
if M.tracing then M.tracel "no_ov" "no_ov %b exp: %a" res CilType.Exp.pp exp;
res
)

Expand Down Expand Up @@ -249,20 +249,20 @@ struct
let assign man (lv:lval) e =
let st = man.local in
let simplified_e = replace_deref_exps man.ask e in
if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" d_lval lv d_exp e d_exp simplified_e;
if M.tracing then M.traceli "relation" "assign %a = %a (simplified to %a)" CilType.Lval.pp lv CilType.Exp.pp e CilType.Exp.pp simplified_e;
let ask = Analyses.ask_of_man man in
let r = assign_to_global_wrapper ask man.global man.sideg st lv (fun st v ->
assign_from_globals_wrapper ask man.global st simplified_e (fun apr' e' ->
if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pretty v d_exp e' d_plainexp e';
if M.tracing then M.trace "relation" "st: %a" RD.pretty apr';
if M.tracing then M.traceli "relation" "assign inner %a = %a (%a)" CilType.Varinfo.pp v CilType.Exp.pp e' CilType.Exp.pp e';
if M.tracing then M.trace "relation" "st: %a" RD.pp apr';
let r = RD.assign_exp ask apr' (RV.local v) e' (no_overflow ask simplified_e) in
let r' = assert_type_bounds ask r v in
if M.tracing then M.traceu "relation" "-> %a" RD.pretty r';
if M.tracing then M.traceu "relation" "-> %a" RD.pp r';
r'
)
)
in
if M.tracing then M.traceu "relation" "-> %a" D.pretty r;
if M.tracing then M.traceu "relation" "-> %a" D.pp r;
r

let branch man e b =
Expand Down Expand Up @@ -331,7 +331,7 @@ struct
| Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *)
| _ -> false (* keep everything else (just added args, globals, global privs) *)
);
if M.tracing then M.tracel "combine" "relation enter newd: %a" RD.pretty new_rel;
if M.tracing then M.tracel "combine" "relation enter newd: %a" RD.pp new_rel;
new_rel

let enter man r f args =
Expand Down Expand Up @@ -386,11 +386,11 @@ struct
let st = man.local in
let reachable_from_args = reachable_from_args man args in
let fundec = Node.find_fundec man.node in
if M.tracing then M.tracel "combine-rel" "relation f: %a" CilType.Varinfo.pretty f.svar;
if M.tracing then M.tracel "combine-rel" "relation formals: %a" (d_list "," CilType.Varinfo.pretty) f.sformals;
if M.tracing then M.tracel "combine-rel" "relation args: %a" (d_list "," d_exp) args;
if M.tracing then M.tracel "combine-rel" "relation st: %a" D.pretty st;
if M.tracing then M.tracel "combine-rel" "relation fun_st: %a" D.pretty fun_st;
if M.tracing then M.tracel "combine-rel" "relation f: %a" CilType.Varinfo.pp f.svar;
if M.tracing then M.tracel "combine-rel" "relation formals: %a" (d_list "," CilType.Varinfo.pp) f.sformals;
if M.tracing then M.tracel "combine-rel" "relation args: %a" (d_list "," CilType.Exp.pp) args;
if M.tracing then M.tracel "combine-rel" "relation st: %a" D.pp st;
if M.tracing then M.tracel "combine-rel" "relation fun_st: %a" D.pp fun_st;
let new_fun_rel = RD.add_vars fun_st.rel (RD.vars st.rel) in
let arg_substitutes =
let filter_actuals (x,e) =
Expand All @@ -416,7 +416,7 @@ struct
in
let any_local_reachable = any_local_reachable fundec reachable_from_args in
let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pretty ())) arg_vars;
if M.tracing then M.tracel "combine-rel" "relation remove vars: %a" (docList (GobApron.Var.pp ())) arg_vars;
RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
let tainted = f_ask.f Queries.MayBeTainted in
let tainted_vars = TaintPartialContexts.conv_varset tainted in
Expand All @@ -430,7 +430,7 @@ struct
)
in
let unify_rel = RD.unify new_rel new_fun_rel in (* TODO: unify_with *)
if M.tracing then M.tracel "combine-rel" "relation unifying %a %a = %a" RD.pretty new_rel RD.pretty new_fun_rel RD.pretty unify_rel;
if M.tracing then M.tracel "combine-rel" "relation unifying %a %a = %a" RD.pp new_rel RD.pp new_fun_rel RD.pp unify_rel;
{fun_st with rel = unify_rel}

let combine_assign man r fe f args fc fun_st (f_ask : Queries.ask) =
Expand Down Expand Up @@ -640,10 +640,10 @@ struct
in
match q with
| EvalInt e ->
if M.tracing then M.traceli "evalint" "relation query %a (%a)" d_exp e d_plainexp e;
if M.tracing then M.trace "evalint" "relation st: %a" D.pretty man.local;
if M.tracing then M.traceli "evalint" "relation query %a (%a)" CilType.Exp.pp e CilType.Exp.pp e;
if M.tracing then M.trace "evalint" "relation st: %a" D.pp man.local;
let r = eval_int e (no_overflow (Analyses.ask_of_man man) e) in
if M.tracing then M.traceu "evalint" "relation query %a -> %a" d_exp e ID.pretty r;
if M.tracing then M.traceu "evalint" "relation query %a -> %a" CilType.Exp.pp e ID.pp r;
r
| Queries.IterSysVars (vq, vf) ->
let vf' x = vf (Obj.repr x) in
Expand Down Expand Up @@ -720,9 +720,9 @@ struct
in
match q with
| EvalInt e ->
if M.tracing then M.traceli "relation" "evalint query %a (%a), man %a" d_exp e d_plainexp e D.pretty man.local;
if M.tracing then M.traceli "relation" "evalint query %a (%a), man %a" CilType.Exp.pp e CilType.Exp.pp e D.pp man.local;
let r = eval_int e (no_overflow (dummyask) e) in
if M.tracing then M.trace "relation" "evalint response %a -> %a" d_exp e ValueDomainQueries.ID.pretty r;
if M.tracing then M.trace "relation" "evalint response %a -> %a" CilType.Exp.pp e ValueDomainQueries.ID.pp r;
r
|_ -> Queries.Result.top q
in
Expand Down
Loading