Merge branch 'master' into affineeq-refine

Author: DrMichaelPetter

.git-blame-ignore-revs

@@ -37,3 +37,6 @@ c3e2cc848479ae86de5542b6ab0e75a74e9cf8c9
 
 # Fix LibraryFunctions.invalidate_actions indentation
 5662024232f32fe74dd25c9317dee4436ecb212d
+
+# Rename ctx -> man
+0c155e68607fede6fab17704a9a7aee38df5408e

src/analyses/abortUnless.ml

@@ -13,61 +13,61 @@ struct
   module D = BoolDomain.MustBool
   module C = Printable.Unit
 
-  let context ctx _ _ = ()
+  let context man _ _ = ()
   let startcontext () = ()
 
   (* transfer functions *)
-  let assign ctx (lval:lval) (rval:exp) : D.t =
+  let assign man (lval:lval) (rval:exp) : D.t =
     false
 
-  let branch ctx (exp:exp) (tv:bool) : D.t =
-    ctx.local
+  let branch man (exp:exp) (tv:bool) : D.t =
+    man.local
 
-  let body ctx (f:fundec) : D.t =
-    ctx.local
+  let body man (f:fundec) : D.t =
+    man.local
 
-  let return ctx (exp:exp option) (f:fundec) : D.t =
-    if ctx.local then
+  let return man (exp:exp option) (f:fundec) : D.t =
+    if man.local then
       match f.sformals with
       | [arg] when isIntegralType arg.vtype ->
-        (match ctx.ask (EvalInt (Lval (Var arg, NoOffset))) with
+        (match man.ask (EvalInt (Lval (Var arg, NoOffset))) with
          | v when Queries.ID.is_bot v -> false
          | v ->
            match Queries.ID.to_bool v with
            | Some b -> b
            | None -> false)
       | _ ->
-        (* should not happen, ctx.local should always be false in this case *)
+        (* should not happen, man.local should always be false in this case *)
         false
     else
       false
 
-  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+  let enter man (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     let candidate = match f.sformals with
       | [arg] when isIntegralType arg.vtype -> true
       | _ -> false
     in
     [false, candidate]
 
-  let combine_env ctx lval fexp f args fc au f_ask =
+  let combine_env man lval fexp f args fc au f_ask =
     if au then (
       (* Assert before combine_assign, so if variables in `arg` are assigned to, asserting doesn't unsoundly yield bot *)
       (* See test 62/03 *)
       match args with
-      | [arg] -> ctx.emit (Events.Assert arg)
+      | [arg] -> man.emit (Events.Assert arg)
       | _ -> ()
     );
     false
 
-  let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
+  let combine_assign man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
     false
 
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     false
 
   let startstate v = false
-  let threadenter ctx ~multiple lval f args = [false]
-  let threadspawn ctx ~multiple lval f args fctx = false
+  let threadenter man ~multiple lval f args = [false]
+  let threadspawn man ~multiple lval f args fman = false
   let exitstate v = false
 end
 

src/analyses/accessAnalysis.ml

@@ -31,112 +31,112 @@ struct
     let activated = get_string_list "ana.activated" in
     emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
 
-  let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) =
+  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;
     let reach_or_mpt: _ Queries.t = if reach then ReachableFrom e else MayPointTo e in
-    let ad = ctx.ask reach_or_mpt in
-    ctx.emit (Access {exp=e; ad; kind; reach})
+    let ad = man.ask reach_or_mpt in
+    man.emit (Access {exp=e; ad; kind; reach})
 
   (** Three access levels:
       + [deref=false], [reach=false] - Access [exp] without dereferencing, used for all normal reads and all function call arguments.
       + [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) ctx (kind: AccessKind.t) reach exp =
+  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 force || !collect_local || !emit_single_threaded || ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx) then (
+    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 ctx kind reach exp;
+        do_access man kind reach exp;
       if M.tracing then M.tracei "access" "distribute_access_exp";
-      Access.distribute_access_exp (do_access ctx Read false) exp;
+      Access.distribute_access_exp (do_access man Read false) exp;
       if M.tracing then M.traceu "access" "distribute_access_exp";
     );
     if M.tracing then M.traceu "access" "access_one_top"
 
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
-  let threadenter ctx ~multiple lval f args = [()]
+  let threadenter man ~multiple lval f args = [()]
   let exitstate  v = ()
-  let context ctx fd d = ()
+  let context man fd d = ()
 
 
   (** Transfer functions: *)
 
-  let vdecl ctx v =
-    access_one_top ctx Read false (SizeOf v.vtype);
-    ctx.local
+  let vdecl man v =
+    access_one_top man Read false (SizeOf v.vtype);
+    man.local
 
-  let assign ctx lval rval : D.t =
+  let assign man lval rval : D.t =
     (* ignore global inits *)
-    if !AnalysisState.global_initialization then ctx.local else begin
-      access_one_top ~deref:true ctx Write false (AddrOf lval);
-      access_one_top ctx Read false rval;
-      ctx.local
+    if !AnalysisState.global_initialization then man.local else begin
+      access_one_top ~deref:true man Write false (AddrOf lval);
+      access_one_top man Read false rval;
+      man.local
     end
 
-  let branch ctx exp tv : D.t =
-    access_one_top ctx Read false exp;
-    ctx.local
+  let branch man exp tv : D.t =
+    access_one_top man Read false exp;
+    man.local
 
-  let return ctx exp fundec : D.t =
+  let return man exp fundec : D.t =
     begin match exp with
-      | Some exp -> access_one_top ctx Read false exp
+      | Some exp -> access_one_top man Read false exp
       | None -> ()
     end;
-    ctx.local
+    man.local
 
-  let body ctx f : D.t =
-    ctx.local
+  let body man f : D.t =
+    man.local
 
-  let special ctx lv f arglist : D.t =
+  let special man lv f arglist : D.t =
     let desc = LF.find f in
     match desc.special arglist with
     (* TODO: remove Lock/Unlock cases when all those libraryfunctions use librarydescs and don't read mutex contents *)
     | Lock _
     | Unlock _ ->
-      ctx.local
+      man.local
     | _ ->
       LibraryDesc.Accesses.iter desc.accs (fun {kind; deep = reach} exp ->
-          access_one_top ~deref:true ctx kind reach exp (* access dereferenced using special accesses *)
+          access_one_top ~deref:true man kind reach exp (* access dereferenced using special accesses *)
         ) arglist;
       (match lv with
-       | Some x -> access_one_top ~deref:true ctx Write false (AddrOf x)
+       | Some x -> access_one_top ~deref:true man Write false (AddrOf x)
        | None -> ());
-      List.iter (access_one_top ctx Read false) arglist; (* always read all argument expressions without dereferencing *)
-      ctx.local
+      List.iter (access_one_top man Read false) arglist; (* always read all argument expressions without dereferencing *)
+      man.local
 
-  let enter ctx lv f args : (D.t * D.t) list =
-    [(ctx.local,ctx.local)]
+  let enter man lv f args : (D.t * D.t) list =
+    [(man.local,man.local)]
 
-  let combine_env ctx lval fexp f args fc au f_ask =
+  let combine_env man lval fexp f args fc au f_ask =
     (* These should be in enter, but enter cannot emit events, nor has fexp argument *)
-    access_one_top ctx Read false fexp;
-    List.iter (access_one_top ctx Read false) args;
+    access_one_top man Read false fexp;
+    List.iter (access_one_top man Read false) args;
     au
 
-  let combine_assign ctx lv fexp f args fc al f_ask =
+  let combine_assign man lv fexp f args fc al f_ask =
     begin match lv with
       | None      -> ()
-      | Some lval -> access_one_top ~deref:true ctx Write false (AddrOf lval)
+      | Some lval -> access_one_top ~deref:true man Write false (AddrOf lval)
     end;
-    ctx.local
+    man.local
 
 
-  let threadspawn ctx  ~multiple lval f args fctx =
+  let threadspawn man  ~multiple lval f args fman =
     (* must explicitly access thread ID lval because special to pthread_create doesn't if singlethreaded before *)
     begin match lval with
       | None -> ()
-      | Some lval -> access_one_top ~force:true ~deref:true ctx Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
+      | Some lval -> access_one_top ~force:true ~deref:true man Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
     end;
-    ctx.local
+    man.local
 
-  let query ctx (type a) (q: a Queries.t): a Queries.result =
+  let query man (type a) (q: a Queries.t): a Queries.result =
     match q with
     | MayAccessed ->
-      (ctx.global ctx.node: G.t)
+      (man.global man.node: G.t)
     | _ -> Queries.Result.top q
 
-  let event ctx e octx =
+  let event man e oman =
     match e with
     | Events.Access {ad; kind; _} when !collect_local && !AnalysisState.postsolving ->
       let events = Queries.AD.fold (fun addr es ->
@@ -151,9 +151,9 @@ struct
           | _ -> es
         ) ad (G.empty ())
       in
-      ctx.sideg ctx.node events
+      man.sideg man.node events
     | _ ->
-      ctx.local
+      man.local
 end
 
 let _ =

src/analyses/activeLongjmp.ml

@@ -12,25 +12,25 @@ struct
   (* The first component are the longjmp targets, the second are the longjmp callers *)
   module D = JmpBufDomain.ActiveLongjmps
 
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special arglist, f.vname with
     | Longjmp {env; value}, _ ->
       (* Set target to current value of env *)
-      let bufs = ctx.ask (EvalJumpBuf env) in
-      bufs, JmpBufDomain.NodeSet.singleton(ctx.prev_node)
-    | _ -> ctx.local
+      let bufs = man.ask (EvalJumpBuf env) in
+      bufs, JmpBufDomain.NodeSet.singleton(man.prev_node)
+    | _ -> man.local
 
   (* Initial values don't really matter: overwritten at longjmp call. *)
   let startstate v = D.bot ()
-  let threadenter ctx ~multiple lval f args = [D.bot ()]
+  let threadenter man ~multiple lval f args = [D.bot ()]
   let exitstate  v = D.top ()
 
-  let query ctx (type a) (q: a Queries.t): a Queries.result =
+  let query man (type a) (q: a Queries.t): a Queries.result =
     match q with
     | ActiveJumpBuf ->
       (* Does not compile without annotation: "This instance (...) is ambiguous: it would escape the scope of its equation" *)
-      (ctx.local:JmpBufDomain.ActiveLongjmps.t)
+      (man.local:JmpBufDomain.ActiveLongjmps.t)
     | _ -> Queries.Result.top q
 end
 

src/analyses/activeSetjmp.ml

@@ -13,24 +13,24 @@ struct
   include Analyses.ValueContexts(D)
   module P = IdentityP (D)
 
-  let combine_env ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask): D.t =
-    ctx.local (* keep local as opposed to IdentitySpec *)
+  let combine_env man (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask): D.t =
+    man.local (* keep local as opposed to IdentitySpec *)
 
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
+  let special man (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special arglist with
     | Setjmp _ ->
-      let entry = (ctx.prev_node, ctx.control_context ()) in
-      D.add (Target entry) ctx.local
-    | _ -> ctx.local
+      let entry = (man.prev_node, man.control_context ()) in
+      D.add (Target entry) man.local
+    | _ -> man.local
 
   let startstate v = D.bot ()
-  let threadenter ctx ~multiple lval f args = [D.bot ()]
+  let threadenter man ~multiple lval f args = [D.bot ()]
   let exitstate v = D.top ()
 
-  let query ctx (type a) (q: a Queries.t): a Queries.result =
+  let query man (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | ValidLongJmp -> (ctx.local: D.t)
+    | ValidLongJmp -> (man.local: D.t)
     | _ -> Queries.Result.top q
 end