Merge branch 'master' into apron_track_address

Author: michael-schwarz

docs/developer-guide/extending-library.md

@@ -0,0 +1,79 @@
+# Extending library
+
+Analyzed programs often call functions for which the implementation is not available to Goblint.
+These can belong to the standard libraries of C, POSIX, Linux kernel, etc or to project dependencies whose implementation is not available.
+
+Goblint outputs "Function definition missing" errors in such cases and by default assumes the worst about what the function does (invalidating everything).
+Such invalidation is a major source of imprecision and should be avoided at all cost (while still being sound).
+The semantics of unknown functions are controlled by options under `sem.unknown_function`, which can be used to avoid the invalidation, but disabling them if any unknown function does such invalidation will lead to unsoundness.
+
+To strike a better balance between soundness and precision, more fine-grained specifications can be provided in the `LibraryFunctions` module.
+
+
+## Library function specifications
+
+In the `LibraryFunctions` module (implementation), specifications of library functions are organized into a number of association lists.
+Functions are grouped based on their origin and context.
+This (in the future[^spec-list-selection]) allows groups of library function specifications to be toggled based on the program under analysis.
+
+There are also older (less granular) specifications implemented using `classify` and `invalidate_actions`.
+No new specifications should be added there and all the existing ones should be migrated to the new DSL-based format.
+
+[^spec-list-selection]: Specification list toggling will only be possible when all the old specifications are migrated.
+
+
+## Library function descriptor DSL
+
+A library function's specification is a pair of its name and descriptor (of type `LibraryDesc.t`).
+The descriptors are easiest written using the OCaml DSL from `LibraryDsl`.
+
+
+### Function descriptor
+
+A function descriptor can be one of the following:
+
+1. `special` consists of an arguments descriptor and a continuation function for converting the captured arguments to a `LibraryDesc.special` variant.
+    This is used when the library function should (or at least could) be specially handled by analyses.
+
+2. `unknown` consists of just an arguments descriptor (which must `drop` all arguments) and defaults to `Unknown` variant.
+    This is used when the library function isn't specially handled by analyses.
+
+
+### Arguments descriptor
+
+An arguments descriptor is a list (with standard OCaml list syntax) of individual argument descriptors.
+Additionally for library functions with variadic arguments, the list may be terminated with `VarArg` constructor instead of `[]`.
+
+
+### Argument descriptor
+
+An argument descriptor can be one of the following:
+
+1. `__` captures the argument expression for use in `special`'s continuation function.
+2. `drop` ignores (drops) the argument expression to not be used by the continuation.
+
+Both functions consist of an argument name string (for readability purposes) and a list of accesses the function does to the _pointer_ argument.
+
+Unnamed variants of the functions `__'` and `drop'` also exist, but should be avoided.
+
+
+### Access
+
+An access consists of an access kind and depth.
+Access kinds (`AccessKind.t`) are: read, write, free and spawn.
+
+Accesses specify what the library function may do with the corresponding _pointer_ argument.
+Since function calls unconditionally read the immediate expressions given as arguments, there would be no point specifying that all the arguments (including of integer) type are read.
+Also, non-pointer arguments are copied (passed-by-value) to the function, so write accesses would make no sense.
+Therefore only pointer arguments should have accesses specified.
+
+Two depths of accessing are distinguished:
+
+1. Shallow (non-transitive, may-point-to) access means the function dereferences the pointer argument, but doesn't dereference any pointers within (e.g. if a pointer to struct is given as argument, but the struct contains further pointers).
+    This is is almost always the case for standard library functions, since they take `void*` or `char*` as generic memory arguments and don't know about any pointers within the pointed block of memory.
+
+2. Deep (transitive, reachable) access means the function follows (dereferences) pointers within.
+
+In the DSL, shallow accesses can be specified by `r`, `w`, `f` or `s`, respectively. Deep accesses can be specified using the previous values with an additional `_deep` suffix.
+
+

goblint.opam

@@ -68,7 +68,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#9118601602d34edf53f73b35996abf2296c2d900" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

goblint.opam.locked

@@ -124,7 +124,7 @@ version: "dev"
 pin-depends: [
   [
     "goblint-cil.1.8.2"
-    "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9"
+    "git+https://github.com/goblint/cil.git#9118601602d34edf53f73b35996abf2296c2d900"
   ]
   [
     "apron.v0.9.13"

goblint.opam.template

@@ -1,7 +1,7 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 pin-depends: [
-  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#0a37478e08b9ae10587b0355ad2805dfeca1cca9" ]
+  [ "goblint-cil.1.8.2" "git+https://github.com/goblint/cil.git#9118601602d34edf53f73b35996abf2296c2d900" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
   # quoter workaround reverted for release, so no pin needed

gobview

@@ -11,6 +11,7 @@ theme:
 markdown_extensions:
   - toc:
       permalink: True
+  - footnotes
 
 dev_addr: '127.0.0.1:8010' # different port from default python http.server for g2html
 
@@ -24,6 +25,7 @@ nav:
   - 'Developer guide':
     - developer-guide/developing.md
     - developer-guide/firstanalysis.md
+    - developer-guide/extending-library.md
     - developer-guide/messaging.md
     - developer-guide/testing.md
     - developer-guide/debugging.md

mkdocs.yml

@@ -50,6 +50,7 @@ struct
     ctx.sideg (lv_opt, ty) d
 
   let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (conf:int) (e:exp) =
+    if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach;
     let open Queries in
     let part_access ctx (e:exp) (vo:varinfo option) (kind: AccessKind.t): MCPAccess.A.t =
       ctx.emit (Access {var_opt=vo; kind});
@@ -106,17 +107,18 @@ struct
     | _ ->
       add_access (conf - 60) None None
 
-  let access_one_top ?(force=false) ctx kind reach exp =
-    (* ignore (Pretty.printf "access_one_top %b %b %a:\n" write reach d_exp exp); *)
+  (** 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 =
+    if M.tracing then M.traceli "access" "access_one_top %a %b %a:\n" AccessKind.pretty kind reach d_exp exp;
     if force || ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) then (
       let conf = 110 in
-      let write = match kind with
-        | `Write | `Free -> true
-        | `Read -> false
-      in
-      if reach || write then do_access ctx kind reach conf exp;
-      Access.distribute_access_exp (do_access ctx) `Read false conf exp;
-    )
+      if deref then do_access ctx kind reach conf exp;
+      Access.distribute_access_exp (do_access ctx Read false) conf exp;
+    );
+    if M.tracing then M.traceu "access" "access_one_top %a %b %a\n" AccessKind.pretty kind reach d_exp exp
 
   (** We just lift start state, global and dependency functions: *)
   let startstate v = ()
@@ -129,18 +131,18 @@ struct
   let assign ctx lval rval : D.t =
     (* ignore global inits *)
     if !GU.global_initialization then ctx.local else begin
-      access_one_top ctx `Write false (AddrOf lval);
-      access_one_top ctx `Read false rval;
+      access_one_top ~deref:true ctx Write false (AddrOf lval);
+      access_one_top ctx Read false rval;
       ctx.local
     end
 
   let branch ctx exp tv : D.t =
-    access_one_top ctx `Read false exp;
+    access_one_top ctx Read false exp;
     ctx.local
 
   let return ctx exp fundec : D.t =
     begin match exp with
-      | Some exp -> access_one_top ctx `Read false exp
+      | Some exp -> access_one_top ctx Read false exp
       | None -> ()
     end;
     ctx.local
@@ -149,18 +151,19 @@ struct
     ctx.local
 
   let special ctx lv f arglist : D.t =
-    match (LF.classify f.vname arglist, f.vname) with
+    let desc = LF.find f in
+    match desc.special arglist, f.vname with
     (* TODO: remove cases *)
     | _, "_lock_kernel" ->
       ctx.local
     | _, "_unlock_kernel" ->
       ctx.local
-    | `Lock (failing, rw, nonzero_return_when_aquired), _
+    | Lock { try_ = failing; write = rw; return_on_success = nonzero_return_when_aquired; _ }, _
       -> ctx.local
-    | `Unlock, "__raw_read_unlock"
-    | `Unlock, "__raw_write_unlock"  ->
+    | Unlock _, "__raw_read_unlock"
+    | Unlock _, "__raw_write_unlock"  ->
       ctx.local
-    | `Unlock, _ ->
+    | Unlock _, _ ->
       ctx.local
     | _, "spinlock_check" -> ctx.local
     | _, "acquire_console_sem" when get_bool "kernel" ->
@@ -176,51 +179,34 @@ struct
     | _, "pthread_cond_wait"
     | _, "pthread_cond_timedwait" ->
       ctx.local
-    | _, x ->
-      let arg_acc act =
-        match act, LF.get_threadsafe_inv_ac x with
-        | _, Some fnc -> (fnc act arglist)
-        | `Read, None -> arglist
-        | (`Write | `Free), None ->
-          if get_bool "sem.unknown_function.invalidate.args" then
-            arglist
-          else
-            []
-      in
-      (* TODO: per-argument reach *)
-      let reach =
-        match f.vname with
-        | "memset" | "__builtin_memset" | "__builtin___memset_chk" -> false
-        | "bzero" | "__builtin_bzero" | "explicit_bzero" | "__explicit_bzero_chk" -> false
-        | "__builtin_object_size" -> false
-        | _ -> true
-      in
-      List.iter (access_one_top ctx `Read reach) (arg_acc `Read);
-      List.iter (access_one_top ctx `Write reach) (arg_acc `Write);
-      List.iter (access_one_top ctx `Free reach) (arg_acc `Free);
+    | _, _ ->
+      LibraryDesc.Accesses.iter desc.accs (fun {kind; deep = reach} exp ->
+          access_one_top ~deref:true ctx kind reach exp (* access dereferenced using special accesses *)
+        ) arglist;
       (match lv with
-       | Some x -> access_one_top ctx `Write false (AddrOf x)
+       | Some x -> access_one_top ~deref:true ctx Write false (AddrOf x)
        | None -> ());
+      List.iter (access_one_top ctx Read false) arglist; (* always read all argument expressions without dereferencing *)
       ctx.local
 
   let enter ctx lv f args : (D.t * D.t) list =
     [(ctx.local,ctx.local)]
 
   let combine ctx lv fexp f args fc al =
-    access_one_top ctx `Read false fexp;
+    access_one_top ctx Read false fexp;
     begin match lv with
       | None      -> ()
-      | Some lval -> access_one_top ctx `Write false (AddrOf lval)
+      | Some lval -> access_one_top ~deref:true ctx Write false (AddrOf lval)
     end;
-    List.iter (access_one_top ctx `Read false) args;
+    List.iter (access_one_top ctx Read false) args;
     al
 
 
   let threadspawn ctx lval f args fctx =
     (* 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 ctx `Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
+      | Some lval -> access_one_top ~force:true ~deref:true ctx Write false (AddrOf lval) (* must force because otherwise doesn't if singlethreaded before *)
     end;
     ctx.local
 

src/analyses/accessAnalysis.ml

@@ -373,17 +373,18 @@ struct
           invalidate_one ask ctx st (Lval.CilLval.to_lval lval)
         ) rs st
 
-
   let special ctx r f args =
     let ask = Analyses.ask_of_ctx ctx in
     let st = ctx.local in
-    match LibraryFunctions.classify f.vname args with
+    let desc = LibraryFunctions.find f in
+    match desc.special args, f.vname with
     (* TODO: assert handling from https://github.com/goblint/analyzer/pull/278 *)
-    | `Assert expression -> st
-    | `Unknown "__goblint_check" -> st
-    | `Unknown "__goblint_commit" -> st
-    | `Unknown "__goblint_assert" -> st
-    | `ThreadJoin (id,retvar) ->
+    | Assert expression, _ -> st
+    | Unknown, "__goblint_check" -> st
+    | Unknown, "__goblint_commit" -> st
+    | Unknown, "__goblint_assert" -> st
+    | ThreadJoin { thread = id; ret_var = retvar }, _ ->
+      (* nothing to invalidate as only arguments that have their AddrOf taken may be invalidated *)
       (
         (* Forget value that thread return is assigned to *)
         let st' = forget_reachable ctx st [retvar] in
@@ -392,29 +393,33 @@ struct
         | Some lv -> invalidate_one ask ctx st' lv
         | None -> st'
       )
-    | _ ->
-      let ask = Analyses.ask_of_ctx ctx in
-      let st' = match LibraryFunctions.get_invalidate_action f.vname with
-        | Some fnc -> forget_reachable ctx st (fnc `Write args)
-        | None ->
-          let st' = if GobConfig.get_bool "sem.unknown_function.invalidate.globals" then (
-            let globals = foldGlobals !Cilfacade.current_file (fun acc global ->
-                match global with
-                | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
-                  (Var vi, NoOffset) :: acc
-                (* TODO: what about GVarDecl? *)
-                | _ -> acc
-              ) []
-            in
-            List.fold_left (invalidate_one ask ctx) st globals)
-          else
-            st
+    | _, _ ->
+      let lvallist e =
+        let s = ask.f (Queries.MayPointTo e) in
+        match s with
+        | `Top -> []
+        | `Lifted _ -> List.map (Lval.CilLval.to_lval) (Queries.LS.elements s)
+      in
+      let shallow_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = false } args in
+      let deep_addrs = LibraryDesc.Accesses.find desc.accs { kind = Write; deep = true } args in
+      let st' =
+        if List.mem LibraryDesc.InvalidateGlobals desc.attrs then (
+          let globals = foldGlobals !Cilfacade.current_file (fun acc global ->
+              match global with
+              | GVar (vi, _, _) when not (BaseUtil.is_static vi) ->
+                (Var vi, NoOffset) :: acc
+              (* TODO: what about GVarDecl? *)
+              | _ -> acc
+            ) []
           in
-          if GobConfig.get_bool "sem.unknown_function.invalidate.args" then
-            forget_reachable ctx st' args
-          else
-            st'
+          List.fold_left (invalidate_one ask ctx) st globals
+        )
+        else
+          st
       in
+      let st' = forget_reachable ctx st' deep_addrs in
+      let shallow_lvals = List.concat_map lvallist shallow_addrs in
+      let st' = List.fold_left (invalidate_one ask ctx) st' shallow_lvals in
       (* invalidate lval if present *)
       match r with
       | Some lv -> invalidate_one ask ctx st' lv
@@ -433,7 +438,8 @@ struct
     in
     match q with
     | EvalInt e ->
-      if M.tracing then M.traceli "evalint" "apron query %a\n" d_exp e;
+      if M.tracing then M.traceli "evalint" "apron query %a (%a)\n" d_exp e d_plainexp e;
+      if M.tracing then M.trace "evalint" "apron st: %a\n" D.pretty ctx.local;
       let r = eval_int e in
       if M.tracing then M.traceu "evalint" "apron query %a -> %a\n" d_exp e ID.pretty r;
       r