Analysis of longjmp/setjmp

src/analyses/activeLongjmp.ml

@@ -0,0 +1,60 @@
+(** Analysis tracking which longjmp is currently active *)
+
+open Prelude.Ana
+open Analyses
+
+(* module Spec : Analyses.MCPSpec with module D = Lattice.Unit and module C = Lattice.Unit and type marshal = unit = *)
+(* No signature so others can override module G *)
+module Spec =
+struct
+  include Analyses.DefaultSpec
+
+  let name () = "activeLongjmp"
+  module D = JmpBufDomain.JmpBufSet
+  module C = Lattice.Unit
+
+  (* transfer functions *)
+  let assign ctx (lval:lval) (rval:exp) : D.t =
+    ctx.local
+
+  let branch ctx (exp:exp) (tv:bool) : D.t =
+    ctx.local
+
+  let body ctx (f:fundec) : D.t =
+    ctx.local
+
+  let return ctx (exp:exp option) (f:fundec) : D.t =
+    ctx.local
+
+  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
+    [ctx.local, ctx.local]
+
+  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
+    au
+
+  let special ctx (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; sigrestore}, _ ->
+      (* Put current buffer into set *)
+      let bufs = ctx.ask (EvalJumpBuf env) in
+      bufs
+    | _ -> ctx.local
+
+  let startstate v = D.bot ()
+  let threadenter ctx lval f args = [D.top ()]
+  let threadspawn ctx lval f args fctx = ctx.local
+  let exitstate  v = D.top ()
+
+  let context _ _ = ()
+
+  let query ctx (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.JmpBufSet.t)
+    | _ -> Queries.Result.top q
+end
+
+let _ =
+  MCP.register_analysis (module Spec : MCPSpec)

src/analyses/base.ml

@@ -528,6 +528,7 @@ struct
     | `Int _ -> empty
     | `Float _ -> empty
     | `Thread _ -> empty (* thread IDs are abstract and nothing known can be reached from them *)
+    | `JmpBuf _ -> empty (* Jump buffers are abstract and nothing known can be reached from them *)
     | `Mutex -> empty (* mutexes are abstract and nothing known can be reached from them *)
 
   (* Get the list of addresses accessable immediately from a given address, thus
@@ -668,6 +669,7 @@ struct
         | `Int _ -> (empty, TS.bot (), false)
         | `Float _ -> (empty, TS.bot (), false)
         | `Thread _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
+        | `JmpBuf _ -> (empty, TS.bot (), false) (* TODO: is this right? *)
         | `Mutex -> (empty, TS.bot (), false) (* TODO: is this right? *)
       in
       reachable_from_value (get (Analyses.ask_of_ctx ctx) ctx.global ctx.local adr None)
@@ -1246,6 +1248,14 @@ struct
         let fs = eval_funvar ctx e in
         List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
       end
+    | Q.EvalJumpBuf e ->
+      (match eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
+       | `Address jmp_buf ->
+         begin match get (Analyses.ask_of_ctx ctx) ctx.global ctx.local jmp_buf None with
+           | `JmpBuf x -> x
+           | y -> failwith (Printf.sprintf "problem?! is %s" (VD.show y))
+         end
+       | _ -> failwith "problem?!");
     | Q.EvalInt e ->
       query_evalint (Analyses.ask_of_ctx ctx) ctx.global ctx.local e
     | Q.EvalLength e -> begin
@@ -1684,7 +1694,7 @@ struct
      | _ -> ()
     );
     match lval with (* this section ensure global variables contain bottom values of the proper type before setting them  *)
-    | (Var v, offs) when AD.is_definite lval_val && v.vglob ->
+    | (Var v, offs) when v.vglob ->
       (* Optimization: In case of simple integral types, we not need to evaluate the old value.
           v is not an allocated block, as v directly appears as a variable in the program;
           so no explicit check is required here (unlike in set) *)
@@ -2217,6 +2227,24 @@ struct
           st
       end
     | Assert { exp; refine; _ }, _ -> assert_fn ctx exp refine
+    | Setjmp { env; savesigs}, _ ->
+      (let st' = (match (eval_rv (Analyses.ask_of_ctx ctx) gs st env) with
+           | `Address jmp_buf ->
+             let controlctx = ControlSpecC.hash (ctx.control_context ()) in
+             let value = `JmpBuf (ValueDomain.JmpBufs.singleton (ctx.node, IntDomain.Flattened.of_int (Int64.of_int controlctx))) in
+             set ~ctx (Analyses.ask_of_ctx ctx) gs st jmp_buf (Cilfacade.typeOf env) value
+           | _      -> failwith "problem?!")
+       in
+       match lv with
+       | Some lv ->
+         set ~ctx (Analyses.ask_of_ctx ctx) gs st' (eval_lv (Analyses.ask_of_ctx ctx) ctx.global st lv) (Cilfacade.typeOfLval lv) (`Int (ID.of_int IInt BI.zero))
+       | None -> st')
+    | Longjmp {env; value; sigrestore}, _ ->
+      let rv = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local value in
+      let t = Cil.typeOf value in
+      let res = set ~ctx ~t_override:t (Analyses.ask_of_ctx ctx) ctx.global ctx.local (return_var ()) t rv in
+      res
+      (* Not rasing Deadode here, deadcode is raised at a higher level! *)
     | _, _ -> begin
         let st =
           special_unknown_invalidate ctx (Analyses.ask_of_ctx ctx) gs st f args

src/analyses/libraryDesc.ml

@@ -62,6 +62,8 @@ type special =
   | Strcpy of { dest: Cil.exp; src: Cil.exp } (* TODO: add count for strncpy when actually used *)
   | Abort
   | Identity of Cil.exp (** Identity function. Some compiler optimization annotation functions map to this. *)
+  | Setjmp of {env: Cil.exp; savesigs: Cil.exp; }
+  | Longjmp of {env: Cil.exp; value: Cil.exp; sigrestore: bool}
   | Unknown (** Anything not belonging to other types. *) (* TODO: rename to Other? *)
 
 

src/analyses/libraryFunctions.ml

@@ -44,6 +44,12 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("setbuf", unknown [drop "stream" [w]; drop "buf" [w]]);
     ("swprintf", unknown (drop "wcs" [w] :: drop "maxlen" [] :: drop "fmt" [r] :: VarArgs (drop' [])));
     ("assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" }); (* only used if assert is used without include, e.g. in transformed files *)
+    ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env; savesigs = Cil.zero }); (* only has one underscore *)
+    ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env; savesigs = Cil.zero });
+    ("__sigsetjmp", special [__ "env" [w]; __ "savesigs" []] @@ fun env savesigs -> Setjmp { env; savesigs }); (* has two underscores *)
+    ("sigsetjmp", special [__ "env" [w]; __ "savesigs" []] @@ fun env savesigs -> Setjmp { env; savesigs });
+    ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value; sigrestore = false });
+    ("siglongjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value; sigrestore = true });
   ]
 
 (** C POSIX library functions.

src/cdomains/jmpBufDomain.ml

@@ -0,0 +1,7 @@
+module BufferEntry = Printable.ProdSimple(Node)(IntDomain.Flattened)
+
+module JmpBufSet =
+struct
+  include SetDomain.ToppedSet (BufferEntry) (struct let topname = "All jumpbufs" end)
+  let name () = "Jumpbuffers"
+end

src/cdomains/valueDomain.ml

@@ -66,6 +66,7 @@ struct
 end
 
 module Threads = ConcDomain.ThreadSet
+module JmpBufs = JmpBufDomain.JmpBufSet
 
 module rec Compound: S with type t = [
     | `Top
@@ -77,6 +78,7 @@ module rec Compound: S with type t = [
     | `Array of CArrays.t
     | `Blob of Blobs.t
     | `Thread of Threads.t
+    | `JmpBuf of JmpBufs.t
     | `Mutex
     | `Bot
   ] and type offs = (fieldinfo,IndexDomain.t) Lval.offs =
@@ -91,6 +93,7 @@ struct
     | `Array of CArrays.t
     | `Blob of Blobs.t
     | `Thread of Threads.t
+    | `JmpBuf of JmpBufs.t
     | `Mutex
     | `Bot
   ] [@@deriving eq, ord, hash]
@@ -106,13 +109,18 @@ struct
     | TNamed ({tname = "pthread_t"; _}, _) -> true
     | _ -> false
 
+  let is_jmp_buf_type = function
+    | TNamed ({tname = "jmp_buf"; _}, _) -> true
+    | _ -> false
+
   let array_length_idx default length =
     let l = BatOption.bind length (fun e -> Cil.getInteger (Cil.constFold true e)) in
     BatOption.map_default (fun x-> IndexDomain.of_int (Cilfacade.ptrdiff_ikind ()) @@ Cilint.big_int_of_cilint x) default l
 
   let rec bot_value ?(varAttr=[]) (t: typ): t =
     match t with
     | _ when is_mutex_type t -> `Mutex
+    | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
     | TInt _ -> `Bot (*`Int (ID.bot ()) -- should be lower than any int or address*)
     | TFloat _ -> `Bot
     | TPtr _ -> `Address (AD.bot ())
@@ -123,6 +131,7 @@ struct
       let len = array_length_idx (IndexDomain.bot ()) length in
       `Array (CArrays.make ~varAttr ~typAttr len (bot_value ai))
     | t when is_thread_type t -> `Thread (ConcDomain.ThreadSet.empty ())
+    | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.empty ())
     | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t)
     | _ -> `Bot
 
@@ -136,13 +145,15 @@ struct
     | `Array x -> CArrays.is_bot x
     | `Blob x -> Blobs.is_bot x
     | `Thread x -> Threads.is_bot x
+    | `JmpBuf x -> JmpBufs.is_bot x
     | `Mutex -> true
     | `Bot -> true
     | `Top -> false
 
   let rec init_value ?(varAttr=[]) (t: typ): t = (* top_value is not used here because structs, blob etc will not contain the right members *)
     match t with
     | t when is_mutex_type t -> `Mutex
+    | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
     | TInt (ik,_) -> `Int (ID.top_of ik)
     | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.top_of fkind)
     | TPtr _ -> `Address AD.top_ptr
@@ -160,6 +171,7 @@ struct
   let rec top_value ?(varAttr=[]) (t: typ): t =
     match t with
     | _ when is_mutex_type t -> `Mutex
+    | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
     | TInt (ik,_) -> `Int (ID.(cast_to ik (top_of ik)))
     | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.top_of fkind)
     | TPtr _ -> `Address AD.top_ptr
@@ -183,13 +195,15 @@ struct
     | `Array x -> CArrays.is_top x
     | `Blob x -> Blobs.is_top x
     | `Thread x -> Threads.is_top x
+    | `JmpBuf x -> JmpBufs.is_top x
     | `Mutex -> true
     | `Top -> true
     | `Bot -> false
 
   let rec zero_init_value ?(varAttr=[]) (t:typ): t =
     match t with
     | _ when is_mutex_type t -> `Mutex
+    | t when is_jmp_buf_type t -> `JmpBuf (JmpBufs.top ())
     | TInt (ikind, _) -> `Int (ID.of_int ikind BI.zero)
     | TFloat ((FFloat | FDouble | FLongDouble as fkind), _) -> `Float (FD.of_const fkind 0.0)
     | TPtr _ -> `Address AD.null_ptr
@@ -213,7 +227,7 @@ struct
     | _ -> `Top
 
   let tag_name : t -> string = function
-    | `Top -> "Top" | `Int _ -> "Int" | `Float _ -> "Float" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Mutex -> "Mutex" | `Bot -> "Bot"
+    | `Top -> "Top" | `Int _ -> "Int" | `Float _ -> "Float" | `Address _ -> "Address" | `Struct _ -> "Struct" | `Union _ -> "Union" | `Array _ -> "Array" | `Blob _ -> "Blob" | `Thread _ -> "Thread" | `Mutex -> "Mutex" | `JmpBuf _ -> "JmpBuf" | `Bot -> "Bot"
 
   include Printable.Std
   let name () = "compound"
@@ -238,6 +252,7 @@ struct
     | `Array n ->  CArrays.pretty () n
     | `Blob n ->  Blobs.pretty () n
     | `Thread n -> Threads.pretty () n
+    | `JmpBuf n -> JmpBufs.pretty () n
     | `Mutex -> text "mutex"
     | `Bot -> text bot_name
     | `Top -> text top_name
@@ -252,6 +267,7 @@ struct
     | `Array n ->  CArrays.show n
     | `Blob n ->  Blobs.show n
     | `Thread n -> Threads.show n
+    | `JmpBuf n -> JmpBufs.show n
     | `Mutex -> "mutex"
     | `Bot -> bot_name
     | `Top -> top_name
@@ -266,6 +282,7 @@ struct
     | (`Array x, `Array y) -> CArrays.pretty_diff () (x,y)
     | (`Blob x, `Blob y) -> Blobs.pretty_diff () (x,y)
     | (`Thread x, `Thread y) -> Threads.pretty_diff () (x, y)
+    | (`JmpBuf x, `JmpBuf y) -> JmpBufs.pretty_diff () (x, y)
     | _ -> dprintf "%s: %a not same type as %a" (name ()) pretty x pretty y
 
   (************************************************************
@@ -371,7 +388,8 @@ struct
     match v with
     | `Bot
     | `Thread _
-    | `Mutex ->
+    | `Mutex
+    | `JmpBuf _ ->
       v
     | _ ->
       let log_top (_,l,_,_) = Messages.tracel "cast" "log_top at %d: %a to %a is top!\n" l pretty v d_type t in
@@ -457,7 +475,7 @@ struct
 
   let warn_type op x y =
     if GobConfig.get_bool "dbg.verbose" then
-      ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name x) (tag_name y) CilType.Location.pretty !Tracing.current_loc pretty x pretty y
+      ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y
 
   let rec leq x y =
     match (x,y) with
@@ -480,6 +498,7 @@ struct
     | (`Thread x, `Thread y) -> Threads.leq x y
     | (`Int x, `Thread y) -> true
     | (`Address x, `Thread y) -> true
+    | (`JmpBuf x, `JmpBuf y) -> JmpBufs.leq x y
     | (`Mutex, `Mutex) -> true
     | _ -> warn_type "leq" x y; false
 
@@ -512,6 +531,7 @@ struct
     | (`Address x, `Thread y)
     | (`Thread y, `Address x) ->
       `Thread y (* TODO: ignores address! *)
+    | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.join x y)
     | (`Mutex, `Mutex) -> `Mutex
     | _ ->
       warn_type "join" x y;
@@ -549,6 +569,7 @@ struct
     | (`Thread y, `Address x) ->
       `Thread y (* TODO: ignores address! *)
     | (`Mutex, `Mutex) -> `Mutex
+    | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.join x y)
     | _ ->
       warn_type "join" x y;
       `Top
@@ -640,7 +661,7 @@ struct
       warn_type "meet" x y;
       `Bot
 
-  let rec widen x y =
+  let rec widen (x:t) (y:t):t =
     match (x,y) with
     | (`Top, _) -> `Top
     | (_, `Top) -> `Top
@@ -662,6 +683,7 @@ struct
     | (`Array x, `Array y) -> `Array (CArrays.widen x y)
     | (`Blob x, `Blob y) -> `Blob (Blobs.widen x y)
     | (`Thread x, `Thread y) -> `Thread (Threads.widen x y)
+    | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.widen x y)
     | (`Int x, `Thread y)
     | (`Thread y, `Int x) ->
       `Thread y (* TODO: ignores int! *)
@@ -685,6 +707,7 @@ struct
     | (`Array x, `Array y) -> `Array (CArrays.narrow x y)
     | (`Blob x, `Blob y) -> `Blob (Blobs.narrow x y)
     | (`Thread x, `Thread y) -> `Thread (Threads.narrow x y)
+    | (`JmpBuf x, `JmpBuf y) -> `JmpBuf (JmpBufs.narrow x y)
     | (`Int x, `Thread y)
     | (`Thread y, `Int x) ->
       `Int x (* TODO: ignores thread! *)
@@ -958,6 +981,16 @@ struct
             else
               `Top
         end
+      | `JmpBuf _, _ ->
+        (* hack for pthread_t variables *)
+        begin match value with
+          | `JmpBuf t -> value (* if actually assigning thread, use value *)
+          | _ ->
+            if !GU.global_initialization then
+              `JmpBuf (JmpBufs.empty ()) (* if assigning global init (int on linux, ptr to struct on mac), use empty set instead *)
+            else
+              `Top
+        end
       | _ ->
       let result =
         match offs with
@@ -1128,6 +1161,7 @@ struct
     | `Array n ->  CArrays.printXml f n
     | `Blob n ->  Blobs.printXml f n
     | `Thread n -> Threads.printXml f n
+    | `JmpBuf n -> JmpBufs.printXml f n
     | `Mutex -> BatPrintf.fprintf f "<value>\n<data>\nmutex\n</data>\n</value>\n"
     | `Bot -> BatPrintf.fprintf f "<value>\n<data>\nbottom\n</data>\n</value>\n"
     | `Top -> BatPrintf.fprintf f "<value>\n<data>\ntop\n</data>\n</value>\n"
@@ -1141,6 +1175,7 @@ struct
     | `Array n -> CArrays.to_yojson n
     | `Blob n -> Blobs.to_yojson n
     | `Thread n -> Threads.to_yojson n
+    | `JmpBuf n -> JmpBufs.to_yojson n
     | `Mutex -> `String "mutex"
     | `Bot -> `String "⊥"
     | `Top -> `String "⊤"