Support for inline assembler & goto instructions in inline assembler

goblint.opam.locked

@@ -131,6 +131,10 @@ post-messages: [
 ]
 # TODO: manually reordered to avoid opam pin crash: https://github.com/ocaml/opam/issues/4936
 pin-depends: [
+  [
+    "goblint-cil.2.0.3"
+    "git+https://github.com/N0W0RK/goblint-cil.git#second_try" 
+  ]
   [
     "ppx_deriving.5.2.1"
     "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6"

src/analyses/accessAnalysis.ml

@@ -25,8 +25,10 @@ struct
 
   let collect_local = ref false
   let emit_single_threaded = ref false
+  let ignore_asm = ref true
 
   let init _ =
+    ignore_asm := get_bool "asm_is_nop";
     collect_local := get_bool "witness.yaml.enabled" && get_bool "witness.invariant.accessed";
     let activated = get_string_list "ana.activated" in
     emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated
@@ -73,6 +75,17 @@ struct
       ctx.local
     end
 
+  let asm ctx outs ins =
+    if not !ignore_asm then begin
+      let handle_in exp = access_one_top ctx Read false exp in
+      List.iter handle_in ins;
+      (* deref needs to be set to true because we have to use AddrOf *)
+      let handle_out lval = access_one_top ~deref:true ctx Write false (AddrOf lval) in
+      List.iter handle_out outs;
+    end;
+    ctx.local
+
+
   let branch ctx exp tv : D.t =
     access_one_top ctx Read false exp;
     ctx.local

src/analyses/base.ml

@@ -82,6 +82,7 @@ struct
   let name () = "base"
   let startstate v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
   let exitstate  v: store = { cpa = CPA.bot (); deps = Dep.bot (); weak = WeakUpdates.bot (); priv = Priv.startstate ()}
+  let ignore_asm = ref true
 
   (**************************************************************************
    * Helpers
@@ -160,6 +161,7 @@ struct
     end;
     return_varstore := Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType;
     longjmp_return := Cilfacade.create_var @@ makeVarinfo false "LONGJMP_RETURN" intType;
+    ignore_asm := get_bool "asm_is_nop";
     Priv.init ()
 
   let finalize () =
@@ -1240,9 +1242,11 @@ struct
           if AD.mem Addr.UnknownPtr jmp_buf then
             M.warn ~category:Imprecise "Jump buffer %a may contain unknown pointers." d_exp e;
           begin match get ~ctx ~top:(VD.bot ()) ctx.local jmp_buf None with
-            | JmpBuf (x, copied) ->
+            | JmpBuf (x, copied, invalid) ->
               if copied then
                 M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a contains values that were copied here instead of being set by setjmp. This is Undefined Behavior." d_exp e;
+              if invalid then
+                M.warn ~category:(Behavior (Undefined Other)) "The jump buffer %a was modified by inline assembly. This is may lead to Undefined Behavior." d_exp e;
               x
             | Top
             | Bot ->
@@ -2582,7 +2586,7 @@ struct
     | Setjmp { env }, _ ->
       let st' = match eval_rv ~ctx st env with
         | Address jmp_buf ->
-          let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false) in
+          let value = VD.JmpBuf (ValueDomain.JmpBufs.Bufs.singleton (Target (ctx.prev_node, ctx.control_context ())), false, false) in
           let r = set ~ctx st jmp_buf (Cilfacade.typeOf env) value in
           if M.tracing then M.tracel "setjmp" "setting setjmp %a on %a -> %a\n" d_exp env D.pretty st D.pretty r;
           r
@@ -2898,6 +2902,11 @@ struct
     in
     D.join ctx.local e_d'
 
+  let asm ctx outs ins = 
+    if not !ignore_asm then
+      ctx.emit (Events.Invalidate {lvals=outs});
+    ctx.local
+
   let event ctx e octx =
     let ask = Analyses.ask_of_ctx ctx in
     let st: store = ctx.local in
@@ -2929,6 +2938,9 @@ struct
           {st' with cpa = CPA.remove !longjmp_return st'.cpa}
         | None -> ctx.local
       end
+    | Events.Invalidate {lvals} ->
+      let exps = List.map Cil.mkAddrOrStartOf lvals in
+      invalidate ~ctx st exps
     | _ ->
       ctx.local
 end

src/analyses/condVars.ml

@@ -101,6 +101,15 @@ struct
       of_expr true e >? of_lval >? of_clval |? Queries.Result.top q
     | _ -> Queries.Result.top q
 
+  let event ctx event octx = 
+    match event with
+    | Events.Invalidate {lvals} -> 
+      let mpts = List.map (fun lval -> mayPointTo ctx (AddrOf lval)) lvals in
+      let remove_mpt d mpt =
+        List.fold_left (fun d (v,o as k) -> D.remove k d |> D.remove_var v) d mpt in
+      List.fold_left remove_mpt ctx.local mpts
+    | _ -> ctx.local
+
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     (* remove all keys lval may point to, and all exprs that contain the variables (TODO precision) *)

src/analyses/deadlock.ml

@@ -40,6 +40,7 @@ struct
     let remove ctx l =
       let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
+
   end
 
   include LocksetAnalysis.MakeMay (Arg)

src/analyses/expsplit.ml

@@ -96,6 +96,15 @@ struct
       D.add exp value ctx.local
     | Longjmped _ ->
       emit_splits_ctx ctx
+    | Invalidate {lvals} ->
+      let handle_lval local lval =
+        let exp = Lval lval in
+        if D.mem exp local then
+          D.remove exp local
+        else
+          local
+      in
+      List.fold handle_lval ctx.local lvals
     | _ ->
       ctx.local
 end

src/analyses/locksetAnalysis.ml

@@ -1,6 +1,7 @@
 (** Basic lockset analyses. *)
 
 open Analyses
+open GoblintCil
 
 
 module type DS =
@@ -33,6 +34,20 @@ sig
   val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
 end
 
+let addr_set_of_lval (a: Queries.ask) lval =
+  let exp = Cil.mkAddrOrStartOf lval in
+  let addr_set = a.f (Queries.MayPointTo exp) in
+  addr_set
+
+let locks_of_lvals ctx lvals =
+  let ask = Analyses.ask_of_ctx ctx in
+  let collect_addr_sets locks lval = 
+    let addr_set = addr_set_of_lval ask lval in
+    ValueDomain.AD.union locks addr_set 
+  in
+  let addr_set = List.fold_left collect_addr_sets (ValueDomain.AD.empty ()) lvals in
+  ValueDomain.AD.elements addr_set
+
 module MakeMay (Arg: MayArg) =
 struct
   include Make (Arg.D)
@@ -60,6 +75,7 @@ module type MustArg =
 sig
   include MayArg
   val remove_all: (D.t, _, D.t, _) ctx -> D.t
+  val is_held: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> bool
 end
 
 module MakeMust (Arg: MustArg) =
@@ -82,6 +98,13 @@ struct
       Arg.remove_all ctx (* remove all locks *)
     | Events.Unlock l ->
       Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *)
+    | Events.Invalidate {lvals} ->
+      let locks = locks_of_lvals ctx lvals in
+      let is_held lock = Arg.is_held ctx lock in
+      let locks = List.filter is_held locks in
+      let remove_lock ctx lock = {ctx with local = Arg.remove ctx lock} in
+      let ctx = List.fold_left remove_lock ctx locks in
+      ctx.local
     | _ ->
       ctx.local
 end

src/analyses/mCP.ml

@@ -428,15 +428,15 @@ struct
     if q then raise Deadcode else d
 
 
-  let asm (ctx:(D.t, G.t, C.t, V.t) ctx) =
+  let asm (ctx:(D.t, G.t, C.t, V.t) ctx) outs ins =
     let spawns = ref [] in
     let splits = ref [] in
     let sides  = ref [] in
     let emits = ref [] in
     let ctx'' = outer_ctx "asm" ~spawns ~sides ~emits ctx in
     let f post_all (n,(module S:MCPSpec),d) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "asm" ~splits ~post_all ctx'' n d in
-      n, repr @@ S.asm ctx'
+      n, repr @@ S.asm ctx' outs ins
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;

src/analyses/mallocFresh.ml

@@ -29,6 +29,14 @@ struct
   let assign ctx lval rval =
     assign_lval (Analyses.ask_of_ctx ctx) lval ctx.local
 
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let handle_lval local lval = assign_lval ask lval local in
+      List.fold_left handle_lval ctx.local lvals
+    | _ -> ctx.local
+
   let combine_env ctx lval fexp f args fc au f_ask =
     ctx.local (* keep local as opposed to IdentitySpec *)
 

src/analyses/malloc_null.ml

@@ -6,6 +6,7 @@ module Offs = ValueDomain.Offs
 
 open GoblintCil
 open Analyses
+open GobConfig
 
 module Spec =
 struct
@@ -16,6 +17,21 @@ struct
   module C = ValueDomain.AddrSetDomain
   module P = IdentityP (D)
 
+  let name () = "malloc_null"
+
+  let return_addr_ = ref Addr.NullPtr
+  let return_addr () = !return_addr_
+
+  let startstate v = D.empty ()
+  let threadenter ctx ~multiple lval f args = [D.empty ()]
+  let threadspawn ctx ~multiple lval f args fctx = ctx.local
+  let exitstate  v = D.empty ()
+  let ignore_asm = ref true
+
+  let init marshal =
+    return_addr_ :=  Addr.of_var (Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType);
+    ignore_asm := get_bool "asm_is_nop"
+
   (*
     Addr set functions:
   *)
@@ -153,16 +169,22 @@ struct
       D.add (Addr.of_mval mval) ctx.local
     | _ -> ctx.local
 
+  let asm ctx outs ins =
+    if not !ignore_asm then begin
+      let handle_in exp = warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local exp in
+      List.iter handle_in ins;
+      let handle_out lval = warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local (Lval lval) in
+      List.iter handle_out outs;
+    end;
+    ctx.local
+
   let branch ctx (exp:exp) (tv:bool) : D.t =
     warn_deref_exp (Analyses.ask_of_ctx ctx) ctx.local exp;
     ctx.local
 
   let body ctx (f:fundec) : D.t =
     ctx.local
 
-  let return_addr_ = ref Addr.NullPtr
-  let return_addr () = !return_addr_
-
   let return ctx (exp:exp option) (f:fundec) : D.t =
     let remove_var x v = List.fold_right D.remove (to_addrs v) x in
     let nst = List.fold_left remove_var ctx.local (f.slocals @ f.sformals) in
@@ -212,15 +234,6 @@ struct
       end
     | _ -> ctx.local
 
-  let name () = "malloc_null"
-
-  let startstate v = D.empty ()
-  let threadenter ctx ~multiple lval f args = [D.empty ()]
-  let threadspawn ctx ~multiple lval f args fctx = ctx.local
-  let exitstate  v = D.empty ()
-
-  let init marshal =
-    return_addr_ :=  Addr.of_var (Cilfacade.create_var @@ makeVarinfo false "RETURN" voidType)
 end
 
 let _ =

src/analyses/memLeak.ml

@@ -216,9 +216,8 @@ struct
         | ad when (not (Queries.AD.is_top ad)) && Queries.AD.cardinal ad = 1 ->
           (* Note: Need to always set "ana.malloc.unique_address_count" to a value > 0 *)
           begin match Queries.AD.choose ad with
-            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) ->
-              ToppedVarInfoSet.remove v ctx.local
-            | _ -> ctx.local
+            | Queries.AD.Addr.Addr (v,_) when ctx.ask (Queries.IsAllocVar v) && ctx.ask (Queries.IsHeapVar v) && not @@ ctx.ask (Queries.IsMultiple v) -> ToppedVarInfoSet.remove v state
+            | _ -> state
           end
         | _ -> ctx.local
       end

src/analyses/mutexAnalysis.ml

@@ -154,10 +154,14 @@ struct
         (s', Multiplicity.increment (fst l) m)
       | _ -> (s', m)
 
+    let is_held ctx l =
+      let s, _ = ctx.local in
+      Lockset.mem (l, true) s || Lockset.mem(l, false) s
+
     let remove' ctx ~warn l =
       let s, m = ctx.local in
       let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
-      if warn &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
+      if warn && (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex (%a) which may not be held" Addr.pretty l;
       match Addr.to_mval l with
       | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
         let m',rmed = Multiplicity.decrement l m in

src/analyses/region.ml

@@ -75,6 +75,29 @@ struct
       | Some r when Lvals.is_empty r -> false
       | _ -> true
   end
+
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+        begin
+          match ctx.local with
+          | `Lifted reg ->
+            let old_regpart = ctx.global () in
+            let regpart, reg =
+              List.fold_left
+                (fun (regpart_acc, reg_acc) lval ->
+                  Reg.assign_bullet lval (regpart_acc, reg_acc)
+                )
+                (old_regpart, reg)
+                lvals
+            in
+            if not (RegPart.leq regpart old_regpart) then
+              ctx.sideg () regpart;
+            `Lifted reg
+          | _ -> ctx.local
+        end
+      | _ -> ctx.local
+
   let access ctx (a: Queries.access) =
     match a with
     | Point ->

src/analyses/symbLocks.ml

@@ -103,6 +103,13 @@ struct
       (* TODO: why doesn't invalidate_exp involve any reachable for deep write? *)
       List.fold_left (fun st e -> invalidate_exp (Analyses.ask_of_ctx ctx) e st) st write_args
 
+  let event ctx e octx =
+    match e with
+    | Events.Invalidate {lvals} ->
+      let ask = Analyses.ask_of_ctx ctx in
+      let invalidate local lval = invalidate_lval ask lval local in
+      List.fold_left invalidate ctx.local lvals
+    | _ -> ctx.local
 
   module A =
   struct

src/analyses/taintPartialContexts.ml

@@ -103,6 +103,18 @@ struct
 
 end
 
+let event ctx e octx =
+  match e with
+  | Events.Invalidate {lvals} ->
+    (* Handle the Invalidate event and update the tainted set *)
+    List.fold_left (fun acc lval ->
+      Spec.taint_lval ctx lval 
+    ) ctx.local lvals
+
+  | _ -> ctx.local
+
+
+
 let _ =
   MCP.register_analysis (module Spec : MCPSpec)
 

src/analyses/unassumeAnalysis.ml

@@ -304,7 +304,7 @@ struct
 
     emit_unassume {ctx with local = st} (* doesn't query, so no need to redefine ask *)
 
-  let asm ctx =
+  let asm ctx outs ins =
     emit_unassume ctx
 
   let skip ctx =