Invalidate variables based on annotations of asm statements

src/analyses/base.ml

@@ -1899,34 +1899,34 @@ struct
     in
     List.concat_map do_exp exps
 
-  let invalidate ?ctx ask (gs:glob_fun) (st:store) (exps: exp list): store =
+  type invalidate_mode = InvalidateSelf | InvalidateTransitive | InvalidateSelfAndTransitive [@@deriving show]
+
+  let invalidate_core ~ctx inv_globs inv_exps =
+    let exps_transitive = List.filter_map (function (_, InvalidateSelf) -> None | (exp, _) -> Some exp) inv_exps in
+    let lvals_self = List.filter_map (function (_, InvalidateTransitive) -> None | (Lval lval, _) -> Some lval | _ -> None) inv_exps in
+    let exps_self = List.filter_map (function (_, InvalidateTransitive) | (Lval _, _) -> None | (exp, _) -> Some exp) inv_exps in
+    let exps_global = if inv_globs then foldGlobals !Cilfacade.current_file (fun acc global ->
+        match global with
+        | GVar (vi, _, _) when not (is_static vi) && not (BaseUtil.is_excluded_from_invalidation vi) ->
+          mkAddrOf (Var vi, NoOffset) :: acc
+        (* TODO: what about GVarDecl? *)
+        | _ -> acc
+      ) [] else [] in
+    let addr_list = collect_funargs (ask_of_ctx ctx) ctx.global ctx.local (exps_transitive @ exps_global) @ (List.map (eval_lv (ask_of_ctx ctx) ctx.global ctx.local) lvals_self) in
+    if M.tracing then (
+      M.trace "invalidate" "invalidate_core transitive: [%a]\n" (d_list "," CilType.Exp.pretty) exps_transitive;
+      M.trace "invalidate" "invalidate_core self (exp): [%a]\n" (d_list "," CilType.Exp.pretty) exps_self;
+      M.trace "invalidate" "invalidate_core self (lval): [%a]\n" (d_list "," CilType.Lval.pretty) lvals_self;
+      M.trace "invalidate" "invalidate_core global: [%a]\n" (d_list "," CilType.Exp.pretty) exps_global;
+    );
+    ctx.emit (Events.Invalidate {addr_list})
+
+
+  let invalidate ~ctx ask (gs:glob_fun) (st:store) (exps: exp list): store =
     if M.tracing && exps <> [] then M.tracel "invalidate" "Will invalidate expressions [%a]\n" (d_list ", " d_plainexp) exps;
     if exps <> [] then M.info ~category:Imprecise "Invalidating expressions: %a" (d_list ", " d_plainexp) exps;
-    (* To invalidate a single address, we create a pair with its corresponding
-     * top value. *)
-    let invalidate_address st a =
-      let t = AD.get_type a in
-      let v = get ask gs st a None in (* None here is ok, just causes us to be a bit less precise *)
-      let nv =  VD.invalidate_value ask t v in
-      (a, t, nv)
-    in
-    (* We define the function that invalidates all the values that an address
-     * expression e may point to *)
-    let invalidate_exp exps =
-      let args = collect_funargs ~warn:true ask gs st exps in
-      List.map (invalidate_address st) args
-    in
-    let invalids = invalidate_exp exps in
-    let is_fav_addr x =
-      List.exists BaseUtil.is_excluded_from_invalidation (AD.to_var_may x)
-    in
-    let invalids' = List.filter (fun (x,_,_) -> not (is_fav_addr x)) invalids in
-    if M.tracing && exps <> [] then (
-      let addrs = List.map (Tuple3.first) invalids' in
-      let vs = List.map (Tuple3.third) invalids' in
-      M.tracel "invalidate" "Setting addresses [%a] to values [%a]\n" (d_list ", " AD.pretty) addrs (d_list ", " VD.pretty) vs
-    );
-    set_many ?ctx ask gs st invalids'
+    invalidate_core ~ctx false (List.map (fun exp -> (exp, InvalidateTransitive)) exps);
+    ctx.local
 
 
   let make_entry ?(thread=false) (ctx:(D.t, G.t, C.t, V.t) Analyses.ctx) fundec args: D.t =
@@ -2083,23 +2083,11 @@ struct
   let special_unknown_invalidate ctx ask gs st f args =
     (if not (CilType.Varinfo.equal f dummyFunDec.svar) && not (LF.use_special f.vname) then M.error ~category:Imprecise ~tags:[Category Unsound] "Function definition missing for %s" f.vname);
     (if CilType.Varinfo.equal f dummyFunDec.svar then M.warn "Unknown function ptr called");
-    let addrs =
-      if get_bool "sem.unknown_function.invalidate.globals" then (
-        M.info ~category:Imprecise "INVALIDATING ALL GLOBALS!";
-        foldGlobals !Cilfacade.current_file (fun acc global ->
-            match global with
-            | GVar (vi, _, _) when not (is_static vi) ->
-              mkAddrOf (Var vi, NoOffset) :: acc
-            (* TODO: what about GVarDecl? *)
-            | _ -> acc
-          ) args
-      )
-      else
-        args
-    in
+    if get_bool "sem.unknown_function.invalidate.globals" then M.info ~category:Imprecise "INVALIDATING ALL GLOBALS!";
     (* TODO: what about escaped local variables? *)
     (* invalidate arguments and non-static globals for unknown functions *)
-    invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st addrs
+    invalidate_core ~ctx (get_bool "sem.unknown_function.invalidate.globals") (List.map (fun arg -> (arg, InvalidateTransitive)) args);
+    ctx.local
 
   let special ctx (lv:lval option) (f: varinfo) (args: exp list) =
     let invalidate_ret_lv st = match lv with
@@ -2413,8 +2401,27 @@ struct
     (* D.join ctx.local @@ *)
     ctx.local
 
+  let asm ctx _ an =
+    let inv_globs, inv_exps = match an with
+      | None ->
+        (* asm basic instruction *)
+        (not (get_bool "sem.asm.basic-preserve-globals"), [])
+      | Some (outs, ins, clobbers) ->
+        (* advanced asm instructions *)
+        (
+          List.mem "memory" clobbers && not (get_bool "sem.asm.memory-preserve-globals"),
+          List.append (if get_bool "sem.asm.readonly-inputs" then [] else List.map (fun (_, _, exp) -> exp, InvalidateTransitive) ins)
+            (List.map (fun (_, c, lval) -> Lval lval, match String.find c "+" with 
+               | _ -> InvalidateSelfAndTransitive
+               | exception Not_found -> InvalidateSelf) outs)
+        )
+    in
+    (if get_bool "sem.asm.enabled" then invalidate_core ~ctx inv_globs inv_exps);
+    ctx.local
+
   let event ctx e octx =
     let st: store = ctx.local in
+    let ask = ask_of_ctx ctx in
     match e with
     | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
       if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr;
@@ -2430,6 +2437,20 @@ struct
     | Events.AssignSpawnedThread (lval, tid) ->
       (* TODO: is this type right? *)
       set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (`Thread (ValueDomain.Threads.singleton tid))
+    | Events.Invalidate {addr_list} ->
+      let invalidate_address a =
+        let t = AD.get_type a in
+        let v = get ask ctx.global st a None in (* None here is ok, just causes us to be a bit less precise *)
+        let nv =  VD.invalidate_value ask t v in
+        (a, t, nv)
+      in
+      let invalids = List.map invalidate_address addr_list in
+      if M.tracing && addr_list <> [] then (
+        let addrs = List.map (Tuple3.first) invalids in
+        let vs = List.map (Tuple3.third) invalids in
+        M.tracel "invalidate" "Setting addresses [%a] to values [%a]\n" (d_list ", " AD.pretty) addrs (d_list ", " VD.pretty) vs
+      );
+      set_many ~ctx ask ctx.global ctx.local invalids
     | _ ->
       ctx.local
 end

src/analyses/mCP.ml

@@ -423,15 +423,15 @@ struct
     let d = do_emits ctx !emits d in
     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) t an =
     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' t an
     in
     let d, q = map_deadcode f @@ spec_list ctx.local in
     do_sideg ctx !sides;

src/domains/events.ml

@@ -9,6 +9,7 @@ type t =
   | AssignSpawnedThread of lval * ThreadIdDomain.Thread.t (** Assign spawned thread's ID to lval. *)
   | Access of {var_opt: CilType.Varinfo.t option; write: bool} (** Access varinfo (unknown if None). *)
   | Assign of {lval: CilType.Lval.t; exp: CilType.Exp.t} (** Used to simulate old [ctx.assign]. *)
+  | Invalidate of {addr_list: PreValueDomain.AD.bucket BatMap.Int.t list}
 
 let pretty () = function
   | Lock m -> dprintf "Lock %a" LockDomain.Lockset.Lock.pretty m
@@ -19,3 +20,4 @@ let pretty () = function
   | AssignSpawnedThread (lval, tid) -> dprintf "AssignSpawnedThread (%a, %a)" d_lval lval ThreadIdDomain.Thread.pretty tid
   | Access {var_opt; write} -> dprintf "Access {var_opt=%a, write=%B}" (docOpt (CilType.Varinfo.pretty ())) var_opt write
   | Assign {lval; exp} -> dprintf "Assugn {lval=%a, exp=%a}" CilType.Lval.pretty lval CilType.Exp.pretty exp
+  | Invalidate{addr_list} -> dprintf "Invalidate {addr_list=%a}" (docList (PreValueDomain.AD.pretty ())) addr_list

src/framework/analyses.ml

@@ -361,7 +361,7 @@ sig
   val body  : (D.t, G.t, C.t, V.t) ctx -> fundec -> D.t
   val return: (D.t, G.t, C.t, V.t) ctx -> exp option  -> fundec -> D.t
   val intrpt: (D.t, G.t, C.t, V.t) ctx -> D.t
-  val asm   : (D.t, G.t, C.t, V.t) ctx -> D.t
+  val asm   : (D.t, G.t, C.t, V.t) ctx -> string list -> (Edge.asm_out * Edge.asm_in * string list) option -> D.t
   val skip  : (D.t, G.t, C.t, V.t) ctx -> D.t
 
 
@@ -546,7 +546,7 @@ struct
 
   let vdecl ctx _ = ctx.local
 
-  let asm x =
+  let asm x t an =
     ignore (M.info ~category:Unsound "ASM statement ignored.");
     x.local (* Just ignore. *)
 

src/framework/cfgTools.ml

@@ -291,7 +291,8 @@ let createCFG (file: file) =
             let edge_of_instr = function
               | Set (lval,exp,loc,eloc) -> eloc, Assign (lval, exp) (* TODO: eloc loc fallback if unknown here and If *)
               | Call (lval,func,args,loc,eloc) -> eloc, Proc (lval,func,args)
-              | Asm (attr,tmpl,out,inp,regs,loc) -> loc, ASM (tmpl,out,inp)
+              | Asm (attr, tmpl, Some (out, inp, regs, gotos), loc) -> loc, ASM (tmpl, Some(out, inp, regs))
+              | Asm (attr, tmpl, None, loc) -> loc, ASM (tmpl, None)
               | VarDecl (v, loc) -> loc, VDecl(v)
             in
             let edges = List.map edge_of_instr instrs in

src/framework/constraints.ml

@@ -64,8 +64,8 @@ struct
   let intrpt ctx =
     D.lift @@ S.intrpt (conv ctx)
 
-  let asm ctx =
-    D.lift @@ S.asm (conv ctx)
+  let asm ctx t an =
+    D.lift @@ S.asm (conv ctx) t an
 
   let skip ctx =
     D.lift @@ S.skip (conv ctx)
@@ -231,7 +231,7 @@ struct
   let body ctx f      = lift_fun ctx (lift ctx) S.body   ((|>) f)
   let return ctx r f  = lift_fun ctx (lift ctx) S.return ((|>) f % (|>) r)
   let intrpt ctx      = lift_fun ctx (lift ctx) S.intrpt identity
-  let asm ctx         = lift_fun ctx (lift ctx) S.asm    identity
+  let asm ctx t an    = lift_fun ctx (lift ctx) S.asm    ((|>) an % (|>) t)
   let skip ctx        = lift_fun ctx (lift ctx) S.skip   identity
   let special ctx r f args        = lift_fun ctx (lift ctx) S.special ((|>) args % (|>) f % (|>) r)
   let combine' ctx r fe f args fc es = lift_fun ctx (lift ctx) S.combine (fun p -> p r fe f args fc (fst es))
@@ -358,7 +358,7 @@ struct
   let body ctx f      = lift_fun ctx S.body   ((|>) f)
   let return ctx r f  = lift_fun ctx S.return ((|>) f % (|>) r)
   let intrpt ctx      = lift_fun ctx S.intrpt identity
-  let asm ctx         = lift_fun ctx S.asm    identity
+  let asm ctx t an    = lift_fun ctx S.asm    ((|>) an % (|>) t)
   let skip ctx        = lift_fun ctx S.skip   identity
   let special ctx r f args       = lift_fun ctx S.special ((|>) args % (|>) f % (|>) r)
 
@@ -432,12 +432,12 @@ struct
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     lift_fun ctx identity S.query (fun (x) -> x q) (Queries.Result.bot q)
   let assign ctx lv e = lift_fun ctx D.lift   S.assign ((|>) e % (|>) lv) `Bot
-  let vdecl ctx v     = lift_fun ctx D.lift   S.vdecl  ((|>) v)            `Bot
+  let vdecl ctx v     = lift_fun ctx D.lift   S.vdecl  ((|>) v)           `Bot
   let branch ctx e tv = lift_fun ctx D.lift   S.branch ((|>) tv % (|>) e) `Bot
-  let body ctx f      = lift_fun ctx D.lift   S.body   ((|>) f)            `Bot
+  let body ctx f      = lift_fun ctx D.lift   S.body   ((|>) f)           `Bot
   let return ctx r f  = lift_fun ctx D.lift   S.return ((|>) f % (|>) r)  `Bot
-  let intrpt ctx      = lift_fun ctx D.lift   S.intrpt identity            `Bot
-  let asm ctx         = lift_fun ctx D.lift   S.asm    identity           `Bot
+  let intrpt ctx      = lift_fun ctx D.lift   S.intrpt identity           `Bot
+  let asm ctx t an    = lift_fun ctx D.lift   S.asm    ((|>) an % (|>) t) `Bot
   let skip ctx        = lift_fun ctx D.lift   S.skip   identity           `Bot
   let special ctx r f args       = lift_fun ctx D.lift S.special ((|>) args % (|>) f % (|>) r)        `Bot
   let combine ctx r fe f args fc es = lift_fun ctx D.lift S.combine (fun p -> p r fe f args fc (D.unlift es)) `Bot
@@ -659,9 +659,9 @@ struct
       let funs = List.map one_function functions in
       common_joins ctx funs !r !spawns
 
-  let tf_asm var edge prev_node getl sidel getg sideg d =
+  let tf_asm var edge prev_node t an getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
-    common_join ctx (S.asm ctx) !r !spawns
+    common_join ctx (S.asm ctx t an) !r !spawns
 
   let tf_skip var edge prev_node getl sidel getg sideg d =
     let ctx, r, spawns = common_ctx var edge prev_node d getl sidel getg sideg in
@@ -675,7 +675,7 @@ struct
       | Entry f        -> tf_entry var edge prev_node f
       | Ret (r,fd)     -> tf_ret var edge prev_node r fd
       | Test (p,b)     -> tf_test var edge prev_node p b
-      | ASM (_, _, _)  -> tf_asm var edge prev_node (* TODO: use ASM fields for something? *)
+      | ASM (t,an)     -> tf_asm var edge prev_node t an
       | Skip           -> tf_skip var edge prev_node
       | SelfLoop       -> tf_loop var edge prev_node
     end getl sidel getg sideg d
@@ -989,7 +989,7 @@ struct
   let return ctx e f    = map ctx Spec.return  (fun h -> h e f )
   let branch ctx e tv   = map ctx Spec.branch  (fun h -> h e tv)
   let intrpt ctx        = map ctx Spec.intrpt  identity
-  let asm ctx           = map ctx Spec.asm     identity
+  let asm ctx t an      = map ctx Spec.asm     (fun h -> h t an)
   let skip ctx          = map ctx Spec.skip    identity
   let special ctx l f a = map ctx Spec.special (fun h -> h l f a)
 

src/framework/edge.ml

@@ -18,9 +18,9 @@ type t =
     * transferred to the function node! *)
   | Test of CilType.Exp.t * bool
   (** The true-branch or false-branch of a conditional exp *)
-  | ASM of string list * asm_out * asm_in
+  | ASM of string list * (asm_out * asm_in * string list) option
   (** Inline assembly statements, and the annotations for output and input
-    * variables. *)
+    * variables and clobbers or None if it is an unannotated basic asm statement. *)
   | VDecl of CilType.Varinfo.t
   (** VDecl edge for the variable in varinfo. Whether such an edge is there for all
     * local variables or only when it is not possible to pull the declaration up, is
@@ -42,7 +42,7 @@ let pretty () = function
   | Entry (f) -> Pretty.text "(body)"
   | Ret (Some e,f) -> Pretty.dprintf "return %a" dn_exp e
   | Ret (None,f) -> Pretty.dprintf "return"
-  | ASM (_,_,_) -> Pretty.text "ASM ..."
+  | ASM _ -> Pretty.text "ASM ..."
   | Skip -> Pretty.text "skip"
   | VDecl v -> Cil.defaultCilPrinter#pVDecl () v
   | SelfLoop -> Pretty.text "SelfLoop"

src/framework/myCFG.ml

@@ -15,7 +15,7 @@ type edge = Edge.t =
   | Entry of CilType.Fundec.t
   | Ret of CilType.Exp.t option * CilType.Fundec.t
   | Test of CilType.Exp.t * bool
-  | ASM of string list * Edge.asm_out * Edge.asm_in
+  | ASM of string list * (Edge.asm_out * Edge.asm_in * string list) option
   | VDecl of CilType.Varinfo.t
   | Skip
   | SelfLoop

src/incremental/compareAST.ml

@@ -160,7 +160,8 @@ let eq_instr (a: instr) (b: instr) = match a, b with
   | Set (lv1, exp1, _l1, _el1), Set (lv2, exp2, _l2, _el2) -> eq_lval lv1 lv2 && eq_exp exp1 exp2
   | Call (Some lv1, f1, args1, _l1, _el1), Call (Some lv2, f2, args2, _l2, _el2) -> eq_lval lv1 lv2 && eq_exp f1 f2 && GobList.equal eq_exp args1 args2
   | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) -> eq_exp f1 f2 && GobList.equal eq_exp args1 args2
-  | Asm (attr1, tmp1, ci1, dj1, rk1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, l2) -> GobList.equal String.equal tmp1 tmp2 && GobList.equal(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_lval z1 z2) ci1 ci2 && GobList.equal(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_exp z1 z2) dj1 dj2 && GobList.equal String.equal rk1 rk2(* ignore attributes and locations *)
+  | Asm (_, tmp1, None, _), Asm (_, tmp2, None, _) -> GobList.equal String.equal tmp1 tmp2 (* ignore attributes and locations *)
+  | Asm (_, tmp1, Some (ci1, dj1, rk1, gt1), _), Asm (_, tmp2, Some (ci2, dj2, rk2, gt2), _) -> GobList.equal String.equal tmp1 tmp2 && GobList.equal(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_lval z1 z2) ci1 ci2 && GobList.equal(fun (x1,y1,z1) (x2,y2,z2)-> x1 = x2 && y1 = y2 && eq_exp z1 z2) dj1 dj2 && GobList.equal String.equal rk1 rk2 && GobList.equal String.equal gt1 gt2
   | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2
   | _, _ -> false
 

src/util/cilfacade.ml

@@ -478,7 +478,7 @@ class countFnVisitor = object
     method! vinst = function
       | Set (_,_,loc,_)
       | Call (_,_,_,loc,_)
-      | Asm (_,_,_,_,_,loc)
+      | Asm (_,_,_,loc)
         -> Hashtbl.replace locs loc.line (); SkipChildren
       | _ -> SkipChildren
 

src/util/options.schema.json

@@ -1108,6 +1108,38 @@
             }
           },
           "additionalProperties": false
+        },
+        "asm": {
+          "title": "sem.asm",
+          "description": "Inline Assembly Analysis options",
+          "type": "object",
+          "properties": {
+            "enabled": {
+              "title": "sem.asm.enabled",
+              "description": "",
+              "type": "boolean",
+              "default": true
+            },
+            "basic-preserve-globals": {
+              "title": "sem.asm.basic-preserve-globals",
+              "description": "If enabled, do preserve globals across basic asm statements",
+              "type": "boolean",
+              "default": false
+            },
+            "memory-preserve-globals": {
+              "title": "sem.asm.memory-preserve-globals",
+              "description": "If enabled, do preserve globals across advanced asm statements with memory clobber annotation",
+              "type": "boolean",
+              "default": false
+            },
+            "readonly-inputs": {
+              "title": "sem.asm.readonly-inputs",
+              "description": "If enabled, do not consider changes through pointers given as inputs",
+              "type": "boolean",
+              "default": false
+            }
+          },
+          "additionalProperties": false
         }
       },
       "additionalProperties": false

src/witness/witnessConstraints.ml

@@ -230,7 +230,7 @@ struct
   let return ctx e f    = map ctx Spec.return  (fun h -> h e f )
   let branch ctx e tv   = map ctx Spec.branch  (fun h -> h e tv)
   let intrpt ctx        = map ctx Spec.intrpt  identity
-  let asm ctx           = map ctx Spec.asm     identity
+  let asm ctx t an      = map ctx Spec.asm     (fun h -> h t an)
   let skip ctx          = map ctx Spec.skip    identity
   let special ctx l f a = map ctx Spec.special (fun h -> h l f a)
 

tests/regression/56-asm/01-parsing.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main()
+{
+  int x;
+
+  asm("nop");
+
+  asm volatile("");
+
+  assert(1);
+
+  return 0;
+}

tests/regression/56-asm/02-basic-discard-local.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+int main()
+{
+  int x = 0;
+
+  asm("nop");
+
+  assert(x == 0);
+
+  return 0;
+}