diff --git a/.github/workflows/locked.yml b/.github/workflows/locked.yml index b65ad0c7a3..a7488fa27f 100644 --- a/.github/workflows/locked.yml +++ b/.github/workflows/locked.yml @@ -56,6 +56,44 @@ jobs: - name: Test incremental regression run: ruby scripts/update_suite.rb -i + extraction: + strategy: + fail-fast: false + matrix: + os: + - ubuntu-latest + ocaml-compiler: + - 4.14.0 # matches opam lock file + # don't add any other because they won't be used + + runs-on: ${{ matrix.os }} + + steps: + - name: Checkout code + uses: actions/checkout@v3 + + - name: Set up OCaml ${{ matrix.ocaml-compiler }} + env: + # otherwise setup-ocaml pins non-locked dependencies + # https://github.com/ocaml/setup-ocaml/issues/166 + OPAMLOCKED: locked + uses: ocaml/setup-ocaml@v2 + with: + ocaml-compiler: ${{ matrix.ocaml-compiler }} + + - name: Install spin + run: sudo apt-get -y install spin + + - name: Install dependencies + run: opam install . --deps-only --locked --with-test + + - name: Build + run: ./make.sh nat + + - name: Test extraction + run: cd tests/extraction && ./test.sh + + gobview: strategy: fail-fast: false diff --git a/.gitignore b/.gitignore index 6759705fee..c77904c819 100644 --- a/.gitignore +++ b/.gitignore @@ -22,6 +22,7 @@ doclist.odocl autom4te.cache mytests result/* +pml-result/* tests/regression/*/goblint_temp linux-headers diff --git a/spin/pthread.base.pml b/spin/pthread.base.pml new file mode 100644 index 0000000000..789d0f3d95 --- /dev/null +++ b/spin/pthread.base.pml @@ -0,0 +1,305 @@ +// configuration defaults +#ifndef mutex_count +#define mutex_count 0 +#endif + +#ifndef cond_var_count +#define cond_var_count 0 +#endif + +// resources +mtype = {NONE, THREAD, MUTEX, COND_VAR} +typedef Resource { + mtype type = NONE; + byte id; +}; + +// threads +mtype = {NOTCREATED, READY, WAITING, DONE} // possible thread states + +typedef Thread { + mtype state = NOTCREATED; + chan waitQueue = [thread_count] of { byte } // threads waiting on thread_join + Resource waitingOnResource; +}; +Thread threads[thread_count]; + +#if mutex_count +mtype = {UNLOCKED, LOCKED} +typedef Mutex { + mtype state = UNLOCKED; + byte tid; + chan blockedQueue = [thread_count] of { byte, byte }; +}; +Mutex mutexes[mutex_count]; +#endif + +#if cond_var_count +typedef CondVar { + byte mid; + chan waitQueue = [thread_count] of { byte, byte }; +}; +CondVar cond_vars[cond_var_count]; +#endif + +// manage function calls at runtime to avoid inlining +// each proctype has its own: stack, sp +inline mark(pc) { + sp++; + stack[sp] = pc; +} + +// handle exit call in C programs +inline exit() { + atomic { + for (___i in threads) { + threads[___i].state = DONE; + } + } +} + +// helpers for scheduling etc. +#define notStarving(i) \ + (always(threads[i].state == READY implies always eventually(threads[i].state == READY || \ + threads[i].state == DONE))) + +// LTL formulas +ltl not_starving { allTasks(notStarving) } + +#define canRun(thread_id) (threads[thread_id].state == READY) + +#define isWaiting(thread_id, resource_type, resource_id) \ + (threads[thread_id].state == WAITING && \ + threads[thread_id].waitingOnResource.type == resource_type && \ + threads[thread_id].waitingOnResource.id == resource_id) + +//pragma mark - waiting signaling + +inline setWaiting(thread_id, resource_type, resource_id) { + printf("setWaiting: thread %d will wait for %e %d\n", thread_id, resource_type, + resource_id); + + // thread should not be waiting for anything at this point + assert(threads[thread_id].waitingOnResource.type == NONE); + + threads[thread_id].waitingOnResource.type = resource_type; + threads[thread_id].waitingOnResource.id = resource_id; + + // update process threads[tid].state (provided clause will block immediately) + threads[thread_id].state = WAITING; +} + +inline setReady(thread_id) { + printf("setReady: thread %d will be ready (was waiting for %e %d)\n", + thread_id, threads[thread_id].waitingOnResource.type, threads[thread_id].waitingOnResource.id); + + threads[thread_id].waitingOnResource.type = NONE; + threads[thread_id].state = READY; +} + +//pragma mark - Helper globals +byte ___i; +byte ___rand_num; + +//pragma mark - Thread logic + +inline ThreadCreate(thread_id) { + atomic { + printf("ThreadCreate: id %d\n", thread_id); + + setReady(thread_id); + } +} + +// pthread_join +inline ThreadWait(thread_id) { + atomic { + printf("ThreadWait: id %d\n", thread_id); + + if + :: threads[thread_id].state != DONE -> + threads[thread_id].waitQueue!tid; // should block here + setWaiting(tid, THREAD, thread_id); + :: threads[thread_id].state == DONE -> skip + fi + } +} + +// called by the functions invoked by pthread_create +// notify the caller, that the thread is done computing +// similar to conditional var broadcast +inline ThreadExit() { + atomic { + printf("ThreadBroadcast: id %d\n", tid); + assert(threads[tid].waitingOnResource.type == NONE); // thread should not be waiting for anything at this point + + do + :: nempty(threads[tid].waitQueue) -> + threads[tid].waitQueue?___i; // consume msg from queue + + assert(isWaiting(___i, THREAD, tid)); + printf("ThreadBroadcast: thread %d is waking up thread %d\n", tid, ___i); + + setReady(___i); + + :: empty(threads[tid].waitQueue) -> break + od + + threads[tid].state = DONE; + } +} + +//pragma mark - Mutex logic + +inline MutexInit(mid) { + atomic { + printf("MutexInit: id %d\n", mid); + } +} + +inline MutexLock(mid) { + __MutexLock(tid, mid) +} + +inline __MutexLock(thread_id, x) { + atomic { + if + :: mutexes[x].state == LOCKED -> // TODO: reentrant mutex? + printf("__MutexLock will block: mutexes[%d]\n", x); + + if + :: full(mutexes[x].blockedQueue) -> // TODO can this happen? + printf("FAIL: __MutexLock: queue is full\n"); + assert(false); + :: nfull(mutexes[x].blockedQueue) -> + printf("Thread %d put into queue for mutex %d\n", thread_id, x); + + select (___rand_num : 0..(thread_count - 1)); + + // put random number and tid in queue in a sorted way + // we do this in order to preserve POSIX semantics + // of random mutex awakaning on mutex_unlock + mutexes[x].blockedQueue!!___rand_num,thread_id; + fi; + + setWaiting(thread_id, MUTEX, x); // blocks this process instantly + // doc says: if stmt in atomic blocks, the rest will still remain atomic once it becomes executable. + // atomicity is lost if one jumps out of the sequence (which might be the case with provided (...)). + // revised: atomicity is broken if a statement inside the atomic blocks, but can continue as non-atomic + // so, atomic is broken after setWaiting, but that's ok since we're done with WaitSemaphore anyway + + :: mutexes[x].state == UNLOCKED -> + printf("__MutexLock locked: mutexes[%d] = LOCKED by %d\n", x, thread_id); + mutexes[x].state = LOCKED; + mutexes[x].tid = thread_id; + fi + } +} + +// This makes a strong assumption! If other threads are waiting for the mutex, they get it before we can attempt to +// relock the mutex. +// This is not really what happens for pthreads! +inline MutexUnlock(x) { + atomic { + if + :: mutexes[x].tid == tid -> + printf("MutexUnlock unlocked: mutexes[%d] = UNLOCKED by %d\n", x, tid); + mutexes[x].state = UNLOCKED; + + if + // wake up waiting process and reacquire the mutex + :: nempty(mutexes[x].blockedQueue) -> + printf("MutexUnlock: %d threads in queue for mutex %d\n", + len(mutexes[x].blockedQueue), x); + + mutexes[x].blockedQueue?_,___i; + printf("MutexUnlock: thread %d is waking up thread %d\n", tid, ___i); + + __MutexLock(___i, x); + setReady(___i); + + :: empty(mutexes[x].blockedQueue) -> skip + fi; + :: mutexes[x].tid != tid -> skip // undefined behavior + fi; + } +} + +//pragma mark - conditional vars + +inline CondVarInit(cond_var_id) { + atomic { + printf("CondVarInit: id %d\n", cond_var_id); + } +} + +inline CondVarWait(cond_var_id, mut_id) { + atomic { + printf("CondVarWait: id %d\n", cond_var_id); + + // if (me->tid != tid) failure("illegal wait"); + assert(mutexes[mut_id].tid == tid) + + cond_vars[cond_var_id].mid = mut_id + + // enqueue(cv->wq, tid); + + select (___rand_num : 0..(thread_count - 1)); + + // put random number and tid in queue in a sorted way + // we do this in order to preserve POSIX semantics + // of random cond var awakaning on signaling + + cond_vars[cond_var_id].waitQueue!!___rand_num,tid + + // unlock(me); + MutexUnlock(mut_id) + setWaiting(tid, COND_VAR, cond_var_id) + } +} + +inline CondVarSignal(cond_var_id) { + atomic { + if + // if there is a waiting process -> wake it up + :: nempty(cond_vars[cond_var_id].waitQueue) -> + printf("CondVarSignal: %d threads in queue for condition var %d\n", + len(cond_vars[cond_var_id].waitQueue), cond_var_id); + + cond_vars[cond_var_id].waitQueue?_,___i; + + assert(isWaiting(___i, COND_VAR, cond_var_id)); + printf("CondVarSignal: thread %d is waking up thread %d\n", tid, ___i); + + setReady(___i); + + // reacquire the mutex lock + __MutexLock(___i, cond_vars[cond_var_id].mid) + :: empty(cond_vars[cond_var_id].waitQueue) -> skip + fi; + } +} + +inline CondVarBroadcast(cond_var_id) { + atomic { + printf("CondVarSignal: %d threads in queue for condition var %d\n", + len(cond_vars[cond_var_id].waitQueue), cond_var_id); + + do + :: nempty(cond_vars[cond_var_id].waitQueue) -> + // consume random msg from queue + cond_vars[cond_var_id].waitQueue?_,___i; + + assert(isWaiting(___i, COND_VAR, cond_var_id)); + printf("CondVarSignal: thread %d is waking up thread %d\n", tid, ___i); + + setReady(___i); + // reacquire the mutex lock + __MutexLock(___i, cond_vars[cond_var_id].mid); + + :: empty(cond_vars[cond_var_id].waitQueue) -> break + od + + // All waiting processes/threads are now waiting for the mutex to be released + } +} diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml new file mode 100644 index 0000000000..3f34db17db --- /dev/null +++ b/src/analyses/extractPthread.ml @@ -0,0 +1,1283 @@ +(** Tracking of pthread lib code. Output to promela. *) + +open Prelude.Ana +open Analyses +open Cil +open BatteriesExceptionless +open Option.Infix +open PthreadDomain + +class uniqueVarPrinterClass = + object (self) + inherit defaultCilPrinterClass as super + + method! pVar (v : varinfo) = + text v.vname ++ chr '_' ++ text (string_of_int v.vid) + + method! pExp () = + function + | Const (CInt (i, _, _)) -> + (* Fix the constants with long/unsigned suffixes, e.g. 1LL *) + text @@ string_of_int @@ Z.to_int i + | x -> + super#pExp () x + end + +let printer = new uniqueVarPrinterClass + +(* Typealiases for better readability *) + +type thread_id = int + +type thread_name = string + +type mutex_id = int + +type mutex_name = string + +type cond_var_id = int + +type cond_var_name = string + +type fun_name = string + +module Resource = struct + type resource_type = + | Thread + | Function + [@@deriving show] + + type resource_name = string + + type t = resource_type * resource_name + + let make t n : t = (t, n) + + let res_type = fst + + let res_name = snd + + let show t = + let str_res_type = show_resource_type @@ res_type t in + let str_res_name = res_name t in + str_res_type ^ ":" ^ str_res_name +end + +module Action = struct + type thread = + { tid : thread_id + ; f : varinfo (** a function being called *) + } + + type cond_wait = + { cond_var_id : cond_var_id + ; mid : mutex_id + } + + (** uniquely identifies the function call + ** created/defined by `fun_ctx` function *) + type fun_call_id = string + + (** ADT of all possible edge actions types *) + type t = + | Call of fun_call_id + | Assign of string * string + | Cond of string (* pred *) + | ThreadCreate of thread + | ThreadJoin of thread_id + | ThreadExit + | MutexInit of mutex_id + | MutexLock of mutex_id + | MutexUnlock of mutex_id + | CondVarInit of cond_var_id + | CondVarBroadcast of cond_var_id + | CondVarSignal of cond_var_id + | CondVarWait of cond_wait + | Nop +end + +(** type of a node in CFG *) +type node = PthreadDomain.Pred.Base.t + +(** type of a single edge in CFG *) +type edge = node * Action.t * node + +module Tbls = struct + module type SymTblGen = sig + type k + + type v + + val make_new_val : (k, v) Hashtbl.t -> k -> v + end + + module type TblGen = sig + type k + + type v + end + + module SymTbl (G : SymTblGen) = struct + let table = (Hashtbl.create 123 : (G.k, G.v) Hashtbl.t) + + let get k = + (* in case there is no value for the key, populate the table with the next value (id) *) + let new_value_thunk () = + let new_val = G.make_new_val table k in + Hashtbl.replace table k new_val ; + new_val + in + Hashtbl.find table k |> Option.default_delayed new_value_thunk + + + let get_key v = + table |> Hashtbl.filter (( = ) v) |> Hashtbl.keys |> Enum.get + + + let to_list () = table |> Hashtbl.enum |> List.of_enum + end + + module Tbl (G : TblGen) = struct + let table = (Hashtbl.create 123 : (G.k, G.v) Hashtbl.t) + + let add k v = Hashtbl.replace table k v + + let get k = Hashtbl.find table k + + let get_key v = table |> Hashtbl.enum |> List.of_enum |> List.assoc_inv v + end + + let all_keys_count table = + table |> Hashtbl.keys |> List.of_enum |> List.length + + + module ThreadTidTbl = SymTbl (struct + type k = thread_name + + type v = thread_id + + let make_new_val table k = all_keys_count table + end) + + module FunNameToTids = struct + include Tbl (struct + type k = fun_name + + type v = thread_id Set.t + end) + + let extend k v = Hashtbl.modify_def Set.empty k (Set.add v) table + + let get_fun_for_tid v = + Hashtbl.keys table + |> List.of_enum + |> List.find (fun k -> + Option.get @@ Hashtbl.find table k |> Set.exists (( = ) v)) + end + + module MutexMidTbl = SymTbl (struct + type k = mutex_name + + type v = mutex_id + + let make_new_val table k = all_keys_count table + end) + + module CondVarIdTbl = SymTbl (struct + type k = cond_var_name + + type v = cond_var_id + + let make_new_val table k = all_keys_count table + end) + + (* context hash to differentiate function calls *) + module CtxTbl = SymTbl (struct + type k = int + + type v = int + + let make_new_val table k = all_keys_count table + end) + + module FunCallTbl = SymTbl (struct + type k = fun_name * string (* fun and target label *) + + type v = int + + let make_new_val table k = all_keys_count table + end) + + module NodeTbl = SymTbl (struct + (* table from sum type to negative line number for new intermediate node (-1 to -4 have special meanings) *) + type k = int (* stmt sid *) + + type v = MyCFG.node + + (* function for creating a new intermediate node (will generate a new sid every time!) *) + let make_new_val table k = + (* TODO: all same key occurrences instead *) + let line = -5 - all_keys_count table in + let loc = { !Tracing.current_loc with line } in + MyCFG.Statement + { (mkStmtOneInstr @@ Set (var dummyFunDec.svar, zero, loc, loc)) with + sid = new_sid () + } + end) +end + +let promela_main : fun_name = "mainfun" + +(* assign tid: promela_main -> 0 *) +let _ = Tbls.ThreadTidTbl.get promela_main + +let fun_ctx ctx f = + let ctx_hash = + match PthreadDomain.Ctx.to_int ctx with + | Some i -> + i |> i64_to_int |> Tbls.CtxTbl.get |> string_of_int + | None -> + "TOP" + in + f.vname ^ "_" ^ ctx_hash + + +module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (PthreadDomain.D)) +module rec Env : sig + type t + + val get : (PthreadDomain.D.t, Tasks.t, PthreadDomain.D.t, _) ctx -> t + + val d : t -> PthreadDomain.D.t + + val node : t -> MyCFG.node + + val resource : t -> Resource.t +end = struct + type t = + { d : PthreadDomain.D.t + ; node : MyCFG.node + ; resource : Resource.t + } + + let get ctx = + let d : PthreadDomain.D.t = ctx.local in + let node = Option.get !MyCFG.current_node in + let fundec = Node.find_fundec node in + let thread_name = + let cur_tid = + Int64.to_int @@ Option.get @@ PthreadDomain.Tid.to_int d.tid + in + Option.get @@ Tbls.ThreadTidTbl.get_key cur_tid + in + let resource = + let is_main_fun = + promela_main + |> GobConfig.get_string_list + |> List.mem fundec.svar.vname + in + let is_thread_fun = + let fun_of_thread = Edges.fun_for_thread thread_name in + Some fundec.svar = fun_of_thread + in + let open Resource in + if is_thread_fun || is_main_fun + then Resource.make Thread thread_name + else Resource.make Function (fun_ctx d.ctx fundec.svar) + in + { d; node; resource } + + + let d env = env.d + + let node env = env.node + + let resource env = env.resource +end + +and Edges : sig + val table : (Resource.t, edge Set.t) Hashtbl.t + + val add : ?dst:Node.t -> ?d:PthreadDomain.D.t -> Env.t -> Action.t -> unit + + val get : Resource.t -> edge Set.t + + val filter_map_actions : (Action.t -> 'a option) -> 'a list + + val fun_for_thread : thread_name -> varinfo option +end = struct + let table = Hashtbl.create 199 + + (** [add] adds an edge for the current environment resource id (Thread or Function) + ** [dst] destination node + ** [d] domain + ** [env] environment + ** [action] edge action of type `Action.t` *) + let add ?dst ?d env action = + let open PthreadDomain in + let preds = + let env_d = Env.d env in + (d |? env_d).pred + in + let add_edge_for_node node = + let env_node = Env.node env in + let env_res = Env.resource env in + let action_edge = (node, action, Node.location (dst |? env_node)) in + Hashtbl.modify_def Set.empty env_res (Set.add action_edge) table + in + Pred.iter add_edge_for_node preds + + + let get res_id = Hashtbl.find_default table res_id Set.empty + + let filter_map_actions f = + let action_of_edge (_, action, _) = action in + let all_edges = + table + |> Hashtbl.values + |> List.of_enum + |> List.map Set.elements + |> List.concat + in + List.filter_map (f % action_of_edge) all_edges + + + let fun_for_thread thread_name = + let open Action in + let get_funs = function + | ThreadCreate t when Tbls.ThreadTidTbl.get_key t.tid = Some thread_name + -> + Some t.f + | _ -> + None + in + List.hd @@ filter_map_actions get_funs +end + +module Variable = struct + type t = varinfo + + let is_integral v = match v.vtype with TInt _ -> true | _ -> false + + let is_global v = v.vglob + + let is_mem v = v.vaddrof + + let make_from_lhost = function + | Var v when is_integral v && not (is_mem v) -> + Some v + | _ -> + None + + + let make_from_lval (lhost, _) = make_from_lhost lhost + + let show = sprint (fun () -> printer#pVar) + + let show_def v = "int " ^ show v ^ ";" +end + +module Variables = struct + type var_state = + | Top of Variable.t + | Var of Variable.t + + let table = ref (Hashtbl.create 123 : (thread_id, var_state Set.t) Hashtbl.t) + + let get_globals () = + Hashtbl.values !table + |> List.of_enum + |> List.map Set.elements + |> List.flatten + |> List.filter_map (function + | Var v when Variable.is_global v -> + Some v + | Top v when Variable.is_global v -> + Some v + | _ -> + None) + |> List.unique + + + let get_locals tid = + Hashtbl.find !table tid + |> Option.default Set.empty + |> Set.filter_map (function + (* no globals *) + | Var v when not (Variable.is_global v) -> + Some v + | Top v when not (Variable.is_global v) -> + Some v + | _ -> + None) + |> Set.enum + |> List.of_enum + + + let is_top tid var = + let contains_top_of s = Set.exists (function Top x -> x.vid = var.vid | _ -> false) s in + if Variable.is_global var + then + !table + |> Hashtbl.values + |> List.of_enum + |> List.exists contains_top_of + else + contains_top_of @@ Hashtbl.find_default !table tid Set.empty + + + let add tid var = + if not (is_top tid var) + then Hashtbl.modify_def Set.empty tid (Set.add (Var var)) !table + + + let add_top tid var = + Hashtbl.modify_def Set.empty tid (Set.remove (Var var)) !table ; + Hashtbl.modify_def Set.empty tid (Set.add (Top var)) !table + + + (* is a local var for thread tid or a global + * var must not be set to top *) + let valid_var tid var = + let contains_var_of s = Set.exists (function Var x -> x.vid = var.vid | _ -> false) s in + if Variable.is_global var + then + !table + |> Hashtbl.values + |> List.of_enum + |> List.exists contains_var_of + else + contains_var_of @@ Hashtbl.find_default !table tid Set.empty + + + (* all vars on rhs should be already registered, otherwise -> do not add this var *) + let rec all_vars_are_valid ctx = function + | Const _ -> + true + | Lval l -> + let open PthreadDomain in + let d = Env.d @@ Env.get ctx in + let tid = Int64.to_int @@ Option.get @@ Tid.to_int d.tid in + + l + |> Variable.make_from_lval + |> Option.map @@ valid_var tid + |> Option.default false + | UnOp (_, e, _) -> + all_vars_are_valid ctx e + | BinOp (_, a, b, _) -> + all_vars_are_valid ctx a && all_vars_are_valid ctx b + | _ -> + false +end + +(** promela source code *) +type promela_src = string + +module Codegen = struct + (** [PmlResTbl] module maps resources to unique ids used as prefix for edge labeling *) + module PmlResTbl = struct + module FunTbl = Tbls.SymTbl (struct + type k = fun_name + + type v = int + + let make_new_val table k = Tbls.all_keys_count table + end) + + let get res = + let prefix = + if Resource.res_type res = Resource.Thread then "T" else "F" + in + let id = + match res with + | Resource.Thread, thread_name -> + Tbls.ThreadTidTbl.get thread_name + | Resource.Function, fun_name -> + FunTbl.get fun_name + in + prefix ^ string_of_int id + end + + module AdjacencyMatrix = struct + module HashtblN = Hashtbl.Make (PthreadDomain.Pred.Base) + + let make () = HashtblN.create 97 + + (** build adjacency matrix for all nodes of this process *) + let populate a2bs edges = + Set.iter + (fun ((a, _, _) as edge) -> + HashtblN.modify_def Set.empty a (Set.add edge) a2bs) + edges ; + a2bs + + + let nodes a2bs = HashtblN.keys a2bs |> List.of_enum + + let items a2bs = HashtblN.enum a2bs |> List.of_enum + + let in_edges a2bs node = + let get_b (_, _, b) = b in + HashtblN.filter (Set.mem node % Set.map get_b) a2bs + |> HashtblN.values + |> List.of_enum + |> List.concat_map Set.elements + + + let out_edges a2bs node = + try HashtblN.find a2bs node |> Set.elements with Not_found -> [] + end + + module Action = struct + include Action + + let extract_thread_create = function ThreadCreate x -> Some x | _ -> None + + let to_pml = function + | Call fname -> + "goto Fun_" ^ fname ^ ";" + | Assign (a, b) -> + a ^ " = " ^ b ^ ";" + | Cond cond -> + cond ^ " -> " + | ThreadCreate t -> + "ThreadCreate(" ^ string_of_int t.tid ^ ");" + | ThreadJoin tid -> + "ThreadWait(" ^ string_of_int tid ^ ");" + | ThreadExit -> + "ThreadExit();" + | MutexInit mid -> + "MutexInit(" ^ string_of_int mid ^ ");" + | MutexLock mid -> + "MutexLock(" ^ string_of_int mid ^ ");" + | MutexUnlock mid -> + "MutexUnlock(" ^ string_of_int mid ^ ");" + | CondVarInit id -> + "CondVarInit(" ^ string_of_int id ^ ");" + | CondVarBroadcast id -> + "CondVarBroadcast(" ^ string_of_int id ^ ");" + | CondVarSignal id -> + "CondVarSignal(" ^ string_of_int id ^ ");" + | CondVarWait cond_var_wait -> + "CondVarWait(" + ^ string_of_int cond_var_wait.cond_var_id + ^ ", " + ^ string_of_int cond_var_wait.mid + ^ "); " + | Nop -> + "" + end + + + module Writer = struct + let write desc ext content = + let dir = Goblintutil.create_dir (Fpath.v "pml-result") in + let path = Fpath.to_string @@ Fpath.append dir (Fpath.v ("pthread." ^ ext)) in + output_file ~filename:path ~text:content ; + print_endline @@ "saved " ^ desc ^ " as " ^ path + end + + let tabulate = ( ^ ) "\t" + + let define = ( ^ ) "#define " + + let goto_str = ( ^ ) "goto " + + let escape xs = + let last = Option.get @@ List.last xs in + let rest = List.take (List.length xs - 1) xs in + List.map (fun s -> s ^ " \\") rest @ [ last ] + + + let if_clause stmts = + [ "if" ] @ List.map (( ^ ) "::" % tabulate) stmts @ [ "fi" ] + + + let run ?arg f = "run " ^ f ^ "(" ^ Option.default "" arg ^ ");" + + let string_of_node = PthreadDomain.Pred.string_of_elt + + let save_promela_model () = + let threads = + List.unique @@ Edges.filter_map_actions Action.extract_thread_create + in + + let thread_count = List.length threads + 1 in + let mutex_count = List.length @@ Tbls.MutexMidTbl.to_list () in + let cond_var_count = List.length @@ Tbls.CondVarIdTbl.to_list () in + + let current_thread_name = ref "" in + let called_funs_done = ref Set.empty in + + let rec process_def res = + print_endline @@ Resource.show res ; + let res_type = Resource.res_type res in + let res_name = Resource.res_name res in + let is_thread = res_type = Resource.Thread in + (* if we already generated code for this function, we just return [] *) + if res_type = Resource.Function && Set.mem res_name !called_funs_done + then [] + else + let res_id = PmlResTbl.get res in + (* set the name of the current thread + * (this function is also run for functions, which need a reference to the thread for checking branching on return vars *) + if is_thread + then ( + current_thread_name := res_name ; + called_funs_done := Set.empty ) + else called_funs_done := Set.add res_name !called_funs_done ; + (* build adjacency matrix for all nodes of this process *) + let a2bs = + let edges = Edges.get res in + AdjacencyMatrix.populate (AdjacencyMatrix.make ()) edges + in + let nodes = AdjacencyMatrix.nodes a2bs in + let out_edges = AdjacencyMatrix.out_edges a2bs in + let in_edges = AdjacencyMatrix.in_edges a2bs in + + let is_end_node = List.is_empty % out_edges in + let is_start_node = List.is_empty % in_edges in + let label n = res_id ^ "_" ^ string_of_node n in + let end_label = res_id ^ "_end" in + let goto = goto_str % label in + let goto_start_node = + match List.find is_start_node nodes with + | Some node -> + goto node + | None -> + "" + in + let called_funs = ref [] in + let str_edge (a, action, b) = + let target_label = if is_end_node b then end_label else label b in + match action with + | Action.Call fun_name when fun_name = "exit" -> + "exit();" + | Action.Call fun_name -> + called_funs := fun_name :: !called_funs ; + let pc = + string_of_int @@ Tbls.FunCallTbl.get (fun_name, target_label) + in + "mark(" ^ pc ^ "); " ^ Action.to_pml action + | _ -> + Action.to_pml action ^ " " ^ goto_str target_label + in + let walk_edges (node, out_edges) = + let edges = Set.map str_edge out_edges |> Set.elements in + let body = match edges with + | _::_::_ -> if_clause edges + | _ -> edges + in + (label node ^ ":") :: body + in + let body = + let return = + let end_stmt = + match res with + | Thread, "mainfun" -> + "exit()" + | Thread, _ -> + "ThreadExit()" + | Function, f -> + "ret_" ^ f ^ "()" + in + end_label ^ ": " ^ end_stmt + in + goto_start_node + :: (List.concat_map walk_edges @@ AdjacencyMatrix.items a2bs) + @ [ return ] + in + let head = + match res with + | Thread, name -> + let tid = Tbls.ThreadTidTbl.get name in + let defs = + let local_defs = + Variables.get_locals tid + |> List.map Variable.show_def + |> List.unique + in + let stack_def = [ "int stack[20];"; "int sp = -1;" ] in + + [ stack_def; local_defs ] + |> List.flatten + |> List.map tabulate + |> String.concat "\n" + in + "proctype " + ^ name + ^ "(byte tid)" + ^ " provided (canRun(" + ^ string_of_int tid + ^ ")) {\n" + ^ defs + ^ "\n" + | Function, name -> + "Fun_" ^ name ^ ":" + in + let called_fun_ids = + List.map (fun fname -> (Resource.Function, fname)) !called_funs + in + let funs = List.concat_map process_def called_fun_ids in + ("" :: head :: List.map tabulate body) + @ funs + @ [ (if is_thread then "}" else "") ] + in + (* used for macros oneIs, allAre, noneAre... *) + let checkStatus = + "(" + ^ ( String.concat " op2 " + @@ List.of_enum + @@ (0 --^ thread_count) + /@ fun i -> "status[" ^ string_of_int i ^ "] op1 v" ) + ^ ")" + in + let allTasks = + "(" + ^ ( String.concat " && " + @@ List.of_enum + @@ ((0 --^ thread_count) /@ fun i -> "prop(" ^ string_of_int i ^ ")") ) + ^ ")" + in + + (* sort definitions so that inline functions come before the threads *) + let process_defs = + Edges.table + |> Hashtbl.keys + |> List.of_enum + |> List.filter (fun res -> Resource.res_type res = Resource.Thread) + |> List.unique + |> List.sort (compareBy PmlResTbl.get) + |> List.concat_map process_def + in + let fun_ret_defs = + let fun_map fun_calls = + match List.hd fun_calls with + | None -> + [] + | Some ((name, _), _) -> + let dec_sp ((_, target_label), id) = + "(stack[sp] == " + ^ string_of_int id + ^ ") -> sp--; " + ^ goto_str target_label + in + let if_branches = List.map dec_sp fun_calls in + let body = (define "ret_" ^ name ^ "()") :: if_clause if_branches in + escape body + in + Tbls.FunCallTbl.to_list () + |> List.group (compareBy (fst % fst)) + |> List.concat_map fun_map + in + let globals = List.map Variable.show_def @@ Variables.get_globals () in + let promela = + let empty_line = "" in + let defs = + [ define "thread_count " ^ string_of_int thread_count + ; define "mutex_count " ^ string_of_int mutex_count + ; define "cond_var_count " ^ string_of_int cond_var_count + ; empty_line + ; define "checkStatus(op1, v, op2) " ^ checkStatus + ; empty_line + ; define "allTasks(prop) " ^ allTasks + ; empty_line + ; "#include \"../spin/pthread.base.pml\"" + ; empty_line + ] + in + let init = + let run_threads = + (* NOTE: assumes no args are passed to the thread func *) + List.map + (fun t -> + let tid = Action.(t.tid) in + let thread_name = Option.get @@ Tbls.ThreadTidTbl.get_key tid in + let tid_str = string_of_int tid in + run thread_name ~arg:tid_str) + threads + in + let run_main = run promela_main ~arg:"0" in + let init_body = (run_main :: run_threads) @ [ "setReady(0);" ] in + [ "init {" ] @ List.map tabulate init_body @ [ "}" ] + in + let body = + let separator = [ empty_line ] in + List.flatten + [ defs + ; init + ; separator + ; fun_ret_defs + ; separator + ; globals + ; process_defs + ] + in + String.concat "\n" body + in + let dot_graph = + let dot_thread tid = + let show_edge (a, action, b) = + let show_node x = + "\"" ^ Resource.res_name tid ^ "_" ^ string_of_node x ^ "\"" + in + show_node a + ^ "\t->\t" + ^ show_node b + ^ "\t[label=\"" + ^ Action.to_pml action + ^ "\"]" + in + let subgraph_head = + "subgraph \"cluster_" ^ Resource.res_name tid ^ "\" {" + in + let subgraph_tail = + "label = \"" ^ Resource.res_name tid ^ "\";\n }\n" + in + let edges_decls = Set.elements @@ Set.map show_edge @@ Edges.get tid in + (subgraph_head :: edges_decls) @ [ subgraph_tail ] + in + let lines = + Hashtbl.keys Edges.table + |> List.of_enum + |> List.unique + |> List.map dot_thread + |> List.concat + in + String.concat "\n " ("digraph file {" :: lines) ^ "}" + in + + Writer.write "promela model" "pml" promela ; + Writer.write "graph" "dot" dot_graph ; + print_endline + "Copy spin/pthread_base.pml to same folder and then do: spin -a \ + pthread.pml && cc -o pan pan.c && ./pan -a" +end + + +module Spec : Analyses.MCPSpec = struct + (* Spec implementation *) + include Analyses.DefaultSpec + + module List = BatList + module V = VarinfoV + + (** Domains *) + module D = PthreadDomain.D + + module C = D + + (** Set of created tasks to spawn when going multithreaded *) + module Tasks = SetDomain.Make (Lattice.Prod (Queries.LS) (D)) + + module G = Tasks + + let tasks_var = + Goblintutil.create_var (makeGlobalVar "__GOBLINT_PTHREAD_TASKS" voidPtrType) + + + module ExprEval = struct + let eval_ptr ctx exp = + let mayPointTo ctx exp = + let a = ctx.ask (Queries.MayPointTo exp) in + if (not (Queries.LS.is_top a)) && Queries.LS.cardinal a > 0 then + let top_elt = (dummyFunDec.svar, `NoOffset) in + let a' = + if Queries.LS.mem top_elt a + then (* UNSOUND *) + Queries.LS.remove top_elt a + else a + in + Queries.LS.elements a' + else + [] + in + List.map fst @@ mayPointTo ctx exp + + + let eval_var ctx exp = + match exp with + | Lval (Mem e, _) -> + eval_ptr ctx e + | Lval (Var v, _) -> + [ v ] + | _ -> + eval_ptr ctx exp + + + let eval_ptr_id ctx exp get = + List.map (get % Variable.show) @@ eval_ptr ctx exp + + + let eval_var_id ctx exp get = + List.map (get % Variable.show) @@ eval_var ctx exp + end + + let name () = "extract-pthread" + + let assign ctx (lval : lval) (rval : exp) : D.t = + let should_ignore_assigns = GobConfig.get_bool "ana.extract-pthread.ignore_assign" in + if PthreadDomain.D.is_bot ctx.local || should_ignore_assigns + then ctx.local + else if Option.is_none !MyCFG.current_node + then ( + (* it is global var assignment *) + let var_opt = Variable.make_from_lval lval in + if Variables.all_vars_are_valid ctx rval + (* TODO: handle the assignment of the global *) + then Option.may (Variables.add (-1)) var_opt + else Option.may (Variables.add_top (-1)) var_opt ; + ctx.local ) + else + let env = Env.get ctx in + let d = Env.d env in + let tid = Int64.to_int @@ Option.get @@ Tid.to_int d.tid in + + let var_opt = Variable.make_from_lval lval in + + if Option.is_none var_opt || (not @@ Variables.all_vars_are_valid ctx rval) + then ( + (* set lhs var to TOP *) + Option.may (Variables.add_top tid) var_opt ; + ctx.local ) + else + let var = Option.get var_opt in + + let lhs_str = Variable.show var in + let rhs_str = sprint printer#pExp rval in + Edges.add env @@ Action.Assign (lhs_str, rhs_str) ; + + Variables.add tid var ; + + { d with pred = Pred.of_node @@ Env.node env } + + + let branch ctx (exp : exp) (tv : bool) : D.t = + if PthreadDomain.D.is_bot ctx.local + then ctx.local + else + let env = Env.get ctx in + let d = Env.d env in + let tid = Int64.to_int @@ Option.get @@ Tid.to_int d.tid in + let is_valid_var = + Option.default false + % Option.map (Variables.valid_var tid) + % Variable.make_from_lhost + in + let var_str = Variable.show % Option.get % Variable.make_from_lhost in + let pred_str op lhs rhs = + let cond_str = lhs ^ " " ^ sprint d_binop op ^ " " ^ rhs in + if tv then cond_str else "!(" ^ cond_str ^ ")" + in + + let add_action pred_str = + match Env.node env with + | MyCFG.Statement { skind = If (e, bt, bf, loc, _); _ } -> + let intermediate_node = + let then_stmt = + List.hd + @@ + if List.is_empty bt.bstmts + then + let le = List.nth bf.bstmts (List.length bf.bstmts - 1) in + le.succs + else bt.bstmts + in + let else_stmt = + List.hd + @@ + if List.is_empty bf.bstmts + then + let le = List.nth bt.bstmts (List.length bt.bstmts - 1) in + le.succs + else bf.bstmts + in + Tbls.NodeTbl.get (if tv then then_stmt else else_stmt).sid + in + Edges.add ~dst:intermediate_node env (Action.Cond pred_str) ; + { ctx.local with pred = Pred.of_node intermediate_node } + | _ -> + failwith "branch: current_node is not an If" + in + + let handle_binop op lhs rhs = + match (lhs, rhs) with + | Lval (lhost, _), Const (CInt (i, _, _)) + | Const (CInt (i, _, _)), Lval (lhost, _) + when is_valid_var lhost -> + add_action @@ pred_str op (var_str lhost) (Z.to_string i) + | Lval (lhostA, _), Lval (lhostB, _) + when is_valid_var lhostA && is_valid_var lhostB -> + add_action @@ pred_str op (var_str lhostA) (var_str lhostB) + | _ -> + ctx.local + in + let handle_unop x tv = + match x with + | Lval (lhost, _) when is_valid_var lhost -> + let pred = (if tv then "" else "!") ^ var_str lhost in + add_action pred + | _ -> + ctx.local + in + match exp with + | BinOp (op, a, b, _) -> + handle_binop op (stripCasts a) (stripCasts b) + | UnOp (LNot, a, _) -> + handle_unop a (not tv) + | Const (CInt _) -> + handle_unop exp tv + | _ -> + ctx.local + + + let body ctx (f : fundec) : D.t = + (* enter is not called for spawned threads -> initialize them here *) + let context_hash = Int64.of_int (if not !Goblintutil.global_initialization then ControlSpecC.hash (ctx.control_context ()) else 37) in + { ctx.local with ctx = Ctx.of_int context_hash } + + + 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 = + (* on function calls (also for main); not called for spawned threads *) + let d_caller = ctx.local in + let d_callee = + if D.is_bot ctx.local + then ctx.local + else + { ctx.local with + pred = Pred.of_node (MyCFG.Function f) + ; ctx = Ctx.top () + } + in + (* set predecessor set to start node of function *) + [ (d_caller, d_callee) ] + + + let combine + ctx + (lval : lval option) + fexp + (f : fundec) + (args : exp list) + fc + (au : D.t) : D.t = + if D.any_is_bot ctx.local || D.any_is_bot au + then ctx.local + else + let d_caller = ctx.local in + let d_callee = au in + (* check if the callee has some relevant edges, i.e. advanced from the entry point + * if not, we generate no edge for the call and keep the predecessors from the caller *) + (* set should never be empty *) + if Pred.is_bot d_callee.pred then failwith "d_callee.pred is bot!" ; + if Pred.equal d_callee.pred @@ Pred.of_node @@ MyCFG.Function f + then + (* set current node as new predecessor, since something interesting happend during the call *) + { d_callee with pred = d_caller.pred; ctx = d_caller.ctx } + else + let env = Env.get ctx in + (* write out edges with call to f coming from all predecessor nodes of the caller *) + ( if Ctx.is_int d_callee.ctx + then + let last_pred = d_caller.pred in + let action = Action.Call (fun_ctx d_callee.ctx f.svar) in + Edges.add ~d:{ d_caller with pred = last_pred } env action ) ; + (* set current node as new predecessor, since something interesting happend during the call *) + { d_callee with + pred = Pred.of_node @@ Env.node env + ; ctx = d_caller.ctx + } + + + let special ctx (lval : lval option) (f : varinfo) (arglist : exp list) : D.t = + if D.any_is_bot ctx.local then + ctx.local + else + let env = Env.get ctx in + let d = Env.d env in + let tid = Int64.to_int @@ Option.get @@ Tid.to_int d.tid in + + let add_actions (actions : Action.t list) = + let add_failed_assign_action () = + lval + >>= Variable.make_from_lval + >>= fun var -> + Variables.add tid var ; + + Option.some + @@ Action.Assign (Variable.show var, "-1") + in + + List.iter (Edges.add env) actions ; + + let should_assume_success = + GobConfig.get_bool "ana.extract-pthread.assume_success" + in + if not should_assume_success + then Option.may (Edges.add env) @@ add_failed_assign_action () ; + + if List.is_empty actions + then d + else { d with pred = Pred.of_node @@ Env.node env } + in + let add_action action = add_actions [ action ] in + + let arglist' = List.map (stripCasts % constFold false) arglist in + match (LibraryFunctions.find f).special arglist', f.vname, arglist with + | ThreadCreate _ , _, [ thread; thread_attr; func; fun_arg ] -> + let funs_ls = + let ls = ctx.ask (Queries.ReachableFrom func) in + Queries.LS.filter + (fun (v, o) -> + let lval = (Var v, Lval.CilLval.to_ciloffs o) in + isFunctionType (typeOfLval lval)) + ls + in + let thread_fun = + funs_ls + |> Queries.LS.elements + |> List.map fst + |> List.unique ~eq:(fun a b -> a.vid = b.vid) + |> List.hd + in + + let add_task tid = + let tasks = + let f_d:PthreadDomain.D.t = + { tid = Tid.of_int @@ Int64.of_int tid + ; pred = Pred.of_node (ctx.prev_node) + ; ctx = Ctx.top () + } + in + Tasks.singleton (funs_ls, f_d) + in + ctx.sideg tasks_var tasks ; + in + let thread_create tid = + let fun_name = Variable.show thread_fun in + let add_visited_edges fun_tids = + let existing_tid = List.hd @@ Set.elements fun_tids in + let resource_from_tid tid = + Resource.make Resource.Thread + @@ Option.get + @@ Tbls.ThreadTidTbl.get_key tid + in + let edges = Edges.get @@ resource_from_tid existing_tid in + + let launches_child_thread = + let is_thread_create = function + | _, Action.ThreadCreate _, _ -> + true + | _ -> + false + in + Set.exists is_thread_create edges + in + + if launches_child_thread + then + failwith + "Unsupported use case! Thread is not allowed to launch a \ + child thread" ; + + Hashtbl.add Edges.table (resource_from_tid tid) edges + in + + add_task tid ; + + (* multiple threads may be launched with the same function entrypoint + * but functions are visited only once + * Want to have add the visited edges to the new thread that visits + * the same function *) + Option.may add_visited_edges @@ Tbls.FunNameToTids.get fun_name ; + Tbls.FunNameToTids.extend fun_name tid ; + + Action.ThreadCreate { f = thread_fun; tid } + in + + add_actions + @@ List.map thread_create + @@ ExprEval.eval_ptr_id ctx thread Tbls.ThreadTidTbl.get + + | ThreadJoin _, _, [ thread; thread_ret ] -> + add_actions + @@ List.map (fun tid -> Action.ThreadJoin tid) + @@ ExprEval.eval_var_id ctx thread Tbls.ThreadTidTbl.get + | Lock _, _, [ mutex ] -> + add_actions + @@ List.map (fun mid -> Action.MutexLock mid) + @@ ExprEval.eval_ptr_id ctx mutex Tbls.MutexMidTbl.get + | Unlock _, _, [mutex] -> + add_actions + @@ List.map (fun mid -> Action.MutexUnlock mid) + @@ ExprEval.eval_ptr_id ctx mutex Tbls.MutexMidTbl.get + | ThreadExit _, _ , [status] -> + add_action Action.ThreadExit + | Abort, _, _ -> + add_action (Action.Call "exit") + | Unknown, "pthread_mutex_init", [ mutex; mutex_attr ] -> + (* TODO: reentrant mutex handling *) + add_actions + @@ List.map (fun mid -> Action.MutexInit mid) + @@ ExprEval.eval_ptr_id ctx mutex Tbls.MutexMidTbl.get + | Unknown, "pthread_cond_init", [ cond_var; cond_var_attr ] -> + add_actions + @@ List.map (fun id -> Action.CondVarInit id) + @@ ExprEval.eval_ptr_id ctx cond_var Tbls.CondVarIdTbl.get + | Unknown, "pthread_cond_broadcast", [ cond_var ] -> + add_actions + @@ List.map (fun id -> Action.CondVarBroadcast id) + @@ ExprEval.eval_ptr_id ctx cond_var Tbls.CondVarIdTbl.get + | Unknown, "pthread_cond_signal", [ cond_var ] -> + add_actions + @@ List.map (fun id -> Action.CondVarSignal id) + @@ ExprEval.eval_ptr_id ctx cond_var Tbls.CondVarIdTbl.get + | Unknown, "pthread_cond_wait", [ cond_var; mutex ] -> + let cond_vars = ExprEval.eval_ptr ctx cond_var in + let mutex_vars = ExprEval.eval_ptr ctx mutex in + let cond_var_action (v, m) = + let open Action in + CondVarWait + { cond_var_id = Tbls.CondVarIdTbl.get @@ Variable.show v + ; mid = Tbls.MutexMidTbl.get @@ Variable.show m + } + in + add_actions + @@ List.map cond_var_action + @@ List.cartesian_product cond_vars mutex_vars + | _ -> ctx.local + + let startstate v = + let open D in + make + (Tid.of_int 0L) + (Pred.of_node (MyCFG.Function (emptyFunction "main"))) + (Ctx.top ()) + + + let threadenter ctx lval f args = + let d : D.t = ctx.local in + let tasks = ctx.global tasks_var in + (* TODO: optimize finding *) + let tasks_f = + Tasks.filter + (fun (fs, f_d) -> Queries.LS.exists (fun (ls_f, _) -> ls_f = f) fs) + tasks + in + let f_d = snd (Tasks.choose tasks_f) in + [ { f_d with pred = d.pred } ] + + + let threadspawn ctx lval f args fctx = ctx.local + + let exitstate v = D.top () + + let finalize = Codegen.save_promela_model + +end + +let _ = MCP.register_analysis ~dep:[ "base" ] (module Spec : MCPSpec) diff --git a/src/cdomains/pthreadDomain.ml b/src/cdomains/pthreadDomain.ml new file mode 100644 index 0000000000..9f2d4dbad7 --- /dev/null +++ b/src/cdomains/pthreadDomain.ml @@ -0,0 +1,86 @@ +open Prelude + +(** Thread ID *) +module Tid = IntDomain.Flattened + +(** Context hash for function calls *) +module Ctx = IntDomain.Flattened + +(** Set of predecessor nodes *) +module Pred = struct + module Base = CilType.Location + include SetDomain.Make (Base) + + let of_node = singleton % Node.location + + let of_current_node () = of_node @@ Option.get !MyCFG.current_node + + let string_of_elt (loc:Base.t) = + let f i = (if i < 0 then "n" else "") ^ string_of_int (abs i) in + f loc.line ^ "b" ^ f loc.byte +end + +module D = struct + type domain = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving to_yojson] + type t = domain + + (** printing *) + let show x = + Printf.sprintf + "{ Tid=%s; pred=%s; ctx=%s }" + (Tid.show x.tid) + (Pred.show x.pred) + (Ctx.show x.ctx) + + include Printable.SimpleShow(struct type t = domain let show = show end) + + let name () = "pthread state" + + (** let equal = Util.equals *) + let equal x y = + Tid.equal x.tid y.tid && Pred.equal x.pred y.pred && Ctx.equal x.ctx y.ctx + + + (** compare all fields with correspoding compare operators *) + let compare x y = + List.fold_left + (fun acc v -> if acc = 0 && v <> 0 then v else acc) + 0 + [ Tid.compare x.tid y.tid + ; Pred.compare x.pred y.pred + ; Ctx.compare x.ctx y.ctx + ] + + + (** let hash = Hashtbl.hash *) + let hash x = Hashtbl.hash (Tid.hash x.tid, Pred.hash x.pred, Ctx.hash x.ctx) + let make tid pred ctx = { tid; pred; ctx } + let bot () = { tid = Tid.bot (); pred = Pred.bot (); ctx = Ctx.bot () } + let is_bot x = Tid.is_bot x.tid && Pred.is_bot x.pred && Ctx.is_bot x.ctx + let any_is_bot x = Tid.is_bot x.tid || Pred.is_bot x.pred + let top () = { tid = Tid.top (); pred = Pred.top (); ctx = Ctx.top () } + let is_top x = Tid.is_top x.tid && Pred.is_top x.pred && Ctx.is_top x.ctx + + let leq x y = Tid.leq x.tid y.tid && Pred.leq x.pred y.pred && Ctx.leq x.ctx y.ctx + + let op_scheme op1 op2 op3 x y : t = + { tid = op1 x.tid y.tid; pred = op2 x.pred y.pred; ctx = op3 x.ctx y.ctx } + + let join = op_scheme Tid.join Pred.join Ctx.join + let widen = join + let meet = op_scheme Tid.meet Pred.meet Ctx.meet + let narrow = meet + + let arbitrary () = failwith "no arbitrary" + let tag x = failwith "no tag" + let relift x = x + + let pretty_diff () (x,y) = + if not (Tid.leq x.tid y.tid) then + Tid.pretty_diff () (x.tid,y.tid) + else if not (Pred.leq x.pred y.pred) then + Pred.pretty_diff () (x.pred,y.pred) + else + Ctx.pretty_diff () (x.ctx, y.ctx) + +end diff --git a/src/util/options.schema.json b/src/util/options.schema.json index f91bb9b34e..357347161a 100644 --- a/src/util/options.schema.json +++ b/src/util/options.schema.json @@ -891,6 +891,25 @@ } }, "additionalProperties": false + }, + "extract-pthread" : { + "title": "ana.extract-pthread", + "type": "object", + "properties": { + "assume_success": { + "title": "ana.extract-pthread.assume_success", + "description": "Assume that all POSIX pthread functions succeed.", + "type": "boolean", + "default": true + }, + "ignore_assign": { + "title": "ana.extract-pthread.ignore_assign", + "description": "Ignores any assigns in POSIX programs.", + "type": "boolean", + "default": true + } + }, + "additionalProperties": false } }, "additionalProperties": false diff --git a/tests/extraction/00-sanity.c b/tests/extraction/00-sanity.c new file mode 100644 index 0000000000..e3531e0b4f --- /dev/null +++ b/tests/extraction/00-sanity.c @@ -0,0 +1,17 @@ +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + + +int main(void) { + pthread_t id1, id2; + int i; + + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + pthread_mutex_lock(&mutex1); + + return 0; +} diff --git a/tests/extraction/01-base.c b/tests/extraction/01-base.c new file mode 100644 index 0000000000..bea2419862 --- /dev/null +++ b/tests/extraction/01-base.c @@ -0,0 +1,37 @@ +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex1); + pthread_mutex_lock(&mutex2); + g1 = g2 + 1; + pthread_mutex_unlock(&mutex2); + pthread_mutex_unlock(&mutex1); + return NULL; +} + +void *t2(void *arg) { + pthread_mutex_lock(&mutex2); + pthread_mutex_lock(&mutex1); + pthread_mutex_unlock(&mutex1); + pthread_mutex_unlock(&mutex2); + return NULL; +} + +int main(void) { + pthread_t id1, id2; + int i; + + pthread_create(&id1, NULL, t1, NULL); + pthread_create(&id2, NULL, t2, NULL); + pthread_mutex_unlock(&mutex1); + pthread_join (id1, NULL); + pthread_join (id2, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + + return 0; +} diff --git a/tests/extraction/02-starve.c b/tests/extraction/02-starve.c new file mode 100644 index 0000000000..dc0c4e639c --- /dev/null +++ b/tests/extraction/02-starve.c @@ -0,0 +1,23 @@ +#include +#include + +int g1, g2; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t1(void *arg) { + pthread_mutex_lock(&mutex1); + return NULL; +} + + +int main(void) { + pthread_t id1, id2; + int i; + + pthread_mutex_lock(&mutex1); + pthread_create(&id1, NULL, t1, NULL); + printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2); + + return 0; +} diff --git a/tests/extraction/test.sh b/tests/extraction/test.sh new file mode 100755 index 0000000000..d6cf4af536 --- /dev/null +++ b/tests/extraction/test.sh @@ -0,0 +1,28 @@ +#!/usr/bin/env bash +mkdir -p run +cp -r ../../spin run/spin +cd run + +../../../goblint --set ana.activated[+] extract-pthread ../00-sanity.c && spin -a pml-result/pthread.pml && cc -o pan pan.c && ./pan -a &> out.txt +output=$(cat out.txt | grep pthread.pml.trail) +if [ "$output" ] +then + echo "Unexpected verdict: Starving" + exit 1 +fi + +../../../goblint --set ana.activated[+] extract-pthread ../01-base.c && spin -a pml-result/pthread.pml && cc -o pan pan.c && ./pan -a &> out.txt +output=$(cat out.txt | grep pthread.pml.trail) +if [ -z "$output" ] +then + echo "Unexpected verdict: Non-Starving" + exit 2 +fi + +../../../goblint --set ana.activated[+] extract-pthread ../02-starve.c && spin -a pml-result/pthread.pml && cc -o pan pan.c && ./pan -a &> out.txt +output=$(cat out.txt | grep pthread.pml.trail) +if [ -z "$output" ] +then + echo "Unexpected verdict: Non-Starving" + exit 3 +fi