diff --git a/goblint.opam.locked b/goblint.opam.locked index b0a1c9ef20..d66084af78 100644 --- a/goblint.opam.locked +++ b/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" diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index efad8b4c2e..4e46f96b2a 100644 --- a/src/analyses/accessAnalysis.ml +++ b/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 diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 42e43b623a..ddaa88e04f 100644 --- a/src/analyses/base.ml +++ b/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 diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml index 3b23dc03fc..001aeac8d0 100644 --- a/src/analyses/condVars.ml +++ b/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) *) diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml index c23d6f4294..38aafef7a3 100644 --- a/src/analyses/deadlock.ml +++ b/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) diff --git a/src/analyses/expsplit.ml b/src/analyses/expsplit.ml index fef3d9ff9f..5758068eba 100644 --- a/src/analyses/expsplit.ml +++ b/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 diff --git a/src/analyses/locksetAnalysis.ml b/src/analyses/locksetAnalysis.ml index 6a816b9e6c..3582d147e1 100644 --- a/src/analyses/locksetAnalysis.ml +++ b/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 diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml index 50f6d5409b..f17ef5e7b4 100644 --- a/src/analyses/mCP.ml +++ b/src/analyses/mCP.ml @@ -428,7 +428,7 @@ 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 @@ -436,7 +436,7 @@ struct 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; diff --git a/src/analyses/mallocFresh.ml b/src/analyses/mallocFresh.ml index d1314d5009..0bc0c0e4c3 100644 --- a/src/analyses/mallocFresh.ml +++ b/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 *) diff --git a/src/analyses/malloc_null.ml b/src/analyses/malloc_null.ml index f993db0c6e..0946b9f544 100644 --- a/src/analyses/malloc_null.ml +++ b/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,6 +169,15 @@ 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 @@ -160,9 +185,6 @@ struct 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 _ = diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 456d434be7..707887f30e 100644 --- a/src/analyses/memLeak.ml +++ b/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 diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index a13c8d6bfd..9d8b3cf739 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/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 diff --git a/src/analyses/region.ml b/src/analyses/region.ml index a6ffa54ed6..63d716b06e 100644 --- a/src/analyses/region.ml +++ b/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 -> diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml index c237967a7a..e7214b2f32 100644 --- a/src/analyses/symbLocks.ml +++ b/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 diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml index 85dabd1c9d..606620e602 100644 --- a/src/analyses/taintPartialContexts.ml +++ b/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) diff --git a/src/analyses/unassumeAnalysis.ml b/src/analyses/unassumeAnalysis.ml index 5895f242c9..3939efa517 100644 --- a/src/analyses/unassumeAnalysis.ml +++ b/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 = diff --git a/src/analyses/uninit.ml b/src/analyses/uninit.ml index 8693599a4d..20043ad50d 100644 --- a/src/analyses/uninit.ml +++ b/src/analyses/uninit.ml @@ -7,6 +7,7 @@ module Offs = ValueDomain.Offs open GoblintCil open Analyses +open GobConfig module Spec = struct @@ -29,6 +30,11 @@ struct let threadspawn ctx ~multiple lval f args fctx = ctx.local let exitstate v : D.t = D.empty () + let ignore_asm = ref true + + let init _ = + ignore_asm := get_bool "asm_is_nop" + let access_address (ask: Queries.ask) write lv = match ask.f (Queries.MayPointTo (AddrOf lv)) with | ad when not (Queries.AD.is_top ad) -> @@ -223,6 +229,14 @@ struct ignore (is_expr_initd (Analyses.ask_of_ctx ctx) rval ctx.local); init_lval (Analyses.ask_of_ctx ctx) lval ctx.local + let asm ctx outs ins = + if not !ignore_asm then begin + let handle_in exp = ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local) in + List.iter handle_in ins; + let handle_out local lval = init_lval (Analyses.ask_of_ctx ctx) lval local in + List.fold_left handle_out ctx.local outs + end else ctx.local + let branch ctx (exp:exp) (tv:bool) : trans_out = ignore (is_expr_initd (Analyses.ask_of_ctx ctx) exp ctx.local); ctx.local diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index 69db6b4bfa..b29741bd21 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -4,6 +4,7 @@ open GoblintCil open Analyses open MessageCategory open AnalysisStateUtil +open GobConfig module AllocaVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All alloca() Variables" end) module HeapVars = SetDomain.ToppedSet(CilType.Varinfo)(struct let topname = "All Heap Variables" end) @@ -24,9 +25,12 @@ struct module G = ThreadIdToJoinedThreadsMap module V = VarinfoV - let context _ _ = () + let ignore_asm = ref true + let init _ = + ignore_asm := get_bool "asm_is_nop" + let context _ _ = () (* HELPER FUNCTIONS *) let get_current_threadid ctx = @@ -175,6 +179,15 @@ struct warn_exp_might_contain_freed "branch" ctx exp; ctx.local + let asm ctx outs ins = + if not !ignore_asm then begin + let handle_out lval = warn_lval_might_contain_freed "asm" ctx lval in + List.iter handle_out outs; + let handle_in exp = warn_exp_might_contain_freed "asm" ctx exp in + List.iter handle_in ins; + end; + ctx.local + let return ctx (exp:exp option) (f:fundec) : D.t = Option.iter (fun x -> warn_exp_might_contain_freed "return" ctx x) exp; ctx.local @@ -239,7 +252,6 @@ struct let startstate v = D.bot () let exitstate v = D.top () - end let _ = diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 30b36404af..01abc330ae 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -589,6 +589,10 @@ struct remove ask (Cil.var v) st in List.fold_left remove_var ctx.local (EscapeDomain.EscapedVars.elements vars) + | Events.Invalidate {lvals} -> + let ask = Analyses.ask_of_ctx ctx in + let remove_lval ctx lval = remove ask lval ctx in + List.fold_left remove_lval ctx.local lvals | _ -> ctx.local end diff --git a/src/cdomain/value/cdomains/jmpBufDomain.ml b/src/cdomain/value/cdomains/jmpBufDomain.ml index 3c94fa8f47..f2ef201c34 100644 --- a/src/cdomain/value/cdomains/jmpBufDomain.ml +++ b/src/cdomain/value/cdomains/jmpBufDomain.ml @@ -37,13 +37,14 @@ struct let meet = inter end -module JmpBufSetTaint = +module JmpBufSetTaintInvalid = struct module Bufs = JmpBufSet - include Lattice.Prod(JmpBufSet)(BoolDomain.MayBool) - let buffers (a,_) = a - let copied (_,b) = b - let name () = "JumpbufferCopyTaint" + include Lattice.Prod3(JmpBufSet)(BoolDomain.MayBool)(BoolDomain.MayBool) + let buffers (buffer,_,_) = buffer + let copied (_,copied,_) = copied + let invalid (_,_,invalid) = invalid + let name () = "JumpbufferTaintOrInvalid" end diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml index d748706ad1..3f42978167 100644 --- a/src/cdomain/value/cdomains/valueDomain.ml +++ b/src/cdomain/value/cdomains/valueDomain.ml @@ -79,7 +79,7 @@ struct end module Threads = ConcDomain.ThreadSet -module JmpBufs = JmpBufDomain.JmpBufSetTaint +module JmpBufs = JmpBufDomain.JmpBufSetTaintInvalid module rec Compound: sig type t = @@ -153,7 +153,7 @@ struct Array (CArrays.make ~varAttr ~typAttr len (bot_value ai)) | t when is_thread_type t -> Thread (ConcDomain.ThreadSet.empty ()) | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.bot ()) - | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false) + | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false, false) | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t) | _ -> Bot @@ -724,7 +724,7 @@ struct Array (CArrays.set ask n (array_idx_top) v) | t , Blob n -> Blob (Blobs.invalidate_value ask t n) | _ , Thread tid -> Thread (Threads.join (Threads.top ()) tid) - | _ , JmpBuf _ -> state (* TODO: no top jmpbuf *) + | _ , JmpBuf (b, c, _) -> JmpBuf(b, c, true) (* TODO: no top jmpbuf *) | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *) | t , _ -> top_value t @@ -1007,7 +1007,7 @@ struct | Blob(Bot, _, _) -> Bot (* TODO: Stopgap for malloced jmp_bufs, there is something fundamentally flawed somewhere *) | _ -> if !AnalysisState.global_initialization then - JmpBuf (JmpBufs.Bufs.empty (), false) (* if assigning global init, use empty set instead *) + JmpBuf (JmpBufs.Bufs.empty (), false, false) (* if assigning global init, use empty set instead *) else Top end @@ -1172,7 +1172,7 @@ struct let rec mark_jmpbufs_as_copied (v:t):t = match v with - | JmpBuf (v,t) -> JmpBuf (v, true) + | JmpBuf (v,t,i) -> JmpBuf (v, true, i) | Array n -> Array (CArrays.map (fun (x: t) -> mark_jmpbufs_as_copied x) n) | Struct n -> Struct (Structs.map (fun (x: t) -> mark_jmpbufs_as_copied x) n) | Union (f, n) -> Union (f, mark_jmpbufs_as_copied n) diff --git a/src/common/framework/cfgTools.ml b/src/common/framework/cfgTools.ml index d47f1efde0..dcc4cfa1e5 100644 --- a/src/common/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -213,7 +213,8 @@ let createCFG (file: file) = | Instr _ | If _ - | Return _ -> + | Return _ + | Asm _ -> stmt, visited_stmts | Continue _ @@ -291,7 +292,6 @@ let createCFG (file: file) = let edge_of_instr = function | Set (lval,exp,loc,eloc) -> Cilfacade.eloc_fallback ~eloc ~loc, Assign (lval, exp) | Call (lval,func,args,loc,eloc) -> Cilfacade.eloc_fallback ~eloc ~loc, Proc (lval,func,args) - | Asm (attr,tmpl,out,inp,regs,loc) -> loc, ASM (tmpl,out,inp) | VarDecl (v, loc) -> loc, VDecl(v) in let edges = List.map edge_of_instr instrs in @@ -374,6 +374,24 @@ let createCFG (file: file) = (* Nothing to do, find_real_stmt skips over these. *) () + | Asm (_, tmpls, outs, ins, _, labels, loc) -> + begin match real_succs () with + | [] -> failwith "MyCFG.createCFG: 0 Asm succ" + | [succ, skippedStatements] -> begin + addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, false)) (Statement succ); + if not (get_bool "asm_is_nop") then + let unique_dests = List.fold_left (fun acc label -> + let succ', skippedStatements' = find_real_stmt ~parent:stmt !label in + match List.assoc_opt succ' acc with + | None when succ' != succ -> (succ', skippedStatements') :: acc + | _ -> acc + ) [] labels in + List.iter (fun (succ, skippedStatements) -> + addEdge ~skippedStatements (Statement stmt) (loc, ASM(tmpls, outs, ins, true)) (Statement succ) + ) unique_dests; + end + | _ -> failwith "MyCFG.createCFG: >1 Asm succ" + end | Continue _ | Break _ | Switch _ -> @@ -382,6 +400,7 @@ let createCFG (file: file) = | ComputedGoto _ -> failwith "CfgTools.createCFG: unsupported stmt" + in Timing.wrap ~args:[("function", `String fd.svar.vname)] "handle" (List.iter handle) fd.sallstmts; diff --git a/src/common/framework/edge.ml b/src/common/framework/edge.ml index e6f214a4c8..8e66177bcb 100644 --- a/src/common/framework/edge.ml +++ b/src/common/framework/edge.ml @@ -21,9 +21,10 @@ 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 * bool (** Inline assembly statements, and the annotations for output and input - * variables. *) + * variables. The last field is a flag that indicates if this is an edge that + * was inserted because of asm goto labels. *) | 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 @@ -43,7 +44,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 @@ -91,7 +92,7 @@ let to_yojson e = ("function", CilType.Fundec.to_yojson function_); ("exp", [%to_yojson: CilType.Exp.t option] exp); ] - | ASM (instructions, output, input) -> + | ASM (instructions, output, input, _) -> [ ("type", `String "asm"); ("instructions", [%to_yojson: string list] instructions); diff --git a/src/common/framework/myCFG.ml b/src/common/framework/myCFG.ml index 76675f3c88..5a66d220db 100644 --- a/src/common/framework/myCFG.ml +++ b/src/common/framework/myCFG.ml @@ -17,7 +17,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 * bool | VDecl of CilType.Varinfo.t | Skip diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index d80ce49543..260f9524fa 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -480,13 +480,14 @@ class countFnVisitor = object | Switch (_,_,_,loc,_) | Loop (_,loc,_,_,_) -> Hashtbl.replace locs loc.line (); DoChildren + | Asm (_,_,_,_,_,_,loc) + -> Hashtbl.replace locs loc.line (); SkipChildren | _ -> DoChildren method! vinst = function | Set (_,_,loc,_) | Call (_,_,_,loc,_) - | Asm (_,_,_,_,_,loc) -> Hashtbl.replace locs loc.line (); SkipChildren | _ -> SkipChildren diff --git a/src/common/util/cilfacade0.ml b/src/common/util/cilfacade0.ml index 35fd5fb706..989d0bd316 100644 --- a/src/common/util/cilfacade0.ml +++ b/src/common/util/cilfacade0.ml @@ -29,7 +29,6 @@ let eloc_fallback ~eloc ~loc = let get_instrLoc = function | Set (_, _, loc, eloc) -> eloc_fallback ~eloc ~loc | Call (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc - | Asm (_, _, _, _, _, loc) -> loc | VarDecl (_, loc) -> loc (** Get expression location for [Cil.stmt]. *) @@ -51,3 +50,4 @@ let rec get_stmtLoc stmt = | Switch (_, _, _, loc, eloc) -> eloc_fallback ~eloc ~loc | Loop (_, loc, eloc, _, _) -> eloc_fallback ~eloc ~loc | Block {bstmts = hd :: _; _} -> get_stmtLoc hd + | Asm (_, _, _, _, _, _, loc) -> loc diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 0c83e342e0..fa01e7c655 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -17,6 +17,12 @@ "type": "string", "default": "" }, + "asm_is_nop": { + "title": "asm_is_nop", + "description": "Treat assembly statements as NOOP", + "type": "boolean", + "default": true + }, "justcil": { "title": "justcil", "description": "Just parse and output the CIL.", diff --git a/src/domains/events.ml b/src/domains/events.ml index 06561bddbe..375eb63236 100644 --- a/src/domains/events.ml +++ b/src/domains/events.ml @@ -16,6 +16,7 @@ type t = | Assert of exp | Unassume of {exp: CilType.Exp.t; uuids: string list} | Longjmped of {lval: CilType.Lval.t option} + | Invalidate of {lvals: CilType.Lval.t list} (** Should event be emitted after transfer function raises [Deadcode]? *) let emit_on_deadcode = function @@ -31,7 +32,8 @@ let emit_on_deadcode = function | UpdateExpSplit _ (* Pointless to split on dead. *) | Unassume _ (* Avoid spurious writes. *) | Assert _ (* Pointless to refine dead. *) - | Longjmped _ -> + | Longjmped _ + | Invalidate _ -> false let pretty () = function @@ -47,3 +49,4 @@ let pretty () = function | Assert exp -> dprintf "Assert %a" d_exp exp | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval + | Invalidate {lvals} -> dprintf "Invalidate {vars=%a}" (docList (d_lval ())) lvals diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml index 61f43cb1a5..44863ae062 100644 --- a/src/framework/analyses.ml +++ b/src/framework/analyses.ml @@ -177,7 +177,6 @@ let ctx_failwith s = raise (Ctx_failure s) (* TODO: use everywhere in ctx *) (** Convert [ctx] to [Queries.ask]. *) let ask_of_ctx ctx: Queries.ask = { Queries.f = ctx.ask } - module type Spec = sig module D : Lattice.S @@ -231,8 +230,9 @@ sig "return exp" or "return" in the passed function (fundec) *) val return: (D.t, G.t, C.t, V.t) ctx -> exp option -> fundec -> D.t - (** A transfer function meant to handle inline assembler program points *) - val asm : (D.t, G.t, C.t, V.t) ctx -> D.t + (** A transfer function meant to handle inline assembler program points. + It gets outputs (written by asm) and inputs (read by asm) as arguments. *) + val asm : (D.t, G.t, C.t, V.t) ctx -> lval list -> exp list -> D.t (** A transfer function which works as the identity function, i.e., it skips and does nothing. Used for empty loops. *) @@ -357,10 +357,12 @@ struct let vdecl ctx _ = ctx.local - let asm x = - M.msg_final Info ~category:Unsound "ASM ignored"; - M.info ~category:Unsound "ASM statement ignored."; - x.local (* Just ignore. *) + let asm ctx outs ins = + if get_bool "asm_is_nop" then begin + M.msg_final Info ~category:Unsound "ASM ignored"; + M.info ~category:Unsound "ASM statement ignored."; + end; + ctx.local let skip x = x.local (* Just ignore. *) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 84d7eff1ed..0b379221fc 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -71,8 +71,8 @@ struct let return ctx r f = D.lift @@ S.return (conv ctx) r f - let asm ctx = - D.lift @@ S.asm (conv ctx) + let asm ctx outs ins = + D.lift @@ S.asm (conv ctx) outs ins let skip ctx = D.lift @@ S.skip (conv ctx) @@ -155,8 +155,8 @@ struct let return ctx r f = S.return (conv ctx) r f - let asm ctx = - S.asm (conv ctx) + let asm ctx outs ins = + S.asm (conv ctx) outs ins let skip ctx = S.skip (conv ctx) @@ -244,13 +244,13 @@ struct let sync ctx reason = lift_fun ctx (lift ctx) S.sync ((|>) reason) let query' ctx (type a) (q: a Queries.t): a Queries.result = lift_fun ctx identity S.query (fun x -> x q) - let assign ctx lv e = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv) - let vdecl ctx v = lift_fun ctx (lift ctx) S.vdecl ((|>) v) - let branch ctx e tv = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e) - 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 asm ctx = lift_fun ctx (lift ctx) S.asm identity - let skip ctx = lift_fun ctx (lift ctx) S.skip identity + let assign ctx lv e = lift_fun ctx (lift ctx) S.assign ((|>) e % (|>) lv) + let vdecl ctx v = lift_fun ctx (lift ctx) S.vdecl ((|>) v) + let branch ctx e tv = lift_fun ctx (lift ctx) S.branch ((|>) tv % (|>) e) + 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 asm ctx outs ins = lift_fun ctx (lift ctx) S.asm ((|>) ins % (|>) outs) + 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_env' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_env (fun p -> p r fe f args fc (fst es) f_ask) let combine_assign' ctx r fe f args fc es f_ask = lift_fun ctx (lift ctx) S.combine_assign (fun p -> p r fe f args fc (fst es) f_ask) @@ -387,15 +387,15 @@ struct } let lift_fun ctx f g = g (f (conv ctx)), snd ctx.local - let sync ctx reason = lift_fun ctx S.sync ((|>) reason) - let query ctx = S.query (conv ctx) - let assign ctx lv e = lift_fun ctx S.assign ((|>) e % (|>) lv) - let vdecl ctx v = lift_fun ctx S.vdecl ((|>) v) - let branch ctx e tv = lift_fun ctx S.branch ((|>) tv % (|>) e) - let body ctx f = lift_fun ctx S.body ((|>) f) - let return ctx r f = lift_fun ctx S.return ((|>) f % (|>) r) - let asm ctx = lift_fun ctx S.asm identity - let skip ctx = lift_fun ctx S.skip identity + let sync ctx reason = lift_fun ctx S.sync ((|>) reason) + let query ctx = S.query (conv ctx) + let assign ctx lv e = lift_fun ctx S.assign ((|>) e % (|>) lv) + let vdecl ctx v = lift_fun ctx S.vdecl ((|>) v) + let branch ctx e tv = lift_fun ctx S.branch ((|>) tv % (|>) e) + let body ctx f = lift_fun ctx S.body ((|>) f) + let return ctx r f = lift_fun ctx S.return ((|>) f % (|>) r) + let asm ctx outs ins = lift_fun ctx S.asm ((|>) ins % (|>) outs) + let skip ctx = lift_fun ctx S.skip identity let special ctx r f args = lift_fun ctx S.special ((|>) args % (|>) f % (|>) r) let event ctx e octx = lift_fun ctx S.event ((|>) (conv octx) % (|>) e) @@ -480,13 +480,13 @@ 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 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 return ctx r f = lift_fun ctx D.lift S.return ((|>) f % (|>) r) `Bot - let asm ctx = lift_fun ctx D.lift S.asm identity `Bot - let skip ctx = lift_fun ctx D.lift S.skip identity `Bot + 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 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 return ctx r f = lift_fun ctx D.lift S.return ((|>) f % (|>) r) `Bot + let asm ctx outs ins = lift_fun ctx D.lift S.asm ((|>) ins % (|>) outs) `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_env ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx D.lift S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) `Bot @@ -765,9 +765,12 @@ struct end else 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 outs ins getl sidel getg sideg d = + let third (_, _, x) = x in + let outs = Util.list_map third outs in + let ins = Util.list_map third ins in 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 outs ins) !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 @@ -775,14 +778,14 @@ struct let tf var getl sidel getg sideg prev_node edge d = begin match edge with - | Assign (lv,rv) -> tf_assign var edge prev_node lv rv - | VDecl (v) -> tf_vdecl var edge prev_node v - | Proc (r,f,ars) -> tf_proc var edge prev_node r f ars - | 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? *) - | Skip -> tf_skip var edge prev_node + | Assign (lv,rv) -> tf_assign var edge prev_node lv rv + | VDecl (v) -> tf_vdecl var edge prev_node v + | Proc (r,f,ars) -> tf_proc var edge prev_node r f ars + | 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 (_, outs, ins,_) -> tf_asm var edge prev_node outs ins + | Skip -> tf_skip var edge prev_node end getl sidel getg sideg d type Goblint_backtrace.mark += TfLocation of location @@ -1098,7 +1101,7 @@ struct let body ctx f = map ctx Spec.body (fun h -> h f ) 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 asm ctx = map ctx Spec.asm identity + let asm ctx outs ins = map ctx Spec.asm (fun h -> h outs ins) let skip ctx = map ctx Spec.skip identity let special ctx l f a = map ctx Spec.special (fun h -> h l f a) @@ -1298,7 +1301,7 @@ struct let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx) let sync ctx = S.sync (conv ctx) let skip ctx = S.skip (conv ctx) - let asm ctx = S.asm (conv ctx) + let asm ctx outs ins = S.asm (conv ctx) outs ins let event ctx e octx = S.event (conv ctx) e (conv octx) end @@ -1540,7 +1543,7 @@ struct let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx) let sync ctx = S.sync (conv ctx) let skip ctx = S.skip (conv ctx) - let asm ctx = S.asm (conv ctx) + let asm ctx outs ins = S.asm (conv ctx) outs ins let event ctx e octx = S.event (conv ctx) e (conv octx) end @@ -1683,7 +1686,7 @@ struct let threadspawn ctx ~multiple lv f args fctx = S.threadspawn (conv ctx) ~multiple lv f args (conv fctx) let sync ctx = S.sync (conv ctx) let skip ctx = S.skip (conv ctx) - let asm ctx = S.asm (conv ctx) + let asm ctx outs ins = S.asm (conv ctx) outs ins let event ctx e octx = S.event (conv ctx) e (conv octx) end diff --git a/src/incremental/compareAST.ml b/src/incremental/compareAST.ml index c79735c2b1..e73e64a029 100644 --- a/src/incremental/compareAST.ml +++ b/src/incremental/compareAST.ml @@ -309,11 +309,6 @@ let eq_instr (a: instr) (b: instr) ~(rename_mapping: rename_mapping) = match a, eq_lval lv1 lv2 ~rename_mapping &&>> eq_exp f1 f2 &&>> forward_list_equal eq_exp args1 args2 | Call (None, f1, args1, _l1, _el1), Call (None, f2, args2, _l2, _el2) -> eq_exp f1 f2 ~rename_mapping &&>> forward_list_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, rename_mapping) &&>> - forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>> - forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&> - GobList.equal String.equal rk1 rk2(* ignore attributes and locations *) | VarDecl (v1, _l1), VarDecl (v2, _l2) -> eq_varinfo v1 v2 ~rename_mapping | _, _ -> false, rename_mapping @@ -351,6 +346,12 @@ let rec eq_stmtkind ?(cfg_comp = false) ((a, af): stmtkind * fundec) ((b, bf): s | Switch (exp1, block1, stmts1, _l1, _el1), Switch (exp2, block2, stmts2, _l2, _el2) -> if cfg_comp then failwith "CompareCFG: Invalid stmtkind in CFG" else eq_exp exp1 exp2 ~rename_mapping &&>> eq_block' block1 block2 &&>> forward_list_equal (fun a b -> eq_stmt (a,af) (b,bf)) stmts1 stmts2 | Loop (block1, _l1, _el1, _con1, _br1), Loop (block2, _l2, _el2, _con2, _br2) -> eq_block' block1 block2 ~rename_mapping | Block block1, Block block2 -> eq_block' block1 block2 ~rename_mapping + | Asm (attr1, tmp1, ci1, dj1, rk1, lb1, l1), Asm (attr2, tmp2, ci2, dj2, rk2, lb2, l2) -> + (GobList.equal String.equal tmp1 tmp2, rename_mapping) &&>> + forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_lval z1 z2) ci1 ci2 &&>> + forward_list_equal (fun (x1,y1,z1) (x2,y2,z2) ~rename_mapping:x-> (x1 = x2, x) &&> (y1 = y2) &&>> eq_exp z1 z2) dj1 dj2 &&> + GobList.equal String.equal rk1 rk2(* ignore attributes and locations *) &&> + GobList.equal (fun st1 st2 -> eq_stmt_with_location (!st1, af) (!st2, bf)) lb1 lb2 | _, _ -> false, rename_mapping and eq_stmt ?cfg_comp ((a, af): stmt * fundec) ((b, bf): stmt * fundec) ~(rename_mapping: rename_mapping) = diff --git a/src/transform/deadCode.ml b/src/transform/deadCode.ml index 1b9db8d06a..35744ba27f 100644 --- a/src/transform/deadCode.ml +++ b/src/transform/deadCode.ml @@ -72,7 +72,7 @@ let filter_map_block ?(unchecked_condition = Fun.const (GoblintCil.integer 1)) f let keep_block = impl_block b in if keep_stmt || keep_block then Some skind else None - | Instr _ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ as skind -> + | Instr _ | Return _ | Goto _ | ComputedGoto _ | Break _ | Continue _ | Asm _ as skind -> (* no further statements are contained recursively here, so nothing left to do *) if keep_stmt then Some skind else None @@ -91,7 +91,7 @@ let filter_map_block ?(unchecked_condition = Fun.const (GoblintCil.integer 1)) f (** Is it possible for this statement to begin executing normally, but not finish? *) let may_stop_execution stmt = match stmt.skind with - | Instr is -> List.exists (function Call _ | Asm _ -> true | _ -> false) is + | Instr is -> List.exists (function Call _ -> true | _ -> false) is | _ -> false (** Perform a depth first search over the CFG. Record the IDs of live statements; diff --git a/src/util/wideningTokens.ml b/src/util/wideningTokens.ml index 1816de90c7..d71ade1851 100644 --- a/src/util/wideningTokens.ml +++ b/src/util/wideningTokens.ml @@ -168,13 +168,13 @@ struct let query ctx (type a) (q: a Queries.t): a Queries.result = lift_fun ctx Fun.const S.query (fun (x) -> x q) - let assign ctx lv e = lift_fun ctx lift' S.assign ((|>) e % (|>) lv) - let vdecl ctx v = lift_fun ctx lift' S.vdecl ((|>) v) - let branch ctx e tv = lift_fun ctx lift' S.branch ((|>) tv % (|>) e) - let body ctx f = lift_fun ctx lift' S.body ((|>) f) - let return ctx r f = lift_fun ctx lift' S.return ((|>) f % (|>) r) - let asm ctx = lift_fun ctx lift' S.asm identity - let skip ctx = lift_fun ctx lift' S.skip identity + let assign ctx lv e = lift_fun ctx lift' S.assign ((|>) e % (|>) lv) + let vdecl ctx v = lift_fun ctx lift' S.vdecl ((|>) v) + let branch ctx e tv = lift_fun ctx lift' S.branch ((|>) tv % (|>) e) + let body ctx f = lift_fun ctx lift' S.body ((|>) f) + let return ctx r f = lift_fun ctx lift' S.return ((|>) f % (|>) r) + let asm ctx outs ins = lift_fun ctx lift' S.asm ((|>) ins % (|>) outs) + let skip ctx = lift_fun ctx lift' S.skip identity let special ctx r f args = lift_fun ctx lift' S.special ((|>) args % (|>) f % (|>) r) let combine_env ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_env (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *) let combine_assign ctx r fe f args fc es f_ask = lift_fun ctx lift' S.combine_assign (fun p -> p r fe f args fc (D.unlift es) f_ask) (* TODO: use tokens from es *) diff --git a/src/witness/witnessConstraints.ml b/src/witness/witnessConstraints.ml index 8dedf77a79..188819a7ef 100644 --- a/src/witness/witnessConstraints.ml +++ b/src/witness/witnessConstraints.ml @@ -189,7 +189,7 @@ struct let body ctx f = map ctx Spec.body (fun h -> h f ) 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 asm ctx = map ctx Spec.asm identity + let asm ctx outs ins = map ctx Spec.asm (fun h -> h outs ins) let skip ctx = map ctx Spec.skip identity let special ctx l f a = map ctx Spec.special (fun h -> h l f a) let event ctx e octx = map_event ctx e (* TODO: ???? *) diff --git a/tests/regression/65-taint/02-invalidate.c b/tests/regression/65-taint/02-invalidate.c index cf4636192f..1b0010118e 100644 --- a/tests/regression/65-taint/02-invalidate.c +++ b/tests/regression/65-taint/02-invalidate.c @@ -4,7 +4,7 @@ extern void unknown_fun (int *a); void mainfunct(int *rptr, int* uptr) { - unknown_fun(rptr); + unknown_fun(rptr); } int g; diff --git a/tests/regression/79-assembly/01-assembly-invalidate.c b/tests/regression/79-assembly/01-assembly-invalidate.c new file mode 100644 index 0000000000..7507a8075b --- /dev/null +++ b/tests/regression/79-assembly/01-assembly-invalidate.c @@ -0,0 +1,12 @@ +// PARAM: --set asm_is_nop false + +#include + +int main(void) { + + int v = 0; + + __asm__("nop": "=x"(v)); + + __goblint_assert(v==0); //UNKNOWN +} \ No newline at end of file diff --git a/tests/regression/79-assembly/02-assembly-precision.c b/tests/regression/79-assembly/02-assembly-precision.c new file mode 100644 index 0000000000..4b318a7cf3 --- /dev/null +++ b/tests/regression/79-assembly/02-assembly-precision.c @@ -0,0 +1,18 @@ +// PARAM: --set asm_is_nop false + +#include + +int main(void) { + + int r; + int v; + + __asm__ goto ("nop": : : : test); + + v = 0; + + test: + + __goblint_assert(v == 0); //UNKNOWN + +} \ No newline at end of file diff --git a/tests/regression/79-assembly/03-asm-use-after-free.c b/tests/regression/79-assembly/03-asm-use-after-free.c new file mode 100644 index 0000000000..47d57f92f6 --- /dev/null +++ b/tests/regression/79-assembly/03-asm-use-after-free.c @@ -0,0 +1,11 @@ +//PARAM: --set ana.activated[+] useAfterFree --disable asm_is_nop +#include + +int main(void) { + int *x = malloc(16); + free(x); + // write + asm ("nop" : "=x" (*x)); // WARN + // read + asm ("nop" : : "x" (*x)); // WARN +} diff --git a/tests/regression/79-assembly/04-asm-modified-since-setjmp.c b/tests/regression/79-assembly/04-asm-modified-since-setjmp.c new file mode 100644 index 0000000000..dcc6dedab7 --- /dev/null +++ b/tests/regression/79-assembly/04-asm-modified-since-setjmp.c @@ -0,0 +1,20 @@ +#include + +jmp_buf buf; + +int main(void) { + int x; +start: + x = 5; + if (setjmp(buf)) { + //read + asm ("nop" : : "x" (x)); + return 0; + } else { + //write + asm goto ("nop" : "=x" (x) : : : exit2, exit); //WARN + longjmp(buf, 1); + } +exit2: +exit: return 0; +} diff --git a/tests/regression/79-assembly/05-asm-var-eq.c b/tests/regression/79-assembly/05-asm-var-eq.c new file mode 100644 index 0000000000..ff53cbcb54 --- /dev/null +++ b/tests/regression/79-assembly/05-asm-var-eq.c @@ -0,0 +1,22 @@ +// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'" --disable asm_is_nop +#include +#include + +void not_ok(int x) { + int y = x; + asm ("nop" : "=x" (x)); + __goblint_check(x == y); // UNKNOWN +} + +void ok(int x) { + asm ("nop" : "=x" (x)); + int y = x; + __goblint_check(x == y); +} + +int main() { + int x; + scanf("%d", &x); + ok(x); + not_ok(x); +} diff --git a/tests/regression/79-assembly/06-asm-uninit.c b/tests/regression/79-assembly/06-asm-uninit.c new file mode 100644 index 0000000000..a02c6c4393 --- /dev/null +++ b/tests/regression/79-assembly/06-asm-uninit.c @@ -0,0 +1,8 @@ +// PARAM: --set ana.activated[+] uninit --disable asm_is_nop + +int main() { + int x, y, z; + asm ("nop" : "=x" (y) : "x" (x)); // WARN + z = y + 1; // NOWARN + return 0; +} diff --git a/tests/regression/79-assembly/07-asm-exp-split.c b/tests/regression/79-assembly/07-asm-exp-split.c new file mode 100644 index 0000000000..c686ee337f --- /dev/null +++ b/tests/regression/79-assembly/07-asm-exp-split.c @@ -0,0 +1,12 @@ +// PARAM: --set ana.activated[+] expsplit --disable asm_is_nop +#include + +int main(void) { + int r, x; + __goblint_split_begin(x); + x = r ? 1 : 0; + asm("nop" : "=x" (x), "=x" (r)); + __goblint_check(x == 0 || x == 1); // UNKNOWN (without asm it would be known) + __goblint_split_end(x); + __goblint_check(x == 0 || x == 1); // UNKNOWN +} diff --git a/tests/regression/79-assembly/08-asm-mutex.c b/tests/regression/79-assembly/08-asm-mutex.c new file mode 100644 index 0000000000..eefacbbb6f --- /dev/null +++ b/tests/regression/79-assembly/08-asm-mutex.c @@ -0,0 +1,14 @@ +// PARAM: --set ana.activated[+] mutexEvents --disable asm_is_nop +#include + +pthread_mutex_t mutex; + +int main() { + int x = 2; + pthread_mutex_init(&mutex, NULL); + pthread_mutex_lock(&mutex); + asm ("nop" : "=g" (mutex), "=x" (x)); + pthread_mutex_unlock(&mutex); // WARN + return 0; +} + diff --git a/tests/regression/79-assembly/09-asm-invalidate-condvar.c b/tests/regression/79-assembly/09-asm-invalidate-condvar.c new file mode 100644 index 0000000000..e6da610251 --- /dev/null +++ b/tests/regression/79-assembly/09-asm-invalidate-condvar.c @@ -0,0 +1,28 @@ +// PARAM: --set ana.activated[+] condvars --set ana.activated[+] taintPartialContexts --disable asm_is_nop +#include + +int glob; + +void f() { +} + +int main() { + int unk; + int tv; + if (unk) + glob = 0; + else + glob = 10; + + tv = (glob == 0); + f(); + + __asm__("nop": "=x"(glob): "x="(glob)); + + if (tv) + __goblint_assert(glob == 0); //UNKNOWN + else + __goblint_assert(glob != 0); //UNKNOWN + +} + diff --git a/tests/regression/79-assembly/10-asm-deadlock.c b/tests/regression/79-assembly/10-asm-deadlock.c new file mode 100644 index 0000000000..82cad87968 --- /dev/null +++ b/tests/regression/79-assembly/10-asm-deadlock.c @@ -0,0 +1,31 @@ +//PARAM: --set ana.activated[+] deadlock --disable asm_is_nop +#include +#include +#include + +pthread_mutex_t lock_a; +pthread_mutex_t lock_b; + +void *proc_a(void *arg) { + pthread_mutex_lock(&lock_a); + asm ("nop" : "=g" (lock_a)); + sleep(1); + pthread_mutex_lock(&lock_b); + pthread_exit(NULL); +} + +void *proc_b(void *arg) { + pthread_mutex_lock(&lock_b); + sleep(1); + pthread_mutex_lock(&lock_a); + return NULL; +} + +int main(void) { + int x; + pthread_t a, b; + pthread_create(&a, NULL, proc_a, NULL); + proc_b(NULL); + // this will remove lock_a from must_lockset + puts("no deadlock!"); +} diff --git a/tests/regression/79-assembly/11-asm-mem-leak.c b/tests/regression/79-assembly/11-asm-mem-leak.c new file mode 100644 index 0000000000..0ffbeb3c57 --- /dev/null +++ b/tests/regression/79-assembly/11-asm-mem-leak.c @@ -0,0 +1,23 @@ +//PARAM: --set ana.malloc.unique_address_count 1 --set ana.activated[+] memLeak --disable asm_is_nop +#include + +void ok(void) { + char *x = malloc(64); + char *y = x; + asm ("nop" : "=x" (x)); + free(y); + return; //NOWARN +} + +void not_ok(void) { + char *x = malloc(64); + asm ("nop" : "=x" (x)); + free(x); //WARN + return; +} + +int main(void) { + ok(); + not_ok(); + return 0; +} diff --git a/tests/regression/79-assembly/12-asm-taint.c b/tests/regression/79-assembly/12-asm-taint.c new file mode 100644 index 0000000000..cfdcf146a3 --- /dev/null +++ b/tests/regression/79-assembly/12-asm-taint.c @@ -0,0 +1,27 @@ +//PARAM --set "ana.activated[+]" taintPartialContexts --set ana.ctx_insens[+] base --disable asm_is_nop +#include + + +void mainfunct(int *rptr, int* uptr) { + asm("nop" : "=x"(*rptr)); +} + +int g; + +int main() { + int r, u; + + g = 1; + r = 1; + u = 1; + mainfunct(&r, &u); + + g = 2; + r = 2; + u = 2; + mainfunct(&r, &u); + + __goblint_check(g == 2); //UNKNOWN! + __goblint_check(r == 2); //UNKNOWN! + __goblint_check(u == 2); +} diff --git a/tests/regression/79-assembly/13-jmpbuf-invalid.c b/tests/regression/79-assembly/13-jmpbuf-invalid.c new file mode 100644 index 0000000000..5541e706e3 --- /dev/null +++ b/tests/regression/79-assembly/13-jmpbuf-invalid.c @@ -0,0 +1,14 @@ +// PARAM: --set asm_is_nop false +#include + +jmp_buf buf; + +int main(void) { + + if (!setjmp(buf)) { + + __asm__("nop" : "=m"(buf)); + + longjmp(buf, 1); //WARN + } +} \ No newline at end of file diff --git a/tests/regression/79-assembly/14-asm-region.c b/tests/regression/79-assembly/14-asm-region.c new file mode 100644 index 0000000000..64ffe469bb --- /dev/null +++ b/tests/regression/79-assembly/14-asm-region.c @@ -0,0 +1,13 @@ +//PARAM: --set ana.activated[+] region --disable asm_is_nop +#include + +int main() { + char *buffer = malloc(256); + buffer[0] = 'a'; + + + __asm__("movb $0, %0" : "=m" (*buffer)); + + free(buffer); + return 0; +} diff --git a/tests/regression/79-assembly/15-jumpbuf-poison.c b/tests/regression/79-assembly/15-jumpbuf-poison.c new file mode 100644 index 0000000000..e44474611f --- /dev/null +++ b/tests/regression/79-assembly/15-jumpbuf-poison.c @@ -0,0 +1,25 @@ +// PARAM: --disable asm_is_nop +#include +#include + +jmp_buf buf; + +void test(void) { + + longjmp(buf, 1); +} + +int main(void) { + + int i = 0; + + if (setjmp(buf)){ + + printf("After Jump: %d\n",i); //WARN + } else { + + printf("Setting i to 69; %d\n", i); + asm ("nop" : "=x"(i) : "=x"(i)); + test(); + } +} diff --git a/tests/regression/79-assembly/16-jumpbuf-read-poison.c b/tests/regression/79-assembly/16-jumpbuf-read-poison.c new file mode 100644 index 0000000000..8f409bf1de --- /dev/null +++ b/tests/regression/79-assembly/16-jumpbuf-read-poison.c @@ -0,0 +1,25 @@ +// PARAM: --disable asm_is_nop +#include +#include + +jmp_buf buf; + +void test(void) { + + longjmp(buf, 1); +} + +int main(void) { + + int i = 0; + + if (setjmp(buf)){ + + asm ("nop" : "x="(i):"x="(i)); //WARN + } else { + + printf("Setting i to 69; %d\n", i); + i = 10; + test(); + } +}