Merge branch 'relational-substring-domain' of github.com:nathanschmid…

…t/goblint-analyzer into relational-substring-domain

.github/workflows/docs.yml

@@ -52,7 +52,7 @@ jobs:
         run: opam exec -- dune build @doc
 
       - name: Upload artifact
-        uses: actions/upload-pages-artifact@v1
+        uses: actions/upload-pages-artifact@v2
         with:
           path: _build/default/_doc/_html/
 

.github/workflows/locked.yml

@@ -174,5 +174,4 @@ jobs:
 
       - name: Test Gobview
         run: |
-          ./goblint --enable gobview tests/regression/00-sanity/01-assert.c
           python3 scripts/test-gobview.py

docs/user-guide/inspecting.md

@@ -22,4 +22,4 @@ To build GobView (also for development):
 2. The executable for the http-server can then be found in the directory `./_build/default/gobview/goblint-http-server`. It takes the analyzer directory and additional Goblint configurations such as the files to be analyzed as parameters. Run it e.g. with the following command:\
 `./_build/default/gobview/goblint-http-server/goblint_http.exe -with-goblint ../analyzer/goblint -goblint --set files[+] "../analyzer/tests/regression/00-sanity/01-assert.c"`
 
-4. Visit <http://localhost:8000>
+4. Visit <http://localhost:8080>

scripts/test-gobview.py

@@ -7,32 +7,30 @@
 from selenium.webdriver.common.by import By
 from selenium.webdriver.chrome.options import Options
 from threading import Thread
-import http.server
-import socketserver
+import subprocess
 
-PORT = 9000
+PORT = 8080 # has to match port defined in goblint_http.ml
 DIRECTORY = "run"
 IP = "localhost"
 url = 'http://' + IP + ':' + str(PORT) + '/'
 
 # cleanup
-def cleanup(browser, httpd, thread):
+def cleanup(browser, thread):
   print("cleanup")
   browser.close()
-  httpd.shutdown()
-  httpd.server_close()
+  p.kill()
   thread.join()
 
 # serve GobView in different thread so it does not block the testing
-class Handler(http.server.SimpleHTTPRequestHandler):
-    def __init__(self, *args, **kwargs):
-        super().__init__(*args, directory=DIRECTORY, **kwargs)
-class Server(socketserver.TCPServer):
-    allow_reuse_address = True # avoids that during a consecutive run the server cannot connect due to an 'Adress already in use' os error
+def serve():
+  global p
+  goblint_http_path = '_build/default/gobview/goblint-http-server/goblint_http.exe'
+  p = subprocess.Popen(['./' + goblint_http_path,
+                  '-with-goblint', '../analyzer/goblint',
+                  '-goblint', '--set', 'files[+]', '"../analyzer/tests/regression/00-sanity/01-assert.c"'])
 
-httpd = Server((IP, PORT), Handler)
 print("serving at port", PORT)
-thread = Thread(target=httpd.serve_forever, args=())
+thread = Thread(target=serve, args=())
 thread.start()
 
 # installation of browser
@@ -42,6 +40,7 @@ class Server(socketserver.TCPServer):
 browser = webdriver.Chrome(service=Service(ChromeDriverManager().install()),options=options)
 print("finished webdriver installation \n")
 browser.maximize_window()
+browser.implicitly_wait(10);
 
 try:
     # retrieve and wait until page is fully loaded and rendered
@@ -62,8 +61,8 @@ class Server(socketserver.TCPServer):
     panel = browser.find_element(By.CLASS_NAME, "panel")
     print("found DOM elements main, sidebar-left, sidebar-right, content and panel")
 
-    cleanup(browser, httpd, thread)
+    cleanup(browser, thread)
 
 except Exception as e:
-    cleanup(browser, httpd, thread)
+    cleanup(browser, thread)
     raise e

src/analyses/apron/relationAnalysis.apron.ml

@@ -507,6 +507,12 @@ struct
     | Unknown, "__goblint_assume_join" ->
       let id = List.hd args in
       Priv.thread_join ~force:true ask ctx.global id st
+    | Rand, _ ->
+      (match r with
+       | Some lv ->
+         let st = invalidate_one ask ctx st lv in
+         assert_fn {ctx with local = st} (BinOp (Ge, Lval lv, zero, intType)) true
+       | None -> st)
     | _, _ ->
       let lvallist e =
         let s = ask.f (Queries.MayPointTo e) in

src/analyses/apron/relationPriv.apron.ml

@@ -713,11 +713,7 @@ module DownwardClosedCluster (ClusteringArg: ClusteringArg) =  functor (RD: Rela
 struct
   open CommonPerMutex(RD)
 
-  module VS =
-  struct
-    include Printable.Std
-    include SetDomain.Make (CilType.Varinfo)
-  end
+  module VS = SetDomain.Make (CilType.Varinfo)
   module LRD = MapDomain.MapBot (VS) (RD)
 
   let keep_only_protected_globals ask m octs =

src/analyses/base.ml

@@ -1336,7 +1336,8 @@ struct
           (* ignore @@ printf "EvalStr Unknown: %a -> %s\n" d_plainexp e (VD.short 80 x); *)
           Queries.Result.top q
       end
-    | Q.IsMultiple v -> WeakUpdates.mem v ctx.local.weak
+    | Q.IsMultiple v -> WeakUpdates.mem v ctx.local.weak ||
+                        (hasAttribute "thread" v.vattr && v.vaddrof) (* thread-local variables if they have their address taken, as one could then compare several such variables *)
     | Q.IterSysVars (vq, vf) ->
       let vf' x = vf (Obj.repr (V.priv x)) in
       Priv.iter_sys_vars (priv_getg ctx.global) vq vf'
@@ -2362,6 +2363,13 @@ struct
       let rv = ensure_not_zero @@ eval_rv ask ctx.global ctx.local value in
       let t = Cilfacade.typeOf value in
       set ~ctx ~t_override:t ask ctx.global ctx.local (AD.of_var !longjmp_return) t rv (* Not raising Deadcode here, deadcode is raised at a higher level! *)
+    | Rand, _ ->
+      begin match lv with
+      | Some x -> 
+        let result:value = (Int (ID.starting IInt Z.zero)) in
+        set ~ctx (Analyses.ask_of_ctx ctx) gs st (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st x) (Cilfacade.typeOfLval x) result
+      | None -> st
+      end
     | _, _ ->
       let st =
         special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args

src/analyses/baseInvariant.ml

@@ -57,33 +57,30 @@ struct
     | Bot -> false (* HACK: bot is here due to typing conflict (we do not cast appropriately) *)
     | _ -> VD.is_bot_value x
 
-  let apply_invariant oldv newv =
-    match oldv, newv with
-    (* | Address o, Address n when AD.mem (Addr.unknown_ptr ()) o && AD.mem (Addr.unknown_ptr ()) n -> *)
-    (*   Address (AD.join o n) *)
-    (* | Address o, Address n when AD.mem (Addr.unknown_ptr ()) o -> Address n *)
-    (* | Address o, Address n when AD.mem (Addr.unknown_ptr ()) n -> Address o *)
-    | _ -> VD.meet oldv newv
+  let apply_invariant ~old_val ~new_val =
+    try
+      VD.meet old_val new_val
+    with Lattice.Uncomparable -> old_val
 
   let refine_lv_fallback ctx a gs st lval value tv =
     if M.tracing then M.tracec "invariant" "Restricting %a with %a\n" d_lval lval VD.pretty value;
     let addr = eval_lv a gs st lval in
     if (AD.is_top addr) then st
     else
-      let oldval = get a gs st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *)
+      let old_val = get a gs st addr None in (* None is ok here, we could try to get more precise, but this is ok (reading at unknown position in array) *)
       let t_lval = Cilfacade.typeOfLval lval in
-      let oldval = map_oldval oldval t_lval in
-      let oldval =
-        if is_some_bot oldval then (
+      let old_val = map_oldval old_val t_lval in
+      let old_val =
+        if is_some_bot old_val then (
           if M.tracing then M.tracec "invariant" "%a is bot! This should not happen. Will continue with top!" d_lval lval;
           VD.top ()
         )
         else
-          oldval
+          old_val
       in
       let state_with_excluded = set a gs st addr t_lval value ~ctx in
       let value =  get a gs state_with_excluded addr None in
-      let new_val = apply_invariant oldval value in
+      let new_val = apply_invariant ~old_val ~new_val:value in
       if M.tracing then M.traceu "invariant" "New value is %a\n" VD.pretty new_val;
       (* make that address meet the invariant, i.e exclusion sets will be joined *)
       if is_some_bot new_val then (
@@ -99,27 +96,27 @@ struct
     match x with
     | Var var, o when refine_entire_var ->
       (* For variables, this is done at to the level of entire variables to benefit e.g. from disjunctive struct domains *)
-      let oldv = get_var a gs st var in
-      let oldv = map_oldval oldv var.vtype in
+      let old_val = get_var a gs st var in
+      let old_val = map_oldval old_val var.vtype in
       let offs = convert_offset a gs st o in
-      let newv = VD.update_offset (Queries.to_value_domain_ask a) oldv offs c' (Some exp) x (var.vtype) in
-      let v = VD.meet oldv newv in
+      let new_val = VD.update_offset (Queries.to_value_domain_ask a) old_val offs c' (Some exp) x (var.vtype) in
+      let v = apply_invariant ~old_val ~new_val in
       if is_some_bot v then contra st
       else (
-        if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)\n" CilType.Varinfo.pretty var VD.pretty oldv VD.pretty v pretty c VD.pretty c';
+        if M.tracing then M.tracel "inv" "improve variable %a from %a to %a (c = %a, c' = %a)\n" CilType.Varinfo.pretty var VD.pretty old_val VD.pretty v pretty c VD.pretty c';
         let r = set' (Var var,NoOffset) v st in
         if M.tracing then M.tracel "inv" "st from %a to %a\n" D.pretty st D.pretty r;
         r
       )
     | Var _, _
     | Mem _, _ ->
       (* For accesses via pointers, not yet *)
-      let oldv = eval_rv_lval_refine a gs st exp x in
-      let oldv = map_oldval oldv (Cilfacade.typeOfLval x) in
-      let v = VD.meet oldv c' in
+      let old_val = eval_rv_lval_refine a gs st exp x in
+      let old_val = map_oldval old_val (Cilfacade.typeOfLval x) in
+      let v = apply_invariant ~old_val ~new_val:c' in
       if is_some_bot v then contra st
       else (
-        if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)\n" d_lval x VD.pretty oldv VD.pretty v pretty c VD.pretty c';
+        if M.tracing then M.tracel "inv" "improve lval %a from %a to %a (c = %a, c' = %a)\n" d_lval x VD.pretty old_val VD.pretty v pretty c VD.pretty c';
         set' x v st
       )
 

src/analyses/commonPriv.ml

@@ -117,11 +117,7 @@ module Locksets =
 struct
   module Lock = LockDomain.Addr
 
-  module Lockset =
-  struct
-    include Printable.Std (* To make it Groupable *)
-    include SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
-  end
+  module Lockset = SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
 
   module MustLockset = SetDomain.Reverse (Lockset)
 

src/analyses/libraryDesc.ml

@@ -72,6 +72,7 @@ type special =
   | Identity of Cil.exp (** Identity function. Some compiler optimization annotation functions map to this. *)
   | Setjmp of { env: Cil.exp; }
   | Longjmp of { env: Cil.exp; value: Cil.exp; }
+  | Rand
   | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
 
 

src/analyses/libraryFunctions.ml

@@ -70,6 +70,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
+    ("rand", special [] Rand);
   ]
 
 (** C POSIX library functions.
@@ -872,7 +873,6 @@ let invalidate_actions = [
     "sendto", writes [2;4]; (*keep [2;4]*)
     "recvfrom", writes [4;5]; (*keep [4;5]*)
     "srand", readsAll; (*safe*)
-    "rand", readsAll; (*safe*)
     "gethostname", writesAll; (*unsafe*)
     "fork", readsAll; (*safe*)
     "setrlimit", readsAll; (*safe*)

src/analyses/spec.ml

@@ -253,7 +253,7 @@ struct
     | Some k1, Some k2 when D.mem k2 m -> (* only k2 in D *)
       M.debug ~category:Analyzer "assign (only k2 in D): %s = %s" (D.string_of_key k1) (D.string_of_key k2);
       let m = D.alias k1 k2 m in (* point k1 to k2 *)
-      if Basetype.Variables.to_group (fst k2) = Some Temp (* check if k2 is a temporary Lval introduced by CIL *)
+      if Basetype.Variables.to_group (fst k2) = Temp (* check if k2 is a temporary Lval introduced by CIL *)
       then D.remove' k2 m (* if yes we need to remove it from our map *)
       else m (* otherwise no change *)
     | Some k1, _ when D.mem k1 m -> (* k1 in D and assign something unknown *)

src/analyses/useAfterFree.ml

@@ -1,10 +1,11 @@
-(** An analysis for the detection of use-after-free vulnerabilities. *)
+(** An analysis for the detection of use-after-free vulnerabilities ([useAfterFree]). *)
 
 open GoblintCil
 open Analyses
 open MessageCategory
 
 module ToppedVarInfoSet = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end)
+module ThreadIdSet = SetDomain.Make(ThreadIdDomain.ThreadLifted)
 
 module Spec : Analyses.MCPSpec =
 struct
@@ -14,22 +15,61 @@ struct
 
   module D = ToppedVarInfoSet
   module C = Lattice.Unit
+  module G = ThreadIdSet
+  module V = VarinfoV
 
   (** TODO: Try out later in benchmarks to see how we perform with and without context-sensititivty *)
   let context _ _ = ()
 
 
   (* HELPER FUNCTIONS *)
 
-  let warn_for_multi_threaded ctx behavior cwe_number =
-    if not (ctx.ask (Queries.MustBeSingleThreaded { since_start = true })) then
-      M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Program isn't running in single-threaded mode. Use-After-Free might occur due to multi-threading"
+  let get_current_threadid ctx =
+    ctx.ask Queries.CurrentThreadId
+
+  let warn_for_multi_threaded_access ctx (heap_var:varinfo) behavior cwe_number =
+    let freeing_threads = ctx.global heap_var in
+    (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *)
+    if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || ThreadIdSet.is_empty freeing_threads then ()
+    else begin
+      let possibly_started current = function
+        | `Lifted tid ->
+          let threads = ctx.ask Queries.CreatedThreads in
+          let not_started = MHP.definitely_not_started (current, threads) tid in
+          let possibly_started = not not_started in
+          possibly_started
+        | `Top -> true
+        | `Bot -> false
+      in
+      let equal_current current = function
+        | `Lifted tid ->
+          ThreadId.Thread.equal current tid
+        | `Top -> true
+        | `Bot -> false
+      in
+      match get_current_threadid ctx with
+      | `Lifted current ->
+        let possibly_started = ThreadIdSet.exists (possibly_started current) freeing_threads in
+        if possibly_started then
+          M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. Use-After-Free might occur" CilType.Varinfo.pretty heap_var
+        else begin
+          let current_is_unique = ThreadId.Thread.is_unique current in
+          let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in
+          if not current_is_unique && any_equal_current freeing_threads then
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Current thread is not unique and a Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var
+          else if D.mem heap_var ctx.local then
+            M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "Use-After-Free might occur in current unique thread %a for heap variable %a" ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var
+        end
+      | `Top ->
+        M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "CurrentThreadId is top. A Use-After-Free might occur for heap variable %a" CilType.Varinfo.pretty heap_var
+      | `Bot ->
+        M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom"
+    end
 
   let rec warn_lval_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (lval:lval) =
     let state = ctx.local in
     let undefined_behavior = if is_double_free then Undefined DoubleFree else Undefined UseAfterFree in
     let cwe_number = if is_double_free then 415 else 416 in
-    warn_for_multi_threaded ctx undefined_behavior cwe_number; (* Simple solution to warn when multi-threaded *)
     let rec offset_might_contain_freed offset =
       match offset with
       | NoOffset -> ()
@@ -53,7 +93,9 @@ struct
         |> List.map fst
         |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var))
       in
-      List.iter warn_for_heap_var pointed_to_heap_vars (* Warn for all heap vars that the lval possibly points to *)
+      List.iter warn_for_heap_var pointed_to_heap_vars; (* Warn for all heap vars that the lval possibly points to *)
+      (* Warn for a potential multi-threaded UAF for all heap vars that the lval possibly points to *)
+      List.iter (fun heap_var -> warn_for_multi_threaded_access ctx heap_var undefined_behavior cwe_number) pointed_to_heap_vars
     | _ -> ()
 
   and warn_exp_might_contain_freed ?(is_double_free = false) (transfer_fn_name:string) ctx (exp:exp) =
@@ -83,6 +125,10 @@ struct
     | StartOf lval
     | AddrOf lval -> warn_lval_might_contain_freed ~is_double_free transfer_fn_name ctx lval
 
+  let side_effect_mem_free ctx freed_heap_vars threadid =
+    let threadid = G.singleton threadid in
+    D.iter (fun var -> ctx.sideg var threadid) freed_heap_vars
+
 
   (* TRANSFER FUNCTIONS *)
 
@@ -138,8 +184,11 @@ struct
             Queries.LS.elements a
             |> List.map fst
             |> List.filter (fun var -> ctx.ask (Queries.IsHeapVar var))
+            |> D.of_list
           in
-          D.join state (D.of_list pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *)
+          (* Side-effect the tid that's freeing all the heap vars collected here *)
+          side_effect_mem_free ctx pointed_to_heap_vars (get_current_threadid ctx);
+          D.join state (pointed_to_heap_vars) (* Add all heap vars, which ptr points to, to the state *)
         | _ -> state
       end
     | _ -> state

src/cdomains/addressDomain.ml

@@ -76,12 +76,6 @@ module AddressPrintable (Mval: Mval.Printable) =
 struct
   include AddressBase (Mval)
 
-  type group = Basetype.Variables.group
-  let show_group = Basetype.Variables.show_group
-  let to_group = function
-    | Addr (x,_) -> Basetype.Variables.to_group x
-    | _ -> Some Basetype.Variables.Local
-
   let of_var x = Addr (x, `NoOffset)
   let of_mval (x, o) = Addr (x, o)