Merge branch 'master' into feature/divide-and-narrow

.git-blame-ignore-revs

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

dune-project

@@ -58,7 +58,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (sha (>= 1.12))
     (fileutils (>= 0.6.4))
     cpu
-    arg-complete
+    (arg-complete (>= 0.2.1))
     (yaml (>= 3.0.0))
     uuidm
     catapult

goblint.opam

@@ -58,7 +58,7 @@ depends: [
   "sha" {>= "1.12"}
   "fileutils" {>= "0.6.4"}
   "cpu"
-  "arg-complete"
+  "arg-complete" {>= "0.2.1"}
   "yaml" {>= "3.0.0"}
   "uuidm"
   "catapult"
@@ -98,7 +98,7 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
   # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
+  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

goblint.opam.locked

@@ -24,7 +24,7 @@ bug-reports: "https://github.com/goblint/analyzer/issues"
 depends: [
   "angstrom" {= "0.16.0"}
   "apron" {= "v0.9.15"}
-  "arg-complete" {= "0.1.0"}
+  "arg-complete" {= "0.2.1"}
   "astring" {= "0.8.5"}
   "base-bigarray" {= "base"}
   "base-bytes" {= "base"}
@@ -140,7 +140,7 @@ post-messages: [
 pin-depends: [
   [
     "goblint-cil.2.0.5"
-    "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd"
+    "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f"
   ]
   [
     "camlidl.1.12"

goblint.opam.template

@@ -3,7 +3,7 @@
 available: os-family != "bsd" & os-distribution != "alpine" & (arch != "arm64" | os = "macos")
 pin-depends: [
   # published goblint-cil 2.0.5 is currently up-to-date, but pinned for reproducibility
-  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#c79208b21ea61d7b72eae29a18c1ddeda4795dfd" ]
+  [ "goblint-cil.2.0.5" "git+https://github.com/goblint/cil.git#f5ee39bd344dc74e2a10e407d877e0ddf73c9c6f" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new camlidl release
   [ "camlidl.1.12" "git+https://github.com/xavierleroy/camlidl.git#1c1e87e3f56c2c6b3226dd0af3510ef414b462d0" ]
   # pinned for stability (https://github.com/goblint/analyzer/issues/1520), remove after new apron release

mkdocs.yml

@@ -41,3 +41,4 @@ nav:
     - "🇸 SAS '21": artifact-descriptions/sas21.md
     - "🇪 ESOP '23": artifact-descriptions/esop23.md
     - "🇻 VMCAI '24": artifact-descriptions/vmcai24.md
+    - "🇻 VMCAI '25": artifact-descriptions/vmcai25.md

scripts/bash-completion.sh

@@ -6,10 +6,27 @@
 # Permanent usage:
 #   Run: echo "source $(readlink -f .)/scripts/bash-completion.sh" >> ~/.bash_completion
 
+# Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
+# Copied & modified from standard __ltrim_colon_completions
+__ltrim_equal_completions()
+{
+    if [[ $1 == *=* && $COMP_WORDBREAKS == *=* ]]; then
+        # Remove equal-word prefix from COMPREPLY items
+        local equal_word=${1%"${1##*=}"}
+        local i=${#COMPREPLY[*]}
+        while ((i-- > 0)); do
+            COMPREPLY[i]=${COMPREPLY[i]#"$equal_word"}
+        done
+    fi
+}
+
 _goblint ()
 {
     IFS=$'\n'
-    COMPREPLY=($(${COMP_WORDS[0]} --complete "${COMP_WORDS[@]:1:COMP_CWORD}"))
+    local words cword cur
+    _get_comp_words_by_ref -n = cur words cword # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
+    COMPREPLY=($(${words[0]} --complete "${words[@]:1:cword}"))
+    __ltrim_equal_completions "$cur" # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
 }
 
 complete -o default -F _goblint goblint
@@ -26,7 +43,10 @@ _regtest ()
             COMPREPLY=($(ls -1 tests/regression/${COMP_WORDS[1]}-* | sed -n -r 's/([0-9][0-9])-.*/\1/p' | grep "^${COMP_WORDS[2]}"))
             ;;
         *)
-            COMPREPLY=($($(dirname ${COMP_WORDS[0]})/goblint --complete "${COMP_WORDS[@]:3:COMP_CWORD}"))
+            local words cword cur
+            _get_comp_words_by_ref -n = cur words cword # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
+            COMPREPLY=($($(dirname ${words[0]})/goblint --complete "${words[@]:3:cword}"))
+            __ltrim_equal_completions "$cur" # Bypass = in COMP_WORDBREAKS (https://stackoverflow.com/a/57437406/854540)
             ;;
     esac
 }

scripts/goblint-lib-modules.py

@@ -48,6 +48,12 @@
 
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
+    "IntervalDomain", # included in IntDomain
+    "IntervalSetDomain", # included in IntDomain
+    "DefExcDomain", # included in IntDomain
+    "EnumsDomain", # included in IntDomain
+    "CongruenceDomain", # included in IntDomain
+    "IntDomTuple", # included in IntDomain
     "WitnessGhostVar", # included in WitnessGhost
 
     "ConfigVersion",

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 _ =