diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index e1648904c3..1d73e037f4 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -46,7 +46,7 @@ jobs: - name: Setup Pages id: pages - uses: actions/configure-pages@v3 + uses: actions/configure-pages@v4 - name: Install dependencies run: opam install . --deps-only --locked --with-doc @@ -68,4 +68,4 @@ jobs: steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@v2 + uses: actions/deploy-pages@v3 diff --git a/.github/workflows/options.yml b/.github/workflows/options.yml index 94c49e4bf6..7ef8b6929e 100644 --- a/.github/workflows/options.yml +++ b/.github/workflows/options.yml @@ -26,10 +26,10 @@ jobs: run: npm install -g ajv-cli - name: Migrate schema # https://github.com/ajv-validator/ajv-cli/issues/199 - run: ajv migrate -s src/common/util/options.schema.json + run: ajv migrate -s src/config/options.schema.json - name: Validate conf - run: ajv validate -s src/common/util/options.schema.json -d "conf/**/*.json" + run: ajv validate -s src/config/options.schema.json -d "conf/**/*.json" - name: Validate incremental tests - run: ajv validate -s src/common/util/options.schema.json -d "tests/incremental/*/*.json" + run: ajv validate -s src/config/options.schema.json -d "tests/incremental/*/*.json" diff --git a/.gitignore b/.gitignore index 75bd23d36b..faf1513653 100644 --- a/.gitignore +++ b/.gitignore @@ -29,7 +29,6 @@ linux-headers .goblint*/ goblint_temp_*/ -src/spec/graph .vagrant g2html.jar diff --git a/.readthedocs.yaml b/.readthedocs.yaml index 08044d195c..22f9c86121 100644 --- a/.readthedocs.yaml +++ b/.readthedocs.yaml @@ -20,4 +20,4 @@ build: - pip install json-schema-for-humans post_build: - mkdir _readthedocs/html/jsfh/ - - generate-schema-doc --config-file jsfh.yml src/common/util/options.schema.json _readthedocs/html/jsfh/ + - generate-schema-doc --config-file jsfh.yml src/config/options.schema.json _readthedocs/html/jsfh/ diff --git a/docs/developer-guide/messaging.md b/docs/developer-guide/messaging.md index 28f24bc49c..0028d51f87 100644 --- a/docs/developer-guide/messaging.md +++ b/docs/developer-guide/messaging.md @@ -47,16 +47,3 @@ The `~loc` argument is optional and defaults to the current location, but allows The `_noloc` suffixed functions allow general messages without any location (not even current). By convention, may-warnings (the usual case) should use warning severity and must-warnings should use error severity. - -### Spec analysis - -Warnings inside `.spec` files are converted to warnings. -They parsed from string warnings: the first space-delimited substring determines the category and the rest determines the text. - -For example: -``` -w1 "behavior.undefined.use_after_free" -w2 "integer.overflow" -w3 "unknown my message" -w4 "integer.overflow some text describing the warning" -``` diff --git a/docs/user-guide/configuring.md b/docs/user-guide/configuring.md index 9a32a14a4c..cae57fc8cd 100644 --- a/docs/user-guide/configuring.md +++ b/docs/user-guide/configuring.md @@ -24,7 +24,7 @@ In `.vscode/settings.json` add the following: "/conf/*.json", "/tests/incremental/*/*.json" ], - "url": "/src/common/util/options.schema.json" + "url": "/src/config/options.schema.json" } ] } diff --git a/dune-project b/dune-project index 81c8d2f091..37e81f4199 100644 --- a/dune-project +++ b/dune-project @@ -25,7 +25,7 @@ (depends (ocaml (>= 4.10)) (goblint-cil (>= 2.0.3)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint. - (batteries (>= 3.5.0)) + (batteries (>= 3.5.1)) (zarith (>= 1.8)) (yojson (>= 2.0.0)) (qcheck-core (>= 0.19)) diff --git a/goblint.opam b/goblint.opam index 669b2d9c40..b5f1f360dc 100644 --- a/goblint.opam +++ b/goblint.opam @@ -22,7 +22,7 @@ depends: [ "dune" {>= "3.7"} "ocaml" {>= "4.10"} "goblint-cil" {>= "2.0.3"} - "batteries" {>= "3.5.0"} + "batteries" {>= "3.5.1"} "zarith" {>= "1.8"} "yojson" {>= "2.0.0"} "qcheck-core" {>= "0.19"} diff --git a/gobview b/gobview index d4eb66b9eb..3de13d7412 160000 --- a/gobview +++ b/gobview @@ -1 +1 @@ -Subproject commit d4eb66b9eb277349a75141cb01899dbab9d3ef5d +Subproject commit 3de13d74124ab7bc30d8be299f02570d8f498b84 diff --git a/scripts/goblint-lib-modules.py b/scripts/goblint-lib-modules.py index 5f02271616..ec0e78e440 100755 --- a/scripts/goblint-lib-modules.py +++ b/scripts/goblint-lib-modules.py @@ -30,20 +30,18 @@ "MessagesCompare", "PrivPrecCompare", "ApronPrecCompare", - "Mainspec", # libraries "Goblint_std", "Goblint_timing", "Goblint_backtrace", + "Goblint_tracing", "Goblint_sites", "Goblint_build_info", "Dune_build_info", "MessageCategory", # included in Messages "PreValueDomain", # included in ValueDomain - "SpecCore", # spec stuff - "SpecUtil", # spec stuff "ConfigVersion", "ConfigProfile", diff --git a/scripts/regression2sv-benchmarks.py b/scripts/regression2sv-benchmarks.py index 8f74a70f52..7bcc1c7ea3 100755 --- a/scripts/regression2sv-benchmarks.py +++ b/scripts/regression2sv-benchmarks.py @@ -31,7 +31,6 @@ "09-regions_34-escape_rc", # duplicate of 04/45 "09-regions_35-list2_rc-offsets-thread", # duplicate of 09/03 "10-synch_17-glob_fld_nr", # duplicate of 05/08 - "19-spec_02-mutex_rc", # duplicate of 04/01 "29-svcomp_01-race-2_3b-container_of", # duplicate sv-benchmarks "29-svcomp_01-race-2_4b-container_of", # duplicate sv-benchmarks diff --git a/scripts/spec/check.sh b/scripts/spec/check.sh deleted file mode 100755 index 57b63edfd2..0000000000 --- a/scripts/spec/check.sh +++ /dev/null @@ -1,27 +0,0 @@ -export OCAMLRUNPARAM=b -# file to analyze -file=${1-"tests/file.c"} -# analysis to run or spec file -ana=${2-"tests/regression/18-file/file.optimistic.spec"} -debug=${debug-"true"} -if [ $ana == "file" ]; then - ana="file" - opt="--set ana.file.optimistic true" -else - spec=$ana - ana="spec" - opt="--set ana.spec.file $spec" -fi -cmd="./goblint --set ana.activated[0][+] $ana $opt --html --set warn.debug $debug $file" -echo -e "$(tput setaf 6)$cmd$(tput sgr 0)" -$cmd - - -# # focuses Firefox and reloads current tab -# if false && command -v xdotool >/dev/null 2>&1; then -# WID=`xdotool search --name "Mozilla Firefox" | head -1` -# xdotool windowactivate $WID -# #xdotool key F5 -# # reload is done by add-on Auto Reload (reload result/* on change of report.html) -# # https://addons.mozilla.org/en-US/firefox/addon/auto-reload/?src=api -# fi diff --git a/scripts/spec/regression.py b/scripts/spec/regression.py deleted file mode 100755 index dc9f9fa276..0000000000 --- a/scripts/spec/regression.py +++ /dev/null @@ -1,61 +0,0 @@ -# import fileinput -# for line in fileinput.input(): -# pass - -import sys, os -import re - -if len(sys.argv) != 2: - print("Stdin: output from goblint, 1. argument: C source-file") - sys.exit(1) -path = sys.argv[1] - -goblint = {} -for line in sys.stdin.readlines(): - line = re.sub(r"\033.*?m", "", line) - m = re.match(r"(.+) \("+re.escape(path)+":(.+)\)", line) - if m: goblint[int(m.group(2))] = m.group(1) - -source = {} -lines = open(path).readlines() -for i,line in zip(range(1, len(lines)+1), lines): - m = re.match(r".+ // WARN: (.+)", line) - if m: source[i] = m.group(1) - -diff = {}; -for k,v in sorted(set.union(set(goblint.items()), set(source.items()))): - if k in diff: continue - if k in goblint and k in source and goblint[k]!=source[k]: - diff[k] = ('D', [goblint[k], source[k]]) - elif (k,v) in goblint.items() and (k,v) not in source.items(): - diff[k] = ('G', [goblint[k]]) - elif (k,v) not in goblint.items() and (k,v) in source.items(): - diff[k] = ('S', [source[k]]) - -if not len(diff): - sys.exit(0) - -print("#"*50) -print(path) -print("file://"+os.getcwd()+"/result/"+os.path.basename(path)+".html") - -if len(goblint): - print("## Goblint warnings:") - for k,v in sorted(goblint.items()): - print("{} \t {}".format(k, v)) - print - -if len(source): - print("## Source warnings:") - for k,v in source.items(): - print("{} \t {}".format(k, v)) - print - -if len(diff): - print("## Diff (G..only goblint, S..only source, D..different):") - for k,(s,v) in sorted(diff.items()): - print("{} {} \t {}".format(s, k, v[0])) - for v in v[1:]: print("\t {}".format(v)) - -print -sys.exit(1) \ No newline at end of file diff --git a/scripts/spec/regression.sh b/scripts/spec/regression.sh deleted file mode 100755 index 6dc740ca75..0000000000 --- a/scripts/spec/regression.sh +++ /dev/null @@ -1,18 +0,0 @@ -debug_tmp=$debug -export debug=false # temporarily disable debug output -n=0 -c=0 -dir=${2-"tests/regression/18-file"} -for f in $dir/*.c; do - ./scripts/spec/check.sh $f ${1-"file"} 2>/dev/null | python scripts/spec/regression.py $f && ((c++)) - ((n++)) -done -debug=$debug_tmp -msg="passed $c/$n tests" -echo $msg -if [ $c -eq $n ]; then - exit 0 -else - notify-send -i stop "$msg" - exit 1 -fi diff --git a/scripts/spec/spec.sh b/scripts/spec/spec.sh deleted file mode 100755 index 03abe9a0c7..0000000000 --- a/scripts/spec/spec.sh +++ /dev/null @@ -1,10 +0,0 @@ -# print all states the parser goes through -#export OCAMLRUNPARAM='p' -bin=src/mainspec.native -spec=${1-"tests/regression/18-file/file.spec"} -ocamlbuild -yaccflag -v -X webapp -no-links -use-ocamlfind $bin \ - && (./_build/$bin $spec \ - || (echo "$spec failed, running interactive now..."; - rlwrap ./_build/$bin - ) - ) diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index b181a1c70e..efad8b4c2e 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -29,7 +29,7 @@ struct let init _ = 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 (ModifiedSinceLongjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated + emit_single_threaded := List.mem (ModifiedSinceSetjmp.Spec.name ()) activated || List.mem (PoisonVariables.Spec.name ()) activated let do_access (ctx: (D.t, G.t, C.t, V.t) ctx) (kind:AccessKind.t) (reach:bool) (e:exp) = if M.tracing then M.trace "access" "do_access %a %a %B\n" d_exp e AccessKind.pretty kind reach; diff --git a/src/analyses/apron/affineEqualityAnalysis.apron.ml b/src/analyses/apron/affineEqualityAnalysis.apron.ml index 03a9ecdb57..ce859d87b7 100644 --- a/src/analyses/apron/affineEqualityAnalysis.apron.ml +++ b/src/analyses/apron/affineEqualityAnalysis.apron.ml @@ -11,7 +11,6 @@ let spec_module: (module MCPSpec) Lazy.t = let module AD = AffineEqualityDomain.D2 (VectorMatrix.ArrayVector) (VectorMatrix.ArrayMatrix) in let module RD: RelationDomain.RD = struct - module Var = AffineEqualityDomain.Var module V = AffineEqualityDomain.V include AD end diff --git a/src/analyses/apron/apronAnalysis.apron.ml b/src/analyses/apron/apronAnalysis.apron.ml index 29e295a662..0ba17cdb35 100644 --- a/src/analyses/apron/apronAnalysis.apron.ml +++ b/src/analyses/apron/apronAnalysis.apron.ml @@ -12,10 +12,9 @@ let spec_module: (module MCPSpec) Lazy.t = let module AD = (val if diff_box then (module ApronDomain.BoxProd (AD): ApronDomain.S3) else (module AD)) in let module RD: RelationDomain.RD = struct - module Var = ApronDomain.Var module V = ApronDomain.V include AD - type var = ApronDomain.Var.t + type var = Apron.Var.t end in let module Priv = (val RelationPriv.get_priv ()) in diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index d2fe7eab9e..5e128ffc30 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -283,8 +283,9 @@ struct let pass_to_callee fundec any_local_reachable var = (* TODO: currently, we pass all locals of the caller to the callee, provided one of them is reachbale to preserve relationality *) (* there should be smarter ways to do this, e.g. by keeping track of which values are written etc. ... *) + (* See, e.g, Beckschulze E, Kowalewski S, Brauer J (2012) Access-based localization for octagons. Electron Notes Theor Comput Sci 287:29–40 *) (* Also, a local *) - let vname = RD.Var.to_string var in + let vname = Apron.Var.to_string var in let locals = fundec.sformals @ fundec.slocals in match List.find_opt (fun v -> VM.var_name (Local v) = vname) locals with (* TODO: optimize *) | None -> true @@ -295,8 +296,7 @@ struct let st = ctx.local in let arg_assigns = GobList.combine_short f.sformals args (* TODO: is it right to ignore missing formals/args? *) - |> List.filter (fun (x, _) -> RD.Tracked.varinfo_tracked x) - |> List.map (Tuple2.map1 RV.arg) + |> List.filter_map (fun (x, e) -> if RD.Tracked.varinfo_tracked x then Some (RV.arg x, e) else None) in let arg_vars = List.map fst arg_assigns in let new_rel = RD.add_vars st.rel arg_vars in @@ -318,7 +318,7 @@ struct RD.remove_filter_with new_rel (fun var -> match RV.find_metadata var with | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *) - | Some (Arg _) when not (List.mem_cmp RD.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *) + | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *) | _ -> false (* keep everything else (just added args, globals, global privs) *) ); if M.tracing then M.tracel "combine" "relation enter newd: %a\n" RD.pretty new_rel; @@ -404,7 +404,7 @@ struct in let any_local_reachable = any_local_reachable fundec reachable_from_args in let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in - if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (RD.Var.to_string v))) arg_vars; + if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (Apron.Var.to_string v))) arg_vars; RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *) let tainted = f_ask.f Queries.MayBeTainted in let tainted_vars = TaintPartialContexts.conv_varset tainted in diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index b386af162b..f073ae274b 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -195,8 +195,7 @@ struct end module AV = struct - include RelationDomain.VarMetadataTbl (VM) (RD.Var) - + include RelationDomain.VarMetadataTbl (VM) let local g = make_var (Local g) let unprot g = make_var (Unprot g) @@ -1011,17 +1010,17 @@ struct ) ) else ( - match ConcDomain.ThreadSet.elements tids with - | [tid] -> - let lmust',l' = G.thread (getg (V.thread tid)) in - {st with priv = (w, LMust.union lmust' lmust, L.join l l')} - | _ -> - (* To match the paper more closely, one would have to join in the non-definite case too *) - (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) - st - | exception SetDomain.Unsupported _ -> - (* elements throws if the thread set is top *) + if ConcDomain.ThreadSet.is_top tids then st + else + match ConcDomain.ThreadSet.elements tids with + | [tid] -> + let lmust',l' = G.thread (getg (V.thread tid)) in + {st with priv = (w, LMust.union lmust' lmust, L.join l l')} + | _ -> + (* To match the paper more closely, one would have to join in the non-definite case too *) + (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) + st ) let thread_return ask getg sideg tid (st: relation_components_t) = diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 9e79eeec2b..993df9a26a 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2461,10 +2461,12 @@ struct (* handling thread joins... sort of *) | ThreadJoin { thread = id; ret_var }, _ -> let st' = + (* TODO: should invalidate shallowly? https://github.com/goblint/analyzer/pull/1224#discussion_r1405826773 *) match (eval_rv (Analyses.ask_of_ctx ctx) gs st ret_var) with | Int n when GobOption.exists (BI.equal BI.zero) (ID.to_int n) -> st | Address ret_a -> begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with + | Thread a when ValueDomain.Threads.is_top a -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var] | Thread a -> let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in (* TODO: is this type right? *) diff --git a/src/analyses/baseInvariant.ml b/src/analyses/baseInvariant.ml index f391231628..304d3e55ad 100644 --- a/src/analyses/baseInvariant.ml +++ b/src/analyses/baseInvariant.ml @@ -709,18 +709,22 @@ struct | _ -> Int c in (* handle special calls *) - begin match t with - | TInt (ik, _) -> - begin match x with - | ((Var v), offs) -> - if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); - let tv_opt = ID.to_bool c in - begin match tv_opt with + begin match x, t with + | (Var v, offs), TInt (ik, _) -> + let tmpSpecial = ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in + if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty tmpSpecial; + begin match tmpSpecial with + | `Lifted (Abs (ik, xInt)) -> + let c' = ID.cast_to ik c in (* different ik! *) + inv_exp (Int (ID.join c' (ID.neg c'))) xInt st + | tmpSpecial -> + begin match ID.to_bool c with | Some tv -> - begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with + begin match tmpSpecial with | `Lifted (Isfinite xFloat) when tv -> inv_exp (Float (FD.finite (unroll_fk_of_exp xFloat))) xFloat st | `Lifted (Isnan xFloat) when tv -> inv_exp (Float (FD.nan_of (unroll_fk_of_exp xFloat))) xFloat st (* should be correct according to C99 standard*) + (* The following do to_bool and of_bool to convert Not{0} into 1 for downstream float inversions *) | `Lifted (Isgreater (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Gt, xFloat, yFloat, (typeOf xFloat))) st | `Lifted (Isgreaterequal (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Ge, xFloat, yFloat, (typeOf xFloat))) st | `Lifted (Isless (xFloat, yFloat)) -> inv_exp (Int (ID.of_bool ik tv)) (BinOp (Lt, xFloat, yFloat, (typeOf xFloat))) st @@ -730,9 +734,8 @@ struct end | None -> update_lval c x c' ID.pretty end - | _ -> update_lval c x c' ID.pretty end - | _ -> update_lval c x c' ID.pretty + | _, _ -> update_lval c x c' ID.pretty end | Float c -> let c' = match t with @@ -744,22 +747,19 @@ struct | _ -> Float c in (* handle special calls *) - begin match t with - | TFloat (fk, _) -> - begin match x with - | ((Var v), offs) -> - if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty (ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs))); - begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) with - | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st - | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st - | `Lifted (Fabs (ret_fk, xFloat)) -> - let inv = FD.inv_fabs (FD.cast_to ret_fk c) in - if FD.is_bot inv then - raise Analyses.Deadcode - else - inv_exp (Float inv) xFloat st - | _ -> update_lval c x c' FD.pretty - end + begin match x, t with + | (Var v, offs), TFloat (fk, _) -> + let tmpSpecial = ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil offs)) in + if M.tracing then M.trace "invSpecial" "qry Result: %a\n" Queries.ML.pretty tmpSpecial; + begin match tmpSpecial with + | `Lifted (Ceil (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_ceil (FD.cast_to ret_fk c))) xFloat st + | `Lifted (Floor (ret_fk, xFloat)) -> inv_exp (Float (FD.inv_floor (FD.cast_to ret_fk c))) xFloat st + | `Lifted (Fabs (ret_fk, xFloat)) -> + let inv = FD.inv_fabs (FD.cast_to ret_fk c) in + if FD.is_bot inv then + raise Analyses.Deadcode + else + inv_exp (Float inv) xFloat st | _ -> update_lval c x c' FD.pretty end | _ -> update_lval c x c' FD.pretty @@ -821,31 +821,4 @@ struct FD.top_of fk in inv_exp (Float ftv) exp st - - let invariant ctx a gs st exp tv: D.t = - let refine0 = invariant ctx a gs st exp tv in - (* bodge for abs(...); To be removed once we have a clean solution *) - let refineAbs op absargexp valexp = - let flip op = match op with | Le -> Ge | Lt -> Gt | _ -> failwith "impossible" in - (* e.g. |arg| <= 40 *) - (* arg <= e (arg <= 40) *) - let le = BinOp (op, absargexp, valexp, intType) in - (* arg >= -e (arg >= -40) *) - let gt = BinOp(flip op, absargexp, UnOp (Neg, valexp, Cilfacade.typeOf valexp), intType) in - let one = invariant ctx (Analyses.ask_of_ctx ctx) ctx.global refine0 le tv in - invariant ctx (Analyses.ask_of_ctx ctx) ctx.global one gt tv - in - match exp with - | BinOp ((Lt|Le) as op, CastE(t, Lval (Var v, NoOffset)), e,_) when tv -> - begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with - | `Lifted (Abs (ik, arg)) -> refineAbs op (CastE (t, arg)) e - | _ -> refine0 - end - | BinOp ((Lt|Le) as op, Lval (Var v, NoOffset), e, _) when tv -> - begin match ctx.ask (Queries.TmpSpecial (v, Offset.Exp.of_cil NoOffset)) with - | `Lifted (Abs (ik, arg)) -> refineAbs op arg e - | _ -> refine0 - end - | _ -> refine0 - end diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 3843dda300..0126449413 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -211,12 +211,12 @@ struct let thread_join ?(force=false) ask get e st = st let thread_return ask get set tid st = st - let invariant_global getg g = - match g with - | `Left _ -> (* mutex *) - Invariant.none + let invariant_global getg = function | `Right g' -> (* global *) ValueDomain.invariant_global (read_unprotected_global getg) g' + | _ -> (* mutex *) + Invariant.none + end module PerMutexOplusPriv: S = @@ -230,7 +230,7 @@ struct CPA.find x st.cpa (* let read_global ask getg cpa x = let (cpa', v) as r = read_global ask getg cpa x in - ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Tracing.current_loc (is_unprotected ask x) VD.pretty v); + ignore (Pretty.printf "READ GLOBAL %a (%a, %B) = %a\n" CilType.Varinfo.pretty x CilType.Location.pretty !Goblint_tracing.current_loc (is_unprotected ask x) VD.pretty v); r *) let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v = let cpa' = CPA.add x v st.cpa in @@ -544,17 +544,17 @@ struct ) ) else ( - match ConcDomain.ThreadSet.elements tids with - | [tid] -> - let lmust',l' = G.thread (getg (V.thread tid)) in - {st with priv = (w, LMust.union lmust' lmust, L.join l l')} - | _ -> - (* To match the paper more closely, one would have to join in the non-definite case too *) - (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) - st - | exception SetDomain.Unsupported _ -> - (* elements throws if the thread set is top *) + if ConcDomain.ThreadSet.is_top tids then st + else + match ConcDomain.ThreadSet.elements tids with + | [tid] -> + let lmust',l' = G.thread (getg (V.thread tid)) in + {st with priv = (w, LMust.union lmust' lmust, L.join l l')} + | _ -> + (* To match the paper more closely, one would have to join in the non-definite case too *) + (* Given how we handle lmust (for initialization), doing this might actually be beneficial given that it grows lmust *) + st ) let thread_return ask getg sideg tid (st: BaseComponents (D).t) = @@ -625,13 +625,11 @@ struct let get_mutex_inits' = CPA.find x get_mutex_inits in VD.join get_mutex_global_x' get_mutex_inits' - let invariant_global getg g = - match g with - | `Left (`Left _) -> (* mutex *) - Invariant.none - | `Left (`Right g') -> (* global *) - ValueDomain.invariant_global (read_unprotected_global getg) g' - | `Right _ -> (* thread *) + let invariant_global getg = function + | `Middle g -> (* global *) + ValueDomain.invariant_global (read_unprotected_global getg) g + | `Left _ + | `Right _ -> (* mutex or thread *) Invariant.none end @@ -847,16 +845,15 @@ struct open Locksets - let invariant_global getg g = - match g with - | `Left _ -> (* mutex *) - Invariant.none + let invariant_global getg = function | `Right g' -> (* global *) ValueDomain.invariant_global (fun x -> GWeak.fold (fun s' tm acc -> WeakRange.fold_weak VD.join tm acc ) (G.weak (getg (V.global x))) (VD.bot ()) ) g' + | _ -> (* mutex *) + Invariant.none let invariant_vars ask getg st = let module VS = Set.Make (CilType.Varinfo) in @@ -1668,7 +1665,7 @@ struct let read_global ask getg st x = let v = Priv.read_global ask getg st x in if !AnalysisState.postsolving && !is_dumping then - LVH.modify_def (VD.bot ()) (!Tracing.current_loc, x) (VD.join v) lvh; + LVH.modify_def (VD.bot ()) (!Goblint_tracing.current_loc, x) (VD.join v) lvh; v let dump () = diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 88181000b9..73a2e75de1 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -85,11 +85,10 @@ struct end module V = struct - (* TODO: Either3? *) - include Printable.Either (struct include Printable.Either (VMutex) (VMutexInits) let name () = "mutex" end) (VGlobal) + include Printable.Either3 (VMutex) (VMutexInits) (VGlobal) let name () = "MutexGlobals" - let mutex x: t = `Left (`Left x) - let mutex_inits: t = `Left (`Right ()) + let mutex x: t = `Left x + let mutex_inits: t = `Middle () let global x: t = `Right x end diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml index f084a21edb..8412a65683 100644 --- a/src/analyses/extractPthread.ml +++ b/src/analyses/extractPthread.ml @@ -220,7 +220,7 @@ module Tbls = struct 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 + let loc = { !Goblint_tracing.current_loc with line } in MyCFG.Statement { (mkStmtOneInstr @@ Set (var dummyFunDec.svar, zero, loc, loc)) with sid = new_sid () diff --git a/src/analyses/fileUse.ml b/src/analyses/fileUse.ml deleted file mode 100644 index 58257b7843..0000000000 --- a/src/analyses/fileUse.ml +++ /dev/null @@ -1,296 +0,0 @@ -(** Analysis of correct file handle usage ([file]). - - @see Vogler, R. Verifying Regular Safety Properties of C Programs Using the Static Analyzer Goblint. Section 3.*) - -open Batteries -open GoblintCil -open Analyses - -module Spec = -struct - include Analyses.DefaultSpec - - let name () = "file" - module D = FileDomain.Dom - module C = FileDomain.Dom - - (* special variables *) - let return_var = Cilfacade.create_var @@ Cil.makeVarinfo false "@return" Cil.voidType, `NoOffset - let unclosed_var = Cilfacade.create_var @@ Cil.makeVarinfo false "@unclosed" Cil.voidType, `NoOffset - - (* keys that were already warned about; needed for multiple returns (i.e. can't be kept in D) *) - let warned_unclosed = ref Set.empty - - (* queries *) - let query ctx (type a) (q: a Queries.t) = - match q with - | Queries.MayPointTo exp -> if M.tracing then M.tracel "file" "query MayPointTo: %a" d_plainexp exp; Queries.Result.top q - | _ -> Queries.Result.top q - - let query_ad (ask: Queries.ask) exp = - match ask.f (Queries.MayPointTo exp) with - | ad when not (Queries.AD.is_top ad) -> Queries.AD.elements ad - | _ -> [] - let print_query_lv ?msg:(msg="") ask exp = - let addrs = query_ad ask exp in (* MayPointTo -> LValSet *) - let pretty_key = function - | Queries.AD.Addr.Addr (v,o) -> Pretty.text (D.string_of_key (v, ValueDomain.Addr.Offs.to_exp o)) - | _ -> Pretty.text "" in - if M.tracing then M.tracel "file" "%s MayPointTo %a = [%a]" msg d_exp exp (Pretty.docList ~sep:(Pretty.text ", ") pretty_key) addrs - - let eval_fv ask exp: varinfo option = - match query_ad ask exp with - | [addr] -> Queries.AD.Addr.to_var_may addr - | _ -> None - - - (* transfer functions *) - let assign ctx (lval:lval) (rval:exp) : D.t = - let m = ctx.local in - (* ignore(printf "%a = %a\n" d_plainlval lval d_plainexp rval); *) - let saveOpened ?unknown:(unknown=false) k m = (* save maybe opened files in the domain to warn about maybe unclosed files at the end *) - if D.may k D.opened m && not (D.is_unknown k m) then (* if unknown we don't have any location for the warning and have handled it already anyway *) - let mustOpen, mayOpen = D.filter_records k D.opened m in - let mustOpen, mayOpen = if unknown then Set.empty, mayOpen else mustOpen, Set.diff mayOpen mustOpen in - D.extend_value unclosed_var (mustOpen, mayOpen) m - else m - in - let key_from_exp = function - | Lval x -> Some (D.key_from_lval x) - | _ -> None - in - match key_from_exp (Lval lval), key_from_exp (stripCasts rval) with (* we just care about Lval assignments *) - | Some k1, Some k2 when k1=k2 -> m (* do nothing on self-assignment *) - | Some k1, Some k2 when D.mem k1 m && D.mem k2 m -> (* both in D *) - if M.tracing then M.tracel "file" "assign (both in D): %s = %s" (D.string_of_key k1) (D.string_of_key k2); - saveOpened k1 m |> D.remove' k1 |> D.alias k1 k2 - | Some k1, Some k2 when D.mem k1 m -> (* only k1 in D *) - if M.tracing then M.tracel "file" "assign (only k1 in D): %s = %s" (D.string_of_key k1) (D.string_of_key k2); - saveOpened k1 m |> D.remove' k1 - | Some k1, Some k2 when D.mem k2 m -> (* only k2 in D *) - if M.tracing then M.tracel "file" "assign (only k2 in D): %s = %s" (D.string_of_key k1) (D.string_of_key k2); - D.alias k1 k2 m - | Some k1, _ when D.mem k1 m -> (* k1 in D and assign something unknown *) - if M.tracing then M.tracel "file" "assign (only k1 in D): %s = %a" (D.string_of_key k1) d_exp rval; - D.warn @@ "[Unsound]changed pointer "^D.string_of_key k1^" (no longer safe)"; - saveOpened ~unknown:true k1 m |> D.unknown k1 - | _ -> (* no change in D for other things *) - if M.tracing then M.tracel "file" "assign (none in D): %a = %a [%a]" d_lval lval d_exp rval d_plainexp rval; - m - - let branch ctx (exp:exp) (tv:bool) : D.t = - let m = ctx.local in - (* ignore(printf "if %a = %B (line %i)\n" d_plainexp exp tv (!Tracing.current_loc).line); *) - let check a b tv = - (* ignore(printf "check: %a = %a, %B\n" d_plainexp a d_plainexp b tv); *) - match a, b with - | Const (CInt(i, kind, str)), Lval lval - | Lval lval, Const (CInt(i, kind, str)) -> - (* ignore(printf "branch(%s==%i, %B)\n" v.vname (Int64.to_int i) tv); *) - let k = D.key_from_lval lval in - if Z.compare i Z.zero = 0 && tv then ( - (* ignore(printf "error-branch\n"); *) - D.error k m - )else - D.success k m - | _ -> M.debug ~category:Analyzer "nothing matched the given BinOp: %a = %a" d_plainexp a d_plainexp b; m - in - match stripCasts (constFold true exp) with - (* somehow there are a lot of casts inside the BinOp which stripCasts only removes when called on the subparts - -> matching as in flagMode didn't work *) - (* | BinOp (Eq, Const (CInt64(i, kind, str)), Lval (Var v, NoOffset), _) - | BinOp (Eq, Lval (Var v, NoOffset), Const (CInt64(i, kind, str)), _) -> - ignore(printf "%s %i\n" v.vname (Int64.to_int i)); m *) - | BinOp (Eq, a, b, _) -> check (stripCasts a) (stripCasts b) tv - | BinOp (Ne, a, b, _) -> check (stripCasts a) (stripCasts b) (not tv) - | e -> M.debug ~category:Analyzer "branch: nothing matched the given exp: %a" d_plainexp e; m - - let body ctx (f:fundec) : D.t = - ctx.local - - let return ctx (exp:exp option) (f:fundec) : D.t = - (* TODO check One Return transformation: oneret.ml *) - let m = ctx.local in - (* if f.svar.vname <> "main" && BatList.is_empty (callstack m) then M.write ("\n\t!!! call stack is empty for function "^f.svar.vname^" !!!"); *) - if f.svar.vname = "main" then ( - let mustOpen, mayOpen = D.union (D.filter_values D.opened m) (D.get_value unclosed_var m) in - if Set.cardinal mustOpen > 0 then ( - D.warn @@ "unclosed files: "^D.string_of_keys mustOpen; - Set.iter (fun v -> D.warn ~loc:(D.V.loc v) "file is never closed") mustOpen; - (* add warnings about currently open files (don't include overwritten or changed file handles!) *) - warned_unclosed := Set.union !warned_unclosed (fst (D.filter_values D.opened m)) (* can't save in domain b/c it wouldn't reach the other return *) - ); - (* go through files "never closed" and recheck for current return *) - Set.iter (fun v -> if D.must (D.V.key v) D.closed m then D.warn ~may:true ~loc:(D.V.loc v) "file is never closed") !warned_unclosed; - (* let mustOpenVars = List.map (fun x -> x.key) mustOpen in *) - (* let mayOpen = List.filter (fun x -> not (List.mem x.key mustOpenVars)) mayOpen in (* ignore values that are already in mustOpen *) *) - let mayOpen = Set.diff mayOpen mustOpen in - if Set.cardinal mayOpen > 0 then - D.warn ~may:true @@ "unclosed files: "^D.string_of_keys mayOpen; - Set.iter (fun v -> D.warn ~may:true ~loc:(D.V.loc v) "file is never closed") mayOpen - ); - (* take care of return value *) - let au = match exp with - | Some(Lval lval) when D.mem (D.key_from_lval lval) m -> (* we return a var in D *) - let k = D.key_from_lval lval in - let varinfo,offset = k in - if varinfo.vglob then - D.alias return_var k m (* if var is global, we alias it *) - else - D.add return_var (D.find' k m) m (* if var is local, we make a copy *) - | _ -> m - in - (* remove formals and locals *) - (* this is not a good approach, what if we added a key foo.fp? -> just keep the globals *) - List.fold_left (fun m var -> D.remove' (var, `NoOffset) m) au (f.sformals @ f.slocals) - (* D.only_globals au *) - - let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - let m = if f.svar.vname <> "main" then - (* push current location onto stack *) - D.edit_callstack (BatList.cons (Option.get !Node.current_node)) ctx.local - else ctx.local in - (* we need to remove all variables that are neither globals nor special variables from the domain for f *) - (* problem: we need to be able to check aliases of globals in check_overwrite_open -> keep those in too :/ *) - (* TODO see Base.make_entry, reachable vars > globals? *) - (* [m, D.only_globals m] *) - [m, m] (* this is [caller, callee] *) - - let check_overwrite_open k m = (* used in combine and special *) - if List.is_empty (D.get_aliases k m) then ( - (* there are no other variables pointing to the file handle - and it is opened again without being closed before *) - D.report k D.opened ("overwriting still opened file handle "^D.string_of_key k) m; - let mustOpen, mayOpen = D.filter_records k D.opened m in - let mayOpen = Set.diff mayOpen mustOpen in - (* save opened files in the domain to warn about unclosed files at the end *) - D.extend_value unclosed_var (mustOpen, mayOpen) m - ) else m - - let combine_env ctx lval fexp f args fc au f_ask = - let m = ctx.local in - (* pop the last location off the stack *) - let m = D.edit_callstack List.tl m in (* TODO could it be problematic to keep this in the caller instead of callee domain? if we only add the stack for the callee in enter, then there would be no need to pop a location anymore... *) - (* TODO add all globals from au to m (since we remove formals and locals on return, we can just add everything except special vars?) *) - D.without_special_vars au |> D.add_all m - - let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t = - let m = ctx.local in - let return_val = D.find_option return_var au in - match lval, return_val with - | Some lval, Some v -> - let k = D.key_from_lval lval in - (* handle potential overwrites *) - let m = check_overwrite_open k m in - (* if v.key is still in D, then it must be a global and we need to alias instead of rebind *) - (* TODO what if there is a local with the same name as the global? *) - if D.V.is_top v then (* returned a local that was top -> just add k as top *) - D.add' k v m - else (* v is now a local which is not top or a global which is aliased *) - let vvar = D.V.get_alias v in (* this is also ok if v is not an alias since it chooses an element from the May-Set which is never empty (global top gets aliased) *) - if D.mem vvar au then (* returned variable was a global TODO what if local had the same name? -> seems to work *) - D.alias k vvar m - else (* returned variable was a local *) - let v = D.V.set_key k v in (* adjust var-field to lval *) - D.add' k v m - | _ -> m - - let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = - (* is f a pointer to a function we look out for? *) - let f = eval_fv (Analyses.ask_of_ctx ctx) (Lval (Var f, NoOffset)) |? f in - let m = ctx.local in - let loc = (Option.get !Node.current_node)::(D.callstack m) in - let arglist = List.map (Cil.stripCasts) arglist in (* remove casts, TODO safe? *) - let split_err_branch lval dom = - (* type? NULL = 0 = 0-ptr? Cil.intType, Cil.intPtrType, Cil.voidPtrType -> no difference *) - if not (GobConfig.get_bool "ana.file.optimistic") then - ctx.split dom [Events.SplitBranch ((Cil.BinOp (Cil.Eq, Cil.Lval lval, Cil.integer 0, Cil.intType)), true)]; - dom - in - (* fold possible keys on domain *) - let ret_all f lval = - let xs = D.keys_from_lval lval (Analyses.ask_of_ctx ctx) in (* get all possible keys for a given lval *) - if xs = [] then (D.warn @@ GobPretty.sprintf "could not resolve %a" CilType.Lval.pretty lval; m) - else if List.compare_length_with xs 1 = 0 then f (List.hd xs) m true - (* else List.fold_left (fun m k -> D.join m (f k m)) m xs *) - else - (* if there is more than one key, join all values and do warnings on the result *) - let v = List.fold_left (fun v k -> match v, D.find_option k m with - | None, None -> None - | Some a, None - | None, Some a -> Some a - | Some a, Some b -> Some (D.V.join a b)) None xs in - (* set all of the keys to the computed joined value *) - (* let m' = Option.map_default (fun v -> List.fold_left (fun m k -> D.add' k v m) m xs) m v in *) - (* then check each key *) - (* List.iter (fun k -> ignore(f k m')) xs; *) - (* get Mval.Exp from lval *) - let k' = D.key_from_lval lval in - (* add joined value for that key *) - let m' = Option.map_default (fun v -> D.add' k' v m) m v in - (* check for warnings *) - ignore(f k' m' true); - (* and join the old domain without issuing warnings *) - List.fold_left (fun m k -> D.join m (f k m false)) m xs - in - match lval, f.vname, arglist with - | None, "fopen", _ -> - D.warn "file handle is not saved!"; m - | Some lval, "fopen", _ -> - let f k m w = - let m = check_overwrite_open k m in - (match arglist with - | Const(CStr(filename,_))::Const(CStr(mode,_))::[] -> - (* M.debug ~category:Analyzer @@ "fopen(\""^filename^"\", \""^mode^"\")"; *) - D.fopen k loc filename mode m |> split_err_branch lval (* TODO k instead of lval? *) - | e::Const(CStr(mode,_))::[] -> - (* ignore(printf "CIL: %a\n" d_plainexp e); *) - (match ctx.ask (Queries.EvalStr e) with - | `Lifted filename -> D.fopen k loc filename mode m - | _ -> D.warn "[Unsound]unknown filename"; D.fopen k loc "???" mode m - ) - | xs -> - let args = (String.concat ", " (List.map CilType.Exp.show xs)) in - M.debug ~category:Analyzer "fopen args: %s" args; - (* List.iter (fun exp -> ignore(printf "%a\n" d_plainexp exp)) xs; *) - D.warn @@ "[Program]fopen needs two strings as arguments, given: "^args; m - ) - in ret_all f lval - - | _, "fclose", [Lval fp] -> - let f k m w = - if w then D.reports k [ - false, D.closed, "closeing already closed file handle "^D.string_of_key k; - true, D.opened, "closeing unopened file handle "^D.string_of_key k - ] m; - D.fclose k loc m - in ret_all f fp - | _, "fclose", _ -> - D.warn "fclose needs exactly one argument"; m - - | _, "fprintf", (Lval fp)::_::_ -> - let f k m w = - if w then D.reports k [ - false, D.closed, "writing to closed file handle "^D.string_of_key k; - true, D.opened, "writing to unopened file handle "^D.string_of_key k; - true, D.writable, "writing to read-only file handle "^D.string_of_key k; - ] m; - m - in ret_all f fp - | _, "fprintf", fp::_::_ -> - (* List.iter (fun exp -> ignore(printf "%a\n" d_plainexp exp)) arglist; *) - print_query_lv ~msg:"fprintf(?, ...): " (Analyses.ask_of_ctx ctx) fp; - D.warn "[Program]first argument to printf must be a Lval"; m - | _, "fprintf", _ -> - D.warn "[Program]fprintf needs at least two arguments"; m - - | _ -> m - - let startstate v = D.bot () - let threadenter ctx ~multiple lval f args = [D.bot ()] - let threadspawn ctx ~multiple lval f args fctx = ctx.local - let exitstate v = D.bot () -end - -let _ = - MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/mCPRegistry.ml b/src/analyses/mCPRegistry.ml index 810da827ff..5d0174d44c 100644 --- a/src/analyses/mCPRegistry.ml +++ b/src/analyses/mCPRegistry.ml @@ -215,7 +215,7 @@ struct let arbitrary () = let arbs = map (fun (n, (module D: Printable.S)) -> QCheck.map ~rev:(fun (_, o) -> obj o) (fun x -> (n, repr x)) @@ D.arbitrary ()) @@ domain_list () in - MyCheck.Arbitrary.sequence arbs + GobQCheck.Arbitrary.sequence arbs let relift = unop_map (fun (module S: Printable.S) x -> Obj.repr (S.relift (Obj.obj x))) end diff --git a/src/analyses/memLeak.ml b/src/analyses/memLeak.ml index 1253cd6763..456d434be7 100644 --- a/src/analyses/memLeak.ml +++ b/src/analyses/memLeak.ml @@ -228,23 +228,20 @@ struct warn_for_multi_threaded_due_to_abort ctx; state | Assert { exp; _ } -> - let warn_for_assert_exp = - match ctx.ask (Queries.EvalInt exp) with + begin match ctx.ask (Queries.EvalInt exp) with | a when Queries.ID.is_bot a -> M.warn ~category:Assert "assert expression %a is bottom" d_exp exp | a -> begin match Queries.ID.to_bool a with - | Some b -> + | Some true -> () + | Some false -> (* If we know for sure that the expression in "assert" is false => need to check for memory leaks *) - if b = false then ( - warn_for_multi_threaded_due_to_abort ctx; - check_for_mem_leak ctx - ) + warn_for_multi_threaded_due_to_abort ctx; + check_for_mem_leak ctx | None -> warn_for_multi_threaded_due_to_abort ctx; check_for_mem_leak ctx ~assert_exp_imprecise:true ~exp:(Some exp) end - in - warn_for_assert_exp; + end; state | ThreadExit _ -> begin match ctx.ask (Queries.CurrentThreadId) with diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceSetjmp.ml similarity index 96% rename from src/analyses/modifiedSinceLongjmp.ml rename to src/analyses/modifiedSinceSetjmp.ml index a129c9f92c..93e55b2a17 100644 --- a/src/analyses/modifiedSinceLongjmp.ml +++ b/src/analyses/modifiedSinceSetjmp.ml @@ -1,6 +1,4 @@ -(** Analysis of variables modified since [setjmp] ([modifiedSinceLongjmp]). *) - -(* TODO: this name is wrong *) +(** Analysis of variables modified since [setjmp] ([modifiedSinceSetjmp]). *) open GoblintCil open Analyses @@ -9,7 +7,7 @@ module Spec = struct include Analyses.IdentitySpec - let name () = "modifiedSinceLongjmp" + let name () = "modifiedSinceSetjmp" module D = JmpBufDomain.LocallyModifiedMap module VS = D.VarSet module C = Lattice.Unit diff --git a/src/analyses/spec.ml b/src/analyses/spec.ml deleted file mode 100644 index 2f754f6160..0000000000 --- a/src/analyses/spec.ml +++ /dev/null @@ -1,496 +0,0 @@ -(** Analysis using finite automaton specification file ([spec]). - - @author Ralf Vogler - - @see Vogler, R. Verifying Regular Safety Properties of C Programs Using the Static Analyzer Goblint. Section 4. *) - -open Batteries -open GoblintCil -open Analyses - -module SC = SpecCore - -module Spec = -struct - include Analyses.DefaultSpec - - let name() = "spec" - module D = SpecDomain.Dom - module C = SpecDomain.Dom - - (* special variables *) - let return_var = Cilfacade.create_var @@ Cil.makeVarinfo false "@return" Cil.voidType, `NoOffset - let global_var = Cilfacade.create_var @@ Cil.makeVarinfo false "@global" Cil.voidType, `NoOffset - - (* spec data *) - let nodes = ref [] - let edges = ref [] - - let load_specfile () = - let specfile = GobConfig.get_string "ana.spec.file" in - if String.length specfile < 1 then failwith "You need to specify a specification file using --set ana.spec.file path/to/file.spec when using the spec analysis!"; - if not (Sys.file_exists specfile) then failwith @@ "The given spec-file ("^specfile^") doesn't exist (CWD is "^Sys.getcwd ()^")."; - let _nodes, _edges = SpecUtil.parseFile specfile in - nodes := _nodes; edges := _edges (* don't change -> no need to save them in domain *) - - (* module for encapsulating general spec checking functions used in multiple transfer functions (assign, special) *) - (* - .spec-format: - - The file contains two types of definitions: nodes and edges. The labels of nodes are output. The labels of edges are the constraints. - - The given nodes are warnings, which have an implicit back edge to the previous node if used as a target. - - Alternatively warnings can be specified like this: "node1 -w1,w2,w3> node2 ...1" (w1, w2 and w3 will be output when the transition is taken). - - The start node of the first transition is the start node of the automaton. - - End nodes are specified by "node -> end _". - - "_end" is the local warning for nodes that are not in an end state, _END is the warning at return ($ is the list of keys). - - An edge with '_' matches everything. - - Edges with "->>" (or "-w1,w2>>" etc.) are forwarding edges, which will continue matching the same statement for the target node. - *) - module SpecCheck = - struct - (* custom goto (D.goto is just for modifying) that checks if the target state is a warning and acts accordingly *) - let goto ?may:(may=false) ?change_state:(change_state=true) key state m ws = - let loc = (Option.get !Node.current_node)::(D.callstack m) in - let warn key m msg = - Str.global_replace (Str.regexp_string "$") (D.string_of_key key) msg - |> D.warn ~may:(D.is_may key m || D.is_unknown key m) - in - (* do transition warnings *) - List.iter (fun state -> match SC.warning state !nodes with Some msg -> warn key m msg | _ -> ()) ws; - match SC.warning state !nodes with - | Some msg -> - warn key m msg; - m (* no goto == implicit back edge *) - | None -> - M.debug ~category:Analyzer "GOTO %s: %s -> %s" (D.string_of_key key) (D.string_of_state key m) state; - if not change_state then m - else if may then D.may_goto key loc state m else D.goto key loc state m - - let equal_exp ctx spec_exp cil_exp = match spec_exp, cil_exp with - (* TODO match constants right away to avoid queries? *) - | `String a, Const(CStr (b,_)) -> a=b - (* | `String a, Const(CWStr xs as c) -> failwith "not implemented" *) - (* CWStr is done in base.ml, query only returns `Str if it's safe *) - | `String a, e -> (match ctx.ask (Queries.EvalStr e) with - | `Lifted b -> a = b - | _ -> M.debug ~category:Analyzer "EQUAL String Query: no result!"; false - ) - | `Regex a, e -> (match ctx.ask (Queries.EvalStr e) with - | `Lifted b -> Str.string_match (Str.regexp a) b 0 - | _ -> M.debug ~category:Analyzer "EQUAL Regex String Query: no result!"; false - ) - | `Bool a, e -> (match ctx.ask (Queries.EvalInt e) with - | b -> (match Queries.ID.to_bool b with Some b -> a=b | None -> false) - ) - | `Int a, e -> (match ctx.ask (Queries.EvalInt e) with - | b -> (match Queries.ID.to_int b with Some b -> (Int64.of_int a)=(IntOps.BigIntOps.to_int64 b) | None -> false) - ) - | `Float a, Const(CReal (b, fkind, str_opt)) -> a=b - | `Float a, _ -> M.debug ~category:Analyzer "EQUAL Float: unsupported!"; false - (* arg is a key. currently there can only be one key per constraint, so we already used it for lookup. TODO multiple keys? *) - | `Var a, b -> true - (* arg is a identifier we use for matching constraints. TODO save in domain *) - | `Ident a, b -> true - | `Error s, b -> failwith @@ "Spec error: "^s - (* wildcard matches anything *) - | `Free, b -> true - | a,b -> M.info ~category:Unsound "EQUAL? Unmatched case - assume true..."; true - - let check_constraint ctx get_key matches m new_a old_key (a,ws,fwd,b,c as edge) = - (* If we have come to a wildcard, we match it instantly, but since there is no way of determining a key - this only makes sense if fwd is true (TODO wildcard for global. TODO use old_key). We pass a state replacement as 'new_a', - which will be applied in the following checks. - Multiple forwarding wildcards are not allowed, i.e. new_a must be None, otherwise we end up in a loop. *) - if SC.is_wildcard c && fwd && new_a=None then Some (m,fwd,Some (b,a),old_key) (* replace b with a in the following checks *) - else - (* save original start state of the constraint (needed to detect reflexive edges) *) - let old_a = a in - (* Assume new_a *) - let a = match new_a with - | Some (x,y) when a=x -> y - | _ -> a - in - (* if we forward, we have to replace the starting state for the following constraints *) - let new_a = if fwd then Some (b,a) else None in - (* TODO how to detect the key?? use "$foo" as key, "foo" as var in constraint and "_" for anything we're not interested in. - What to do for multiple keys (e.g. $foo, $bar)? -> Only allow one key & one map per spec-file (e.g. only $ as a key) or implement multiple maps? *) - (* look inside the constraint if there is a key and if yes, return what it corresponds to *) - (* if we can't find a matching key, we use the global key *) - let key = get_key c |? Cil.var (fst global_var) in - (* ignore(printf "KEY: %a\n" d_plainlval key); *) - (* get possible keys that &lval may point to *) - let keys = D.keys_from_lval key (Analyses.ask_of_ctx ctx) in (* does MayPointTo query *) - let check_key (m,n) var = - (* M.debug ~category:Analyzer @@ "check_key: "^f.vname^"(...): "^D.string_of_entry var m; *) - let wildcard = SC.is_wildcard c && fwd && b<>"end" in - (* skip transitions we can't take b/c we're not in the right state *) - (* i.e. if not in map, we must be at the start node or otherwise we must be in one of the possible saved states *) - if not (D.mem var m) && a<>SC.startnode !edges || D.mem var m && not (D.may_in_state var a m) then ( - (* ignore(printf "SKIP %s: state: %s, a: %s at %i\n" f.vname (D.string_of_state var m) a (!Tracing.current_loc.line)); *) - (m,n) (* not in map -> initial state. TODO save initial state? *) - ) - (* edge must match the current state or be a wildcard transition (except those for end) *) - else if not (matches edge) && not wildcard then (m,n) - (* everything matches the constraint -> go to new state and increase counter *) - else - (* TODO if #Queries.MayPointTo > 1: each result is May, but all combined are Must *) - let may = (List.compare_length_with keys 1 > 0) in - (* do not change state for reflexive edges where the key is not assigned to (e.g. *$p = _) *) - let change_state = not (old_a=b && SC.get_lval c <> Some `Var) in - M.debug ~category:Analyzer "GOTO ~may:%B ~change_state:%B. %s -> %s: %s" may change_state a b (SC.stmt_to_string c); - let new_m = goto ~may:may ~change_state:change_state var b m ws in - (new_m,n+1) - in - (* do check for each varinfo and return the resulting domain if there has been at least one matching constraint *) - let new_m,n = List.fold_left check_key (m,0) keys in (* start with original domain and #transitions=0 *) - if n==0 then None (* no constraint matched the current state *) - else Some (new_m,fwd,new_a,Some key) (* return new domain and forwarding info *) - - let check ctx get_key matches = - let m = ctx.local in - (* go through constraints and return resulting domain for the first match *) - (* if no constraint matches, the unchanged domain is returned *) - (* repeat for target node if it is a forwarding edge *) - (* TODO what should be done if multiple constraints would match? *) - (* TODO ^^ for May-Sets multiple constraints could match and should be taken! *) - try - let rec check_fwd_loop m new_a old_key = (* TODO cycle detection? *) - let new_m,fwd,new_a,key = List.find_map (check_constraint ctx get_key matches m new_a old_key) !edges in - (* List.iter (fun x -> M.debug ~category:Analyzer (x^"\n")) (D.string_of_map new_m); *) - if fwd then M.debug ~category:Analyzer "FWD: %B, new_a: %s, old_key: %s" fwd (dump new_a) (dump old_key); - if fwd then check_fwd_loop new_m new_a key else new_m,key - in - (* now we get the new domain and the latest key that was used *) - let new_m,key = check_fwd_loop m None None in - (* List.iter (fun x -> M.debug ~category:Analyzer (x^"\n")) (D.string_of_map new_m); *) - (* next we have to check if there is a branch() transition we could take *) - let branch_edges = List.filter (fun (a,ws,fwd,b,c) -> SC.is_branch c) !edges in - (* just for the compiler: key is initialized with None, but changes once some constaint matches. If none match, we wouldn't be here but at catch Not_found. *) - match key with - | Some key -> - (* we need to pass the key to the branch function. There is no scheme for getting the key from the constraint, but we should have been forwarded and can use the old key. *) - let check_branch branches var = - (* only keep those branch_edges for which our key might be in the right state *) - let branch_edges = List.filter (fun (a,ws,fwd,b,c) -> D.may_in_state var a new_m) branch_edges in - (* M.debug ~category:Analyzer @@ D.string_of_entry var new_m^" -> branch_edges: "^String.concat "\n " @@ List.map (fun x -> SC.def_to_string (SC.Edge x)) branch_edges; *) - (* count should be a multiple of 2 (true/false), otherwise the spec is malformed *) - if List.length branch_edges mod 2 <> 0 then failwith "Spec is malformed: branch-transitions always need a true and a false case!" else - (* if nothing matches, just return new_m without branching *) - (* if List.is_empty branch_edges then Set.of_list new_m else *) - if List.is_empty branch_edges then Set.of_list ([new_m, Cil.integer 1, true]) else (* XX *) - (* unique set of (dom,exp,tv) used in branch *) - let do_branch branches (a,ws,fwd,b,c) = - let c_str = match SC.branch_exp c with Some (exp,tv) -> SC.exp_to_string exp | _ -> "" in - let c_str = Str.global_replace (Str.regexp_string "$key") "%e:key" c_str in (* TODO what should be used to specify the key? *) - (* TODO this somehow also prints the expression!? why?? *) - let c_exp = Formatcil.cExp c_str [("key", Fe (D.K.to_cil_exp var))] in (* use Fl for Lval instead? *) - (* TODO encode key in exp somehow *) - (* ignore(printf "BRANCH %a\n" d_plainexp c_exp); *) - ctx.split new_m [Events.SplitBranch (c_exp, true)]; - Set.add (new_m,c_exp,true) (Set.add (new_m,c_exp,false) branches) - in - List.fold_left do_branch branches branch_edges - in - let keys = D.keys_from_lval key (Analyses.ask_of_ctx ctx) in - let new_set = List.fold_left check_branch Set.empty keys in ignore(new_set); (* TODO refactor *) - (* List.of_enum (Set.enum new_set) *) - new_m (* XX *) - | None -> new_m - with Not_found -> m (* nothing matched -> no change *) - end - - (* queries *) - let query ctx (type a) (q: a Queries.t) = - match q with - | _ -> Queries.Result.top q - - let query_addrs ask exp = - match ask (Queries.MayPointTo exp) with - | ad when not (Queries.AD.is_top ad) -> Queries.AD.elements ad - | _ -> [] - - let eval_fv ask exp: varinfo option = - match query_addrs ask exp with - | [addr] -> Queries.AD.Addr.to_var_may addr - | _ -> None - - - (* transfer functions *) - let assign ctx (lval:lval) (rval:exp) : D.t = - (* ignore(printf "%a = %a\n" d_plainlval lval d_plainexp rval); *) - let get_key c = match SC.get_key_variant c with - | `Lval s -> - M.debug ~category:Analyzer "Key variant assign `Lval %s; %s" s (SC.stmt_to_string c); - (match SC.get_lval c, lval with - | Some `Var, _ -> Some lval - | Some `Ptr, (Mem Lval x, o) -> Some x (* TODO offset? *) - | _ -> None) - | _ -> None - in - let matches (a,ws,fwd,b,c) = - SC.equal_form (Some lval) c && - (* check for constraints *p = _ where p is the key *) - match lval, SC.get_lval c with - | (Mem Lval x, o), Some `Ptr when SpecCheck.equal_exp ctx (SC.get_rval c) rval -> - let keys = D.keys_from_lval x (Analyses.ask_of_ctx ctx) in - if List.compare_length_with keys 1 <> 0 then failwith "not implemented" - else true - | _ -> false (* nothing to do *) - in - let m = SpecCheck.check ctx get_key matches in - let key_from_exp = function - | Lval (Var v,o) -> Some (v, Offset.Exp.of_cil o) - | _ -> None - in - match key_from_exp (Lval lval), key_from_exp (stripCasts rval) with (* TODO for now we just care about Lval assignments -> should use Queries.MayPointTo *) - | Some k1, Some k2 when k1=k2 -> m (* do nothing on self-assignment *) - | Some k1, Some k2 when D.mem k1 m && D.mem k2 m -> (* both in D *) - M.debug ~category:Analyzer "assign (both in D): %s = %s" (D.string_of_key k1) (D.string_of_key k2); - (* saveOpened k1 *) m |> D.remove' k1 |> D.alias k1 k2 - | Some k1, Some k2 when D.mem k1 m -> (* only k1 in D *) - M.debug ~category:Analyzer "assign (only k1 in D): %s = %s" (D.string_of_key k1) (D.string_of_key k2); - (* saveOpened k1 *) m |> D.remove' k1 - | Some k1, Some k2 when D.mem k2 m -> (* only k2 in D *) - M.debug ~category:Analyzer "assign (only k2 in D): %s = %s" (D.string_of_key k1) (D.string_of_key k2); - let m = D.alias k1 k2 m in (* point k1 to k2 *) - if Basetype.Variables.to_group (fst k2) = Temp (* check if k2 is a temporary Lval introduced by CIL *) - then D.remove' k2 m (* if yes we need to remove it from our map *) - else m (* otherwise no change *) - | Some k1, _ when D.mem k1 m -> (* k1 in D and assign something unknown *) - M.debug ~category:Analyzer "assign (only k1 in D): %s = %a" (D.string_of_key k1) d_exp rval; - D.warn @@ "changed pointer "^D.string_of_key k1^" (no longer safe)"; - (* saveOpened ~unknown:true k1 *) m |> D.unknown k1 - | _ -> (* no change in D for other things *) - M.debug ~category:Analyzer "assign (none in D): %a = %a [%a]" d_lval lval d_exp rval d_plainexp rval; - m - - (* - - branch-transitions in the spec-file come in pairs: e.g. true-branch goes to node a, false-branch to node b - - branch is called for both possibilities - - TODO query the exp and take/don't take the transition - - in case of `Top we take the transition - - both branches get joined after (e.g. for fopen: May [open; error]) - - if there is a branch in the code, branch is also called - -> get the key from exp and backtrack to the corresponding branch-transitions - -> reevaluate with current exp and meet domain with result - *) - (* - - get key from exp - - ask EvalInt - - if result is `Top and we are in a state that is the starting node of a branch edge, we have to: - - go to target node and modify the state in specDomain - - find out which value of key makes exp equal to tv - - save this value and answer queries for EvalInt with it - - if not, compare it with tv and take the corresponding branch - *) - let branch ctx (exp:exp) (tv:bool) : D.t = - let m = ctx.local in - (* ignore(printf "if %a = %B (line %i)\n" d_plainexp exp tv (!Tracing.current_loc).line); *) - let check a b tv = - (* ignore(printf "check: %a = %a\n" d_plainexp a d_plainexp b); *) - match a, b with - | Const (CInt(i, kind, str)), Lval lval - | Lval lval, Const (CInt(i, kind, str)) -> - (* let binop = BinOp (Eq, a, b, Cil.intType) in *) - (* standardize the format of the expression to 'lval==i'. -> spec needs to follow that format, the code is mapped to it. *) - let binop = BinOp (Eq, Lval lval, Const (CInt(i, kind, str)), Cil.intType) in - let key = D.key_from_lval lval in - let value = D.find key m in - if Z.equal i Z.zero && tv then ( - M.debug ~category:Analyzer "error-branch"; - (* D.remove key m *) - )else( - M.debug ~category:Analyzer "success-branch"; - (* m *) - ); - (* there should always be an entry in our domain for key *) - if not (D.mem key m) then m else - (* TODO for now we just assume that a Binop is used and Lval is the key *) - (* get the state(s) that key is/might be in *) - let states = D.get_states key m in - (* compare SC.exp with Cil.exp and tv *) - let branch_exp_eq c exp tv = - (* let c_str = match SC.branch_exp c with Some (exp,tv) -> SC.exp_to_string exp | _ -> "" in - let c_str = Str.global_replace (Str.regexp_string "$key") "%e:key" c_str in - let c_exp = Formatcil.cExp c_str [("key", Fe (D.K.to_exp key))] in *) - (* c_exp=exp *) (* leads to Out_of_memory *) - match SC.branch_exp c with - | Some (c_exp,c_tv) -> - (* let exp_str = CilType.Exp.show exp in *) (* contains too many casts, so that matching fails *) - let exp_str = CilType.Exp.show binop in - let c_str = SC.exp_to_string c_exp in - let c_str = Str.global_replace (Str.regexp_string "$key") (D.string_of_key key) c_str in - (* ignore(printf "branch_exp_eq: '%s' '%s' -> %B\n" c_str exp_str (c_str=exp_str)); *) - c_str=exp_str && c_tv=tv - | _ -> false - in - (* filter those edges that are branches, start with a state from states and have the same branch expression and the same tv *) - let branch_edges = List.filter (fun (a,ws,fwd,b,c) -> SC.is_branch c && List.mem a states && branch_exp_eq c exp tv) !edges in - (* there should be only one such edge or none *) - if List.compare_length_with branch_edges 1 <> 0 then ( (* call of branch for an actual branch *) - M.debug ~category:Analyzer "branch: branch_edges length is not 1! -> actual branch"; - M.debug ~category:Analyzer "%s -> branch_edges1: %a" (D.string_of_entry key m) (Pretty.d_list "\n " (fun () x -> Pretty.text (SC.def_to_string (SC.Edge x)))) branch_edges; - (* filter those edges that are branches, end with a state from states have the same branch expression and the same tv *) - (* TODO they should end with any predecessor of the current state, not only the direct predecessor *) - let branch_edges = List.filter (fun (a,ws,fwd,b,c) -> SC.is_branch c && List.mem b states && branch_exp_eq c exp tv) !edges in - M.debug ~category:Analyzer "%s -> branch_edges2: %a" (D.string_of_entry key m) (Pretty.d_list "\n " (fun () x -> Pretty.text (SC.def_to_string (SC.Edge x)))) branch_edges; - if List.compare_length_with branch_edges 1 <> 0 then m else - (* meet current value with the target state. this is tricky: we can not simply take the target state, since there might have been more than one element already before the branching. - -> find out what the alternative branch target was and remove it *) - let (a,ws,fwd,b,c) = List.hd branch_edges in - (* the alternative branch has the same start node, the same branch expression and the negated tv *) - let (a,ws,fwd,b,c) = List.find (fun (a2,ws,fwd,b,c) -> SC.is_branch c && a2=a && branch_exp_eq c exp (not tv)) !edges in - (* now b is the state the alternative branch goes to -> remove it *) - (* TODO may etc. *) - (* being explicit: check how many records there are. if the value is Must b, then we're sure that it is so and we don't remove anything. *) - if D.V.length value = (1,1) then m else (* XX *) - (* there are multiple possible states -> remove b *) - let v2 = D.V.remove_state b value in - (* M.debug ~category:Analyzer @@ "branch: changed state from "^D.V.string_of value^" to "^D.V.string_of v2; *) - D.add key v2 m - ) else (* call of branch directly after splitting *) - let (a,ws,fwd,b,c) = List.hd branch_edges in - (* TODO may etc. *) - let v2 = D.V.set_state b value in - (* M.debug ~category:Analyzer @@ "branch: changed state from "^D.V.string_of value^" to "^D.V.string_of v2; *) - D.add key v2 m - | _ -> M.debug ~category:Analyzer "nothing matched the given BinOp: %a = %a" d_plainexp a d_plainexp b; m - in - match stripCasts (constFold true exp) with - (* somehow there are a lot of casts inside the BinOp which stripCasts only removes when called on the subparts - -> matching as in flagMode didn't work *) - | BinOp (Eq, a, b, _) -> check (stripCasts a) (stripCasts b) tv - | BinOp (Ne, a, b, _) -> check (stripCasts a) (stripCasts b) (not tv) - | UnOp (LNot, a, _) -> check (stripCasts a) (integer 0) tv - (* TODO makes 2 tests fail. probably check changes something it shouldn't *) - (* | Lval _ as a -> check (stripCasts a) (integer 0) (not tv) *) - | e -> M.debug ~category:Analyzer "branch: nothing matched the given exp: %a" d_plainexp e; m - - let body ctx (f:fundec) : D.t = - ctx.local - - let return ctx (exp:exp option) (f:fundec) : D.t = - let m = ctx.local in - (* M.debug ~category:Analyzer @@ "return: ctx.local="^D.short 50 m^D.string_of_callstack m; *) - (* if f.svar.vname <> "main" && BatList.is_empty (D.callstack m) then M.debug ~category:Analyzer @@ "\n\t!!! call stack is empty for function "^f.svar.vname^" !!!"; *) - if f.svar.vname = "main" then ( - let warn_main msg_loc msg_end = (* there is an end warning for local, return or both *) - (* find edges that have 'end' as a target *) - (* we ignore the constraint, TODO maybe find a better syntax for declaring end states *) - let end_states = BatList.filter_map (fun (a,ws,fwd,b,c) -> if b="end" then Some a else None) !edges in - let must_not, may_not = D.filter_values (fun r -> not @@ List.exists (fun end_state -> D.V.in_state end_state r) end_states) m in - let may_not = Set.diff may_not must_not in - (match msg_loc with (* local warnings for entries that must/may not be in an end state *) - | Some msg -> - Set.iter (fun r -> D.warn ~loc:(D.V.loc r) msg) must_not; - Set.iter (fun r -> D.warn ~may:true ~loc:(D.V.loc r) msg) may_not - | None -> ()); - (match msg_end with - | Some msg -> (* warnings at return for entries that must/may not be in an end state *) - let f msg rs = Str.global_replace (Str.regexp_string "$") (D.string_of_keys rs) msg in - if Set.cardinal must_not > 0 then D.warn (f msg must_not); - if Set.cardinal may_not > 0 then D.warn ~may:true (f msg may_not) - | _ -> ()) - in - (* check if there is a warning for entries that are not in an end state *) - match SC.warning "_end" !nodes, SC.warning "_END" !nodes with - | None, None -> () (* nothing to do here *) - | msg_loc,msg_end -> warn_main msg_loc msg_end - ); - (* take care of return value *) - let au = match exp with - | Some(Lval lval) when D.mem (D.key_from_lval lval) m -> (* we return a var in D *) - let k = D.key_from_lval lval in - let varinfo,offset = k in - if varinfo.vglob then - D.alias return_var k m (* if var is global, we alias it *) - else - D.add return_var (D.find' k m) m (* if var is local, we make a copy *) - | _ -> m - in - (* remove formals and locals *) - (* TODO only keep globals like in fileUse *) - List.fold_left (fun m var -> D.remove' (var, `NoOffset) m) au (f.sformals @ f.slocals) - - let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - (* M.debug ~category:Analyzer @@ "entering function "^f.vname^D.string_of_callstack ctx.local; *) - if f.svar.vname = "main" then load_specfile (); - let m = if f.svar.vname <> "main" then - D.edit_callstack (BatList.cons (Option.get !Node.current_node)) ctx.local - else ctx.local in [m, m] - - let combine_env ctx lval fexp f args fc au f_ask = - (* M.debug ~category:Analyzer @@ "leaving function "^f.vname^D.string_of_callstack au; *) - let au = D.edit_callstack List.tl au in - (* remove special return var *) - D.remove' return_var au - - let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t = - let return_val = D.find_option return_var au in - match lval, return_val with - | Some lval, Some v -> - let k = D.key_from_lval lval in - (* handle potential overwrites *) - (* |> check_overwrite_open k *) - (* if v.key is still in D, then it must be a global and we need to alias instead of rebind *) - (* TODO what if there is a local with the same name as the global? *) - if D.V.is_top v then (* returned a local that was top -> just add k as top *) - D.add' k v ctx.local - else (* v is now a local which is not top or a global which is aliased *) - let vvar = D.V.get_alias v in (* this is also ok if v is not an alias since it chooses an element from the May-Set which is never empty (global top gets aliased) *) - if D.mem vvar au then (* returned variable was a global TODO what if local had the same name? -> seems to work *) - (* let _ = M.debug ~category:Analyzer @@ vvar.vname^" was a global -> alias" in *) - D.alias k vvar ctx.local - else (* returned variable was a local *) - let v = D.V.set_key k v in (* adjust var-field to lval *) - (* M.debug ~category:Analyzer @@ vvar.vname^" was a local -> rebind"; *) - D.add' k v ctx.local - | _ -> ctx.local - - let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = - let arglist = List.map (Cil.stripCasts) arglist in (* remove casts, TODO safe? *) - let get_key c = match SC.get_key_variant c with - | `Lval s -> - M.debug ~category:Analyzer "Key variant special `Lval %s; %s" s (SC.stmt_to_string c); - lval - | `Arg(s, i) -> - M.debug ~category:Analyzer "Key variant special `Arg(%s, %d). %s" s i (SC.stmt_to_string c); - (try - let arg = List.at arglist i in - match arg with - | Lval x -> Some x (* TODO enough to just assume the arg is already there as a Lval? *) - | AddrOf x -> Some x - | _ -> None - with Invalid_argument s -> - M.debug ~category:Analyzer "Key out of bounds! Msg: %s" s; (* TODO what to do if spec says that there should be more args... *) - None - ) - | _ -> None (* `Rval or `None *) - in - let matches (a,ws,fwd,b,c) = - let equal_args spec_args cil_args = - if List.compare_length_with spec_args 1 = 0 && List.hd spec_args = `Free then - true (* wildcard as an argument matches everything *) - else if List.compare_lengths arglist spec_args <> 0 then ( - M.debug ~category:Analyzer "SKIP the number of arguments doesn't match the specification!"; - false - )else - List.for_all2 (SpecCheck.equal_exp ctx) spec_args cil_args (* TODO Cil.constFold true arg. Test: Spec and c-file: 1+1 *) - in - (* function name must fit the constraint *) - SC.fname_is f.vname c && - (* right form (assignment or not) *) - SC.equal_form lval c && - (* function arguments match those of the constraint *) - equal_args (SC.get_fun_args c) arglist - in - SpecCheck.check ctx get_key matches - - - let startstate v = D.bot () - let threadenter ctx ~multiple lval f args = [D.bot ()] - let threadspawn ctx ~multiple lval f args fctx = ctx.local - let exitstate v = D.bot () -end - -let _ = - MCP.register_analysis (module Spec : MCPSpec) diff --git a/src/analyses/stackTrace.ml b/src/analyses/stackTrace.ml index 3c3bd56640..dd2cedf871 100644 --- a/src/analyses/stackTrace.ml +++ b/src/analyses/stackTrace.ml @@ -36,7 +36,7 @@ struct (* transfer functions *) let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list = - [ctx.local, D.push !Tracing.current_loc ctx.local] + [ctx.local, D.push !Goblint_tracing.current_loc ctx.local] let combine_env ctx lval fexp f args fc au f_ask = ctx.local (* keep local as opposed to IdentitySpec *) @@ -46,7 +46,7 @@ struct let exitstate v = D.top () let threadenter ctx ~multiple lval f args = - [D.push !Tracing.current_loc ctx.local] + [D.push !Goblint_tracing.current_loc ctx.local] end diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index 01c5dd87fa..ed30e3633e 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -57,16 +57,18 @@ struct | ThreadJoin { thread = id; ret_var } -> (* TODO: generalize ThreadJoin like ThreadCreate *) (let has_clean_exit tid = not (BatTuple.Tuple3.third (ctx.global tid)) in + let tids = ctx.ask (Queries.EvalThread id) in let join_thread s tid = if has_clean_exit tid && not (is_not_unique ctx tid) then D.remove tid s else s in - match TS.elements (ctx.ask (Queries.EvalThread id)) with - | [t] -> join_thread ctx.local t (* single thread *) - | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *) - | exception SetDomain.Unsupported _ -> ctx.local) + if TS.is_top tids + then ctx.local + else match TS.elements tids with + | [t] -> join_thread ctx.local t (* single thread *) + | _ -> ctx.local (* if several possible threads are may-joined, none are must-joined *)) | ThreadExit { ret_val } -> handle_thread_return ctx (Some ret_val); ctx.local diff --git a/src/analyses/threadJoins.ml b/src/analyses/threadJoins.ml index 862711073c..160b123e78 100644 --- a/src/analyses/threadJoins.ml +++ b/src/analyses/threadJoins.ml @@ -52,7 +52,7 @@ struct if TIDs.is_top threads then ctx.local else ( - (* elements throws if the thread set is top *) + (* all elements are known *) let threads = TIDs.elements threads in match threads with | [tid] when TID.is_unique tid-> @@ -70,7 +70,7 @@ struct (MustTIDs.bot(), true) (* consider everything joined, MustTIDs is reversed so bot is All threads *) ) else ( - (* elements throws if the thread set is top *) + (* all elements are known *) let threads = TIDs.elements threads in if List.compare_length_with threads 1 > 0 then M.info ~category:Unsound "Ambiguous thread ID assume-joined, assuming all of those threads must-joined."; diff --git a/src/analyses/useAfterFree.ml b/src/analyses/useAfterFree.ml index a901a8d2e5..69db6b4bfa 100644 --- a/src/analyses/useAfterFree.ml +++ b/src/analyses/useAfterFree.ml @@ -76,7 +76,7 @@ struct end else if HeapVars.mem heap_var (snd ctx.local) then begin if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref; - M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.FlagConfiguredTID.pretty current CilType.Varinfo.pretty heap_var + M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "%s might occur in current unique thread %a for heap variable %a" bug_name ThreadIdDomain.Thread.pretty current CilType.Varinfo.pretty heap_var end end | `Top -> diff --git a/src/autoTune.ml b/src/autoTune.ml index 0c3d3727f0..3cda36a302 100644 --- a/src/autoTune.ml +++ b/src/autoTune.ml @@ -200,7 +200,7 @@ let reduceThreadAnalyses () = (* This is run independent of the autotuner being enabled or not to be sound in the presence of setjmp/longjmp *) (* It is done this way around to allow enabling some of these analyses also for programs without longjmp *) -let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceLongjmp"; "poisonVariables"; "expsplit"; "vla"] +let longjmpAnalyses = ["activeLongjmp"; "activeSetjmp"; "taintPartialContexts"; "modifiedSinceSetjmp"; "poisonVariables"; "expsplit"; "vla"] let activateLongjmpAnalysesWhenRequired () = let isLongjmp = function diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index a6f00fdba0..5aa1090dd4 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -10,7 +10,7 @@ open Batteries open GoblintCil open Pretty module M = Messages -open Apron +open GobApron open VectorMatrix module Mpqf = struct @@ -26,14 +26,12 @@ module Mpqf = struct let hash x = 31 * (Z.hash (get_den x)) + Z.hash (get_num x) end -module Var = SharedFunctions.Var -module V = RelationDomain.V(Var) +module V = RelationDomain.V (** It defines the type t of the affine equality domain (a struct that contains an optional matrix and an apron environment) and provides the functions needed for handling variables (which are defined by RelationDomain.D2) such as add_vars remove_vars. Furthermore, it provides the function get_coeff_vec that parses an apron expression into a vector of coefficients if the apron expression has an affine form. *) module VarManagement (Vec: AbstractVector) (Mx: AbstractMatrix)= struct - include SharedFunctions.EnvOps module Vector = Vec (Mpqf) module Matrix = Mx(Mpqf) (Vec) @@ -78,16 +76,18 @@ struct let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del + let vars x = Environment.ivars_only x.env + let add_vars t vars = let t = copy t in - let env' = add_vars t.env vars in + let env' = Environment.add_vars t.env vars in change_d t env' true false let add_vars t vars = timing_wrap "add_vars" (add_vars t) vars let drop_vars t vars del = let t = copy t in - let env' = remove_vars t.env vars in + let env' = Environment.remove_vars t.env vars in change_d t env' false del let drop_vars t vars = timing_wrap "drop_vars" (drop_vars t) vars @@ -102,7 +102,7 @@ struct t.env <- t'.env let remove_filter t f = - let env' = remove_filter t.env f in + let env' = Environment.remove_filter t.env f in change_d t env' false false let remove_filter t f = timing_wrap "remove_filter" (remove_filter t) f @@ -114,19 +114,18 @@ struct let keep_filter t f = let t = copy t in - let env' = keep_filter t.env f in + let env' = Environment.keep_filter t.env f in change_d t env' false false let keep_filter t f = timing_wrap "keep_filter" (keep_filter t) f let keep_vars t vs = let t = copy t in - let env' = keep_vars t.env vs in + let env' = Environment.keep_vars t.env vs in change_d t env' false false let keep_vars t vs = timing_wrap "keep_vars" (keep_vars t) vs - let vars t = vars t.env let mem_var t var = Environment.mem_var t.env var @@ -462,6 +461,7 @@ struct let assign_exp (t: VarManagement(Vc)(Mx).t) var exp (no_ov: bool Lazy.t) = let t = if not @@ Environment.mem_var t.env var then add_vars t [var] else t in + (* TODO: Do we need to do a constant folding here? It happens for texpr1_of_cil_exp *) match Convert.texpr1_expr_of_cil_exp t t.env exp (Lazy.force no_ov) with | exp -> assign_texpr t var exp | exception Convert.Unsupported_CilExp _ -> diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml index 7dffafe967..03b9558621 100644 --- a/src/cdomains/apron/apronDomain.apron.ml +++ b/src/cdomains/apron/apronDomain.apron.ml @@ -4,7 +4,7 @@ open Batteries open GoblintCil open Pretty (* A binding to a selection of Apron-Domains *) -open Apron +open GobApron open RelationDomain open SharedFunctions @@ -29,8 +29,7 @@ let widening_thresholds_apron = ResettableLazy.from_fun (fun () -> let reset_lazy () = ResettableLazy.reset widening_thresholds_apron -module Var = SharedFunctions.Var -module V = RelationDomain.V(Var) +module V = RelationDomain.V module type Manager = @@ -209,7 +208,6 @@ module type AOpsExtra = sig type t val copy : t -> t - val vars_as_array : t -> Var.t array val vars : t -> Var.t list type marshal val unmarshal : marshal -> t @@ -248,15 +246,6 @@ struct let copy = A.copy Man.mgr - let vars_as_array d = - let ivs, fvs = Environment.vars (A.env d) in - assert (Array.length fvs = 0); (* shouldn't ever contain floats *) - ivs - - let vars d = - let ivs = vars_as_array d in - List.of_enum (Array.enum ivs) - (* marshal type: Abstract0.t and an array of var names *) type marshal = Man.mt Abstract0.t * string array @@ -266,31 +255,24 @@ struct let env = Environment.make vars [||] in {abstract0; env} + let vars x = Environment.ivars_only @@ A.env x + let marshal (x: t): marshal = - let vars = Array.map Var.to_string (vars_as_array x) in + let vars = Array.map Var.to_string (Array.of_list (vars x)) in x.abstract0, vars let mem_var d v = Environment.mem_var (A.env d) v - let add_vars_with nd vs = - let env' = EnvOps.add_vars (A.env nd) vs in + let envop f nd a = + let env' = f (A.env nd) a in A.change_environment_with Man.mgr nd env' false - let remove_vars_with nd vs = - let env' = EnvOps.remove_vars (A.env nd) vs in - A.change_environment_with Man.mgr nd env' false + let add_vars_with = envop Environment.add_vars + let remove_vars_with = envop Environment.remove_vars + let remove_filter_with = envop Environment.remove_filter + let keep_vars_with = envop Environment.keep_vars + let keep_filter_with = envop Environment.keep_filter - let remove_filter_with nd f = - let env' = EnvOps.remove_filter (A.env nd) f in - A.change_environment_with Man.mgr nd env' false - - let keep_vars_with nd vs = - let env' = EnvOps.keep_vars (A.env nd) vs in - A.change_environment_with Man.mgr nd env' false - - let keep_filter_with nd f = - let env' = EnvOps.keep_filter (A.env nd) f in - A.change_environment_with Man.mgr nd env' false let forget_vars_with nd vs = (* Unlike keep_vars_with, this doesn't check mem_var, but assumes valid vars, like assigns *) @@ -497,9 +479,9 @@ struct let to_yojson (x: t) = let constraints = A.to_lincons_array Man.mgr x - |> SharedFunctions.Lincons1Set.of_earray - |> SharedFunctions.Lincons1Set.elements - |> List.map (fun lincons1 -> `String (SharedFunctions.Lincons1.show lincons1)) + |> Lincons1Set.of_earray + |> Lincons1Set.elements + |> List.map (fun lincons1 -> `String (Lincons1.show lincons1)) in let env = `String (Format.asprintf "%a" (Environment.print: Format.formatter -> Environment.t -> unit) (A.env x)) in @@ -886,7 +868,6 @@ struct let unmarshal (b, d) = (BoxD.unmarshal b, D.unmarshal d) let mem_var (_, d) v = D.mem_var d v - let vars_as_array (_, d) = D.vars_as_array d let vars (_, d) = D.vars d let pretty_diff () ((_, d1), (_, d2)) = D.pretty_diff () (d1, d2) diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml new file mode 100644 index 0000000000..c39a3e42db --- /dev/null +++ b/src/cdomains/apron/gobApron.apron.ml @@ -0,0 +1,98 @@ +open Batteries +include Apron + +module Var = +struct + include Var + let equal x y = Var.compare x y = 0 +end + +module Lincons1 = +struct + include Lincons1 + + let show = Format.asprintf "%a" print + let compare x y = String.compare (show x) (show y) (* HACK *) + + let num_vars x = + (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *) + let size = ref 0 in + Lincons1.iter (fun coeff var -> + if not (Apron.Coeff.is_zero coeff) then + incr size + ) x; + !size +end + +module Lincons1Set = +struct + include Set.Make (Lincons1) + + let of_earray ({lincons0_array; array_env}: Lincons1.earray): t = + Array.enum lincons0_array + |> Enum.map (fun (lincons0: Lincons0.t) -> + Lincons1.{lincons0; env = array_env} + ) + |> of_enum +end + +(** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain. + A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *) +module Environment = +struct + include Environment + + let ivars_only env = + let ivs, fvs = Environment.vars env in + assert (Array.length fvs = 0); (* shouldn't ever contain floats *) + List.of_enum (Array.enum ivs) + + let add_vars env vs = + let vs' = + vs + |> List.enum + |> Enum.filter (fun v -> not (Environment.mem_var env v)) + |> Array.of_enum + in + Environment.add env vs' [||] + + let remove_vars env vs = + let vs' = + vs + |> List.enum + |> Enum.filter (fun v -> Environment.mem_var env v) + |> Array.of_enum + in + Environment.remove env vs' + + let remove_filter env f = + let vs' = + ivars_only env + |> List.enum + |> Enum.filter f + |> Array.of_enum + in + Environment.remove env vs' + + let keep_vars env vs = + (* Instead of iterating over all vars in env and doing a linear lookup in vs just to remove them, + make a new env with just the desired vs. *) + let vs' = + vs + |> List.enum + |> Enum.filter (fun v -> Environment.mem_var env v) + |> Array.of_enum + in + Environment.make vs' [||] + + let keep_filter env f = + (* Instead of removing undesired vars, + make a new env with just the desired vars. *) + let vs' = + ivars_only env + |> List.enum + |> Enum.filter f + |> Array.of_enum + in + Environment.make vs' [||] +end diff --git a/src/cdomains/apron/gobApron.no-apron.ml b/src/cdomains/apron/gobApron.no-apron.ml new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/cdomains/apron/relationDomain.apron.ml b/src/cdomains/apron/relationDomain.apron.ml index c5b6a0a89b..48720b0382 100644 --- a/src/cdomains/apron/relationDomain.apron.ml +++ b/src/cdomains/apron/relationDomain.apron.ml @@ -2,42 +2,16 @@ See {!ApronDomain} and {!AffineEqualityDomain}. *) +open GobApron open Batteries open GoblintCil -(** Abstracts the extended apron Var. *) -module type Var = -sig - type t - val compare : t -> t -> int - val of_string : string -> t - val to_string : t -> string - val hash : t -> int - val equal : t -> t -> bool -end - module type VarMetadata = sig type t val var_name: t -> string end -module VarMetadataTbl (VM: VarMetadata) (Var: Var) = -struct - module VH = Hashtbl.Make (Var) - - let vh = VH.create 113 - - let make_var ?name metadata = - let name = Option.default_delayed (fun () -> VM.var_name metadata) name in - let var = Var.of_string name in - VH.replace vh var metadata; - var - - let find_metadata (var: Var.t) = - VH.find_option vh var -end - module VM = struct type t = @@ -55,10 +29,26 @@ struct | Global g -> g.vname end +module VarMetadataTbl (VM: VarMetadata) = +struct + module VH = Hashtbl.Make (Var) + + let vh = VH.create 113 + + let make_var ?name metadata = + let name = Option.default_delayed (fun () -> VM.var_name metadata) name in + let var = Var.of_string name in + VH.replace vh var metadata; + var + + let find_metadata (var: Var.t) = + VH.find_option vh var +end + module type RV = sig - type t - type vartable + type t = Var.t + type vartable = VM.t VarMetadataTbl (VM).VH.t val vh: vartable val make_var: ?name:string -> VM.t -> t @@ -70,12 +60,13 @@ sig val to_cil_varinfo: t -> varinfo Option.t end -module V (Var: Var): (RV with type t = Var.t and type vartable = VM.t VarMetadataTbl (VM) (Var).VH.t) = +module V: RV = struct + open VM + type t = Var.t - module VMT = VarMetadataTbl (VM) (Var) + module VMT = VarMetadataTbl (VM) include VMT - open VM type vartable = VM.t VMT.VH.t @@ -90,12 +81,6 @@ struct | _ -> None end -module type LinCons = -sig - type t - val num_vars: t -> int -end - module type Tracked = sig val type_tracked: typ -> bool @@ -105,7 +90,7 @@ end module type S2 = sig type t - type var + type var = Var.t type marshal module Tracked: Tracked @@ -144,8 +129,8 @@ module type S3 = sig include S2 - val cil_exp_of_lincons1: Apron.Lincons1.t -> exp option - val invariant: t -> Apron.Lincons1.t list + val cil_exp_of_lincons1: Lincons1.t -> exp option + val invariant: t -> Lincons1.t list end type ('a, 'b) relcomponents_t = { @@ -184,10 +169,9 @@ struct let name () = RD.name () ^ " * " ^ PrivD.name () - let of_tuple(rel, priv):t = {rel; priv} - let to_tuple r = (r.rel, r.priv) - let arbitrary () = + let to_tuple r = (r.rel, r.priv) in + let of_tuple (rel, priv) = {rel; priv} in let tr = QCheck.pair (RD.arbitrary ()) (PrivD.arbitrary ()) in QCheck.map ~rev:to_tuple of_tuple tr @@ -216,7 +200,6 @@ end module type RD = sig - module Var : Var - module V : module type of struct include V(Var) end - include S3 with type var = Var.t + module V : RV + include S3 end diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml index 059a7f8264..e66be00ae4 100644 --- a/src/cdomains/apron/sharedFunctions.apron.ml +++ b/src/cdomains/apron/sharedFunctions.apron.ml @@ -8,42 +8,6 @@ module M = Messages module BI = IntOps.BigIntOps -module Var = -struct - include Var - - let equal x y = Var.compare x y = 0 -end - -module Lincons1 = -struct - include Lincons1 - - let show = Format.asprintf "%a" print - let compare x y = String.compare (show x) (show y) (* HACK *) - - let num_vars x = - (* Apron.Linexpr0.get_size returns some internal nonsense, so we count ourselves. *) - let size = ref 0 in - Lincons1.iter (fun coeff var -> - if not (Apron.Coeff.is_zero coeff) then - incr size - ) x; - !size -end - -module Lincons1Set = -struct - include Set.Make (Lincons1) - - let of_earray ({lincons0_array; array_env}: Lincons1.earray): t = - Array.enum lincons0_array - |> Enum.map (fun (lincons0: Lincons0.t) -> - Lincons1.{lincons0; env = array_env} - ) - |> of_enum -end - let int_of_scalar ?round (scalar: Scalar.t) = if Scalar.is_infty scalar <> 0 then (* infinity means unbounded *) None @@ -291,66 +255,6 @@ struct include CilOfApron (V) end -(** A few code elements for environment changes from functions as remove_vars etc. have been moved to sharedFunctions as they are needed in a similar way inside affineEqualityDomain. - A module that includes various methods used by variable handling operations such as add_vars, remove_vars etc. in apronDomain and affineEqualityDomain. *) -module EnvOps = -struct - let vars env = - let ivs, fvs = Environment.vars env in - assert (Array.length fvs = 0); (* shouldn't ever contain floats *) - List.of_enum (Array.enum ivs) - - let add_vars env vs = - let vs' = - vs - |> List.enum - |> Enum.filter (fun v -> not (Environment.mem_var env v)) - |> Array.of_enum - in - Environment.add env vs' [||] - - let remove_vars env vs = - let vs' = - vs - |> List.enum - |> Enum.filter (fun v -> Environment.mem_var env v) - |> Array.of_enum - in - Environment.remove env vs' - - let remove_filter env f = - let vs' = - vars env - |> List.enum - |> Enum.filter f - |> Array.of_enum - in - Environment.remove env vs' - - let keep_vars env vs = - (* Instead of iterating over all vars in env and doing a linear lookup in vs just to remove them, - make a new env with just the desired vs. *) - let vs' = - vs - |> List.enum - |> Enum.filter (fun v -> Environment.mem_var env v) - |> Array.of_enum - in - Environment.make vs' [||] - - let keep_filter env f = - (* Instead of removing undesired vars, - make a new env with just the desired vars. *) - let vs' = - vars env - |> List.enum - |> Enum.filter f - |> Array.of_enum - in - Environment.make vs' [||] - -end - (** A more specific module type for RelationDomain.RelD2 with ConvBounds integrated and various apron elements. It is designed to be the interface for the D2 modules in affineEqualityDomain and apronDomain and serves as a functor argument for AssertionModule. *) module type AssertionRelS = diff --git a/src/cdomains/concDomain.ml b/src/cdomains/concDomain.ml index b16cdf1d9f..5f609a31d8 100644 --- a/src/cdomains/concDomain.ml +++ b/src/cdomains/concDomain.ml @@ -1,6 +1,25 @@ (** Domains for thread sets and their uniqueness. *) -module ThreadSet = SetDomain.ToppedSet (ThreadIdDomain.Thread) (struct let topname = "All Threads" end) +module ThreadSet = +struct + include SetDomain.Make (ThreadIdDomain.Thread) + + let is_top = mem UnknownThread + + let top () = singleton UnknownThread + + let merge uop cop x y = + match is_top x, is_top y with + | true, true -> uop x y + | false, true -> x + | true, false -> y + | false, false -> cop x y + + let meet x y = merge join meet x y + + let narrow x y = merge (fun x y -> widen x (join x y)) narrow x y + +end module MustThreadSet = SetDomain.Reverse(ThreadSet) module CreatedThreadSet = ThreadSet diff --git a/src/cdomains/fileDomain.ml b/src/cdomains/fileDomain.ml deleted file mode 100644 index ca585b8bce..0000000000 --- a/src/cdomains/fileDomain.ml +++ /dev/null @@ -1,81 +0,0 @@ -(** Domains for file handles. *) - -open Batteries - -module D = MvalMapDomain - - -module Val = -struct - type mode = Read | Write [@@deriving eq, ord, hash] - type s = Open of string*mode | Closed | Error [@@deriving eq, ord, hash] - let name = "File handles" - let var_state = Closed - let string_of_mode = function Read -> "Read" | Write -> "Write" - let string_of_state = function - | Open(filename, m) -> "open("^filename^", "^string_of_mode m^")" - | Closed -> "closed" - | Error -> "error" - - (* properties of records (e.g. used by Dom.warn_each) *) - let opened s = s <> Closed && s <> Error - let closed s = s = Closed - let writable s = match s with Open((_,Write)) -> true | _ -> false -end - - -module Dom = -struct - include D.Domain (D.Value (Val)) - - (* returns a tuple (thunk, result) *) - let report_ ?(neg=false) k p msg m = - let f ?(may=false) msg = - let f () = warn ~may msg in - f, if may then `May true else `Must true in - let mf = (fun () -> ()), `Must false in - if mem k m then - let p = if neg then not % p else p in - let v = find' k m in - if V.must p v then f msg (* must *) - else if V.may p v then f ~may:true msg (* may *) - else mf (* none *) - else if neg then f msg else mf - - let report ?(neg=false) k p msg m = (fst (report_ ~neg k p msg m)) () (* evaluate thunk *) - - let reports k xs m = - let uncurry (neg, p, msg) = report_ ~neg:neg k p msg m in - let f result x = if snd (uncurry x) = result then Some (fst (uncurry x)) else None in - let must_true = BatList.filter_map (f (`Must true)) xs in - let may_true = BatList.filter_map (f (`May true)) xs in - (* output first must and first may *) - if must_true <> [] then (List.hd must_true) (); - if may_true <> [] then (List.hd may_true) () - - (* handling state *) - let opened r = V.state r |> Val.opened - let closed r = V.state r |> Val.closed - let writable r = V.state r |> Val.writable - - let fopen k loc filename mode m = - if is_unknown k m then m else - let mode = match String.lowercase_ascii mode with "r" -> Val.Read | _ -> Val.Write in - let v = V.make k loc (Val.Open(filename, mode)) in - add' k v m - let fclose k loc m = - if is_unknown k m then m else - let v = V.make k loc Val.Closed in - change k v m - let error k m = - if is_unknown k m then m else - let loc = if mem k m then find' k m |> V.split |> snd |> Set.choose |> V.loc else [] in - let v = V.make k loc Val.Error in - change k v m - let success k m = - if is_unknown k m then m else - match find_option k m with - | Some v when V.may (Val.opened%V.state) v && V.may (V.in_state Val.Error) v -> - change k (V.filter (Val.opened%V.state) v) m (* TODO what about must-set? *) - | _ -> m -end diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml index 054030017f..5d5174744f 100644 --- a/src/cdomains/intDomain.ml +++ b/src/cdomains/intDomain.ml @@ -996,12 +996,12 @@ struct let arbitrary ik = let open QCheck.Iter in - (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint MyCheck.Arbitrary.big_int in *) + (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint GobQCheck.Arbitrary.big_int in *) (* TODO: apparently bigints are really slow compared to int64 for domaintest *) - let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in + let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in let pair_arb = QCheck.pair int_arb int_arb in let shrink = function - | Some (l, u) -> (return None) <+> (MyCheck.shrink pair_arb (l, u) >|= of_interval ik >|= fst) + | Some (l, u) -> (return None) <+> (GobQCheck.shrink pair_arb (l, u) >|= of_interval ik >|= fst) | None -> empty in QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) (fun x -> of_interval ik x |> fst ) pair_arb) @@ -1601,13 +1601,13 @@ struct let arbitrary ik = let open QCheck.Iter in - (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint MyCheck.Arbitrary.big_int in *) + (* let int_arb = QCheck.map ~rev:Ints_t.to_bigint Ints_t.of_bigint GobQCheck.Arbitrary.big_int in *) (* TODO: apparently bigints are really slow compared to int64 for domaintest *) - let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in + let int_arb = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in let pair_arb = QCheck.pair int_arb int_arb in let list_pair_arb = QCheck.small_list pair_arb in let canonize_randomly_generated_list = (fun x -> norm_intvs ik x |> fst) in - let shrink xs = MyCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list + let shrink xs = GobQCheck.shrink list_pair_arb xs >|= canonize_randomly_generated_list in QCheck.(set_shrink shrink @@ set_print show @@ map (*~rev:BatOption.get*) canonize_randomly_generated_list list_pair_arb) end @@ -1695,7 +1695,7 @@ struct let logand n1 n2 = of_bool ((to_bool' n1) && (to_bool' n2)) let logor n1 n2 = of_bool ((to_bool' n1) || (to_bool' n2)) let cast_to ?torg t x = failwith @@ "Cast_to not implemented for " ^ (name ()) ^ "." - let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 (* TODO: use ikind *) + let arbitrary ik = QCheck.map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 (* TODO: use ikind *) let invariant _ _ = Invariant.none (* TODO *) end @@ -2402,8 +2402,8 @@ struct let excluded s = from_excl ik s in let definite x = of_int ik x in let shrink = function - | `Excluded (s, _) -> MyCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *) - | `Definite x -> (return `Bot) <+> (MyCheck.shrink (BigInt.arbitrary ()) x >|= definite) + | `Excluded (s, _) -> GobQCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *) + | `Definite x -> (return `Bot) <+> (GobQCheck.shrink (BigInt.arbitrary ()) x >|= definite) | `Bot -> empty in QCheck.frequency ~shrink ~print:show [ @@ -2816,8 +2816,8 @@ module Enums : S with type int_t = BigInt.t = struct let neg s = of_excl_list ik (BISet.elements s) in let pos s = norm ik (Inc s) in let shrink = function - | Exc (s, _) -> MyCheck.shrink (BISet.arbitrary ()) s >|= neg (* S TODO: possibly shrink neg to pos *) - | Inc s -> MyCheck.shrink (BISet.arbitrary ()) s >|= pos + | Exc (s, _) -> GobQCheck.shrink (BISet.arbitrary ()) s >|= neg (* S TODO: possibly shrink neg to pos *) + | Inc s -> GobQCheck.shrink (BISet.arbitrary ()) s >|= pos in QCheck.frequency ~shrink ~print:show [ 20, QCheck.map neg (BISet.arbitrary ()); @@ -3307,7 +3307,7 @@ struct let arbitrary ik = let open QCheck in - let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 MyCheck.Arbitrary.int64 in + let int_arb = map ~rev:Ints_t.to_int64 Ints_t.of_int64 GobQCheck.Arbitrary.int64 in let cong_arb = pair int_arb int_arb in let of_pair ik p = normalize ik (Some p) in let to_pair = Option.get in diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml index 8037cfa21d..016a72a77e 100644 --- a/src/cdomains/mHP.ml +++ b/src/cdomains/mHP.ml @@ -4,7 +4,7 @@ include Printable.Std let name () = "mhp" -module TID = ThreadIdDomain.FlagConfiguredTID +module TID = ThreadIdDomain.Thread module Pretty = GoblintCil.Pretty type t = { diff --git a/src/cdomains/mvalMapDomain.ml b/src/cdomains/mvalMapDomain.ml deleted file mode 100644 index d0d2f8da85..0000000000 --- a/src/cdomains/mvalMapDomain.ml +++ /dev/null @@ -1,299 +0,0 @@ -(** Domains for {{!Mval} mvalue} maps. *) - -open Batteries -open GoblintCil - -module M = Messages - - -exception Unknown -exception Error - -(* signature for map entries *) -module type S = -sig - include Lattice.S - type k = Mval.Exp.t (* key *) - type s (* state is defined by Impl *) - type r (* record *) - - (* printing *) - val string_of: t -> string - val string_of_key: k -> string - val string_of_record: r -> string - - (* constructing *) - val make: k -> Node.t list -> s -> t - - (* manipulation *) - val map: (r -> r) -> t -> t - val filter: (r -> bool) -> t -> t - val union: t -> t -> t - val set_key: k -> t -> t - val set_state: s -> t -> t - val remove_state: s -> t -> t - - (* deconstructing *) - val split: t -> r Set.t * r Set.t - val map': (r -> 'a) -> t -> 'a Set.t * 'a Set.t - val filter': (r -> bool) -> t -> r Set.t * r Set.t - val length: t -> int * int - - (* predicates *) - val must: (r -> bool) -> t -> bool - val may: (r -> bool) -> t -> bool - (* properties of records *) - val key: r -> k - val loc: r -> Node.t list - val edit_loc: (Node.t list -> Node.t list) -> r -> r - val state: r -> s - val in_state: s -> r -> bool - - (* special variables *) - val get_record: t -> r option - (* val make_record: k -> location list -> s -> r *) - val make_var: k -> t - val from_tuple: r Set.t * r Set.t -> t - - (* aliasing *) - val is_alias: t -> bool - val get_alias: t -> k - val make_alias: k -> t -end - -module Value (Impl: sig - type s (* state *) [@@deriving eq, ord, hash] - val name: string - val var_state: s - val string_of_state: s -> string - end) : S with type s = Impl.s = -struct - type k = Mval.Exp.t [@@deriving eq, ord, hash] - type s = Impl.s [@@deriving eq, ord, hash] - module R = struct - include Printable.StdLeaf - type t = { key: k; loc: Node.t list; state: s } [@@deriving eq, ord, hash] - let name () = "MValMapDomainValue" - - let pretty () {key; loc; state} = - Pretty.dprintf "{key=%a; loc=%a; state=%s}" Mval.Exp.pretty key (Pretty.d_list ", " Node.pretty) loc (Impl.string_of_state state) - - include Printable.SimplePretty ( - struct - type nonrec t = t - let pretty = pretty - end - ) - end - type r = R.t - open R - (* TODO: use SetDomain.Reverse? *) - module Must' = SetDomain.ToppedSet (R) (struct let topname = "top" end) - module Must = Lattice.Reverse (Must') - module May = SetDomain.ToppedSet (R) (struct let topname = "top" end) - include Lattice.Prod (Must) (May) - let name () = Impl.name - - (* converts to polymorphic sets *) - let split (x,y) = try Must'.elements x |> Set.of_list, May.elements y |> Set.of_list with SetDomain.Unsupported _ -> Set.empty, Set.empty - - (* special variable used for indirection *) - let alias_var = Cilfacade.create_var @@ Cil.makeVarinfo false "@alias" Cil.voidType, `NoOffset - (* alias structure: x[0].key=alias_var, y[0].key=linked_var *) - let is_alias (x,y) = neg Must'.is_empty x && (Must'.choose x).key=alias_var - let get_alias (x,y) = (May.choose y).key - - (* Printing *) - let string_of_key k = Mval.Exp.show k - let string_of_loc xs = String.concat ", " (List.map (CilType.Location.show % Node.location) xs) - let string_of_record r = Impl.string_of_state r.state^" ("^string_of_loc r.loc^")" - let string_of (x,y) = - if is_alias (x,y) then - "alias for "^string_of_key @@ get_alias (x,y) - else - let x, y = split (x,y) in - let z = Set.diff y x in - "{ "^String.concat ", " (List.map string_of_record (Set.elements x))^" }, "^ - "{ "^String.concat ", " (List.map string_of_record (Set.elements z))^" }" - let show x = string_of x - include Printable.SimpleShow (struct - type nonrec t = t - let show = show - end) - (* constructing & manipulation *) - let make_record k l s = { key=k; loc=l; state=s } - let make k l s = let v = make_record k l s in Must'.singleton v, May.singleton v - let map f (x,y) = Must'.map f x, May.map f y - let filter p (x,y) = Must'.filter p x, May.filter p y (* retains top *) - let union (a,b) (c,d) = Must'.union a c, May.union b d - let set_key k v = map (fun x -> {x with key=k}) v (* changes key for all elements *) - let set_state s v = map (fun x -> {x with state=s}) v - let remove_state s v = filter (fun x -> x.state<>s) v - - (* deconstructing *) - let length = split %> Tuple2.mapn Set.cardinal - let map' f = split %> Tuple2.mapn (Set.map f) - let filter' f = split %> Tuple2.mapn (Set.filter f) - - (* predicates *) - let must p (x,y) = Must'.exists p x || May.for_all p y - let may p (x,y) = May.exists p y - - (* properties of records *) - let key r = r.key - let loc r = r.loc - let edit_loc f r = {r with loc=f r.loc} - let state r = r.state - let in_state s r = r.state = s - - (* special variables *) - let get_record (x,y) = if Must'.is_empty x then None else Some (Must'.choose x) - let make_var_record k = make_record k [] Impl.var_state - let make_var k = Must'.singleton (make_var_record k), May.singleton (make_var_record k) - let make_alias k = Must'.singleton (make_var_record alias_var), May.singleton (make_var_record k) - let from_tuple (x,y) = Set.to_list x |> Must'.of_list, Set.to_list y |> May.of_list -end - - -module Domain (V: S) = -struct - module K = Mval.Exp - module V = V - module MD = MapDomain.MapBot (Mval.Exp) (V) - include MD - - (* Map functions *) - (* find that resolves aliases *) - let find' k m = let v = find k m in if V.is_alias v then find (V.get_alias v) m else v - let find_option k m = if mem k m then Some(find' k m) else None - let get_alias k m = (* target: returns Some k' if k links to k' *) - if mem k m && V.is_alias (find k m) then Some (V.get_alias (find k m)) else None - let get_aliased k m = (* sources: get list of keys that link to k *) - (* iter (fun k' (x,y) -> if V.is_alias (x,y) then print_endline ("alias "^V.string_of_key k'^" -> "^V.string_of_key (Set.choose y).key)) m; *) - (* TODO V.get_alias v=k somehow leads to Out_of_memory... *) - filter (fun k' v -> V.is_alias v && V.string_of_key (V.get_alias v)=V.string_of_key k) m |> bindings |> List.map fst - let get_aliases k m = (* get list of all other keys that have the same pointee *) - match get_alias k m with - | Some k' -> [k] (* k links to k' *) - | None -> get_aliased k m (* k' that link to k *) - let alias a b m = (* link a to b *) - (* if b is already an alias, follow it... *) - let b' = get_alias b m |? b in - (* add an entry for key a, that points to b' *) - add a (V.make_alias b') m - let remove' k m = (* fixes keys that link to k before removing it *) - if mem k m && not (V.is_alias (find k m)) then (* k might be aliased *) - let v = find k m in - match get_aliased k m with - | [] -> remove k m (* nothing links to k *) - | k'::xs -> let m = add k' v m in (* set k' to v, link xs to k', finally remove k *) - (* List.map (fun x -> x.vname) (k'::xs) |> String.concat ", " |> print_endline; *) - List.fold_left (fun m x -> alias x k' m) m xs |> remove k - else remove k m (* k not in m or an alias *) - let add' k v m = - remove' k m (* fixes keys that might have linked to k *) - |> add k v (* set new value *) - let change k v m = (* if k is an alias, replace its pointee *) - add (get_alias k m |? k) v m - - (* special variables *) - let get_record k m = Option.bind (find_option k m) V.get_record - let edit_record k f m = - let v = find_option k m |? V.make_var k in - add k (V.map f v) m - let get_value k m = find_option k m |> Option.map_default V.split (Set.empty,Set.empty) - let extend_value k v' m = - let v = V.from_tuple v' in - if mem k m then - add k (V.union (find k m) v) m - else - add k v m - let union (a,b) (c,d) = Set.union a c, Set.union b d - let is_special_var k = String.get (V.string_of_key k) 0 = '@' - let without_special_vars m = filter (fun k v -> not @@ is_special_var k) m - - (* functions needed for enter & combine *) - (* only keep globals, aliases to them and special variables *) - let only_globals m = filter (fun k v -> (fst k).vglob || V.is_alias v && (fst (V.get_alias v)).vglob || is_special_var k) m - (* adds all the bindings from m2 to m1 (overwrites!) *) - let add_all m1 m2 = add_list (bindings m2) m1 - - (* callstack for locations *) - let callstack_var = Cilfacade.create_var @@ Cil.makeVarinfo false "@callstack" Cil.voidType, `NoOffset - let callstack m = get_record callstack_var m |> Option.map_default V.loc [] - let string_of_callstack m = " [call stack: "^String.concat ", " (List.map (CilType.Location.show % Node.location) (callstack m))^"]" - let edit_callstack f m = edit_record callstack_var (V.edit_loc f) m - - - (* predicates *) - let must k p m = mem k m && V.must p (find' k m) - let may k p m = mem k m && V.may p (find' k m) - let is_may k m = mem k m && let x,y = V.length (find' k m) in x=0 && y>0 - - let filter_values p m = (* filters all values in the map and flattens result *) - let flatten_sets = List.fold_left Set.union Set.empty in - without_special_vars m - |> filter (fun k v -> V.may p v && not (V.is_alias v)) - |> bindings |> List.map (fun (k,v) -> V.filter' p v) - |> List.split |> (fun (x,y) -> flatten_sets x, flatten_sets y) - let filter_records k p m = (* filters both sets of k *) - if mem k m then V.filter' p (find' k m) else Set.empty, Set.empty - - let unknown k m = add' k (V.top ()) m - let is_unknown k m = if mem k m then V.is_top (find' k m) else false - - (* printing *) - let string_of_state k m = if not (mem k m) then "?" else V.string_of (find' k m) - let string_of_key k = V.string_of_key k - let string_of_keys rs = Set.map (V.string_of_key % V.key) rs |> Set.elements |> String.concat ", " - let string_of_entry k m = string_of_key k ^ ": " ^ string_of_state k m - let string_of_map m = List.map (fun (k,v) -> string_of_entry k m) (bindings m) - - let warn ?may:(may=false) ?loc:(loc=[Option.get !Node.current_node]) msg = - let split_category s = - if Str.string_partial_match (Str.regexp {|\[\([^]]*\)\]|}) s 0 then - (Some (Str.matched_group 1 s), Str.string_after s (Str.match_end ())) - else - (None, s) - in - let rec split_categories s = - match split_category s with - | (Some category, s') -> - let (categories, s'') = split_categories s' in - (category :: categories, s'') - | (None, s') -> ([], s') - in - match split_categories msg with - | ([], msg) -> (if may then Messages.warn else Messages.error) ~loc:(Node (List.last loc)) "%s" msg - | (category :: categories, msg) -> - let category_of_string s = Messages.Category.from_string_list [String.lowercase_ascii s] in (* TODO: doesn't split subcategories, not used and no defined syntax even *) - let category = category_of_string category in - let tags = List.map (fun category -> Messages.Tag.Category (category_of_string category)) categories in - (if may then Messages.warn else Messages.error) ~loc:(Node (List.last loc)) ~category ~tags "%s" msg - - (* getting keys from Cil Lvals *) - - let key_from_lval lval = match lval with (* TODO try to get a Mval.Exp from Cil.Lval *) - | Var v1, o1 -> v1, Offset.Exp.of_cil o1 - | Mem Lval(Var v1, o1), o2 -> v1, Offset.Exp.of_cil (addOffset o1 o2) - (* | Mem exp, o1 -> failwith "not implemented yet" (* TODO use query_lv *) *) - | _ -> Cilfacade.create_var @@ Cil.makeVarinfo false ("?"^CilType.Lval.show lval) Cil.voidType, `NoOffset (* TODO *) - - let keys_from_lval lval (ask: Queries.ask) = (* use MayPointTo query to get all possible pointees of &lval *) - (* print_query_lv ctx.ask (AddrOf lval); *) - let query_addrs (ask: Queries.ask) exp = match ask.f (Queries.MayPointTo exp) with - | ad when not (Queries.AD.is_top ad) -> Queries.AD.elements ad - | _ -> [] - in - let exp = AddrOf lval in - let addrs = query_addrs ask exp in (* MayPointTo -> LValSet *) - let keys = List.fold (fun vs addr -> - match addr with - | Queries.AD.Addr.Addr (v,o) -> (v, ValueDomain.Offs.to_exp o) :: vs - | _ -> vs - ) [] addrs - in - let pretty_key k = Pretty.text (string_of_key k) in - Messages.debug ~category:Analyzer "MayPointTo %a = [%a]" d_exp exp (Pretty.docList ~sep:(Pretty.text ", ") pretty_key) keys; - keys -end diff --git a/src/cdomains/offset.ml b/src/cdomains/offset.ml index eca85e08a4..52cfe9eb41 100644 --- a/src/cdomains/offset.ml +++ b/src/cdomains/offset.ml @@ -22,7 +22,7 @@ struct include CilType.Exp let name () = "exp index" - let any = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "any_index") + let any = Cilfacade.any_index_exp let all = CastE (TInt (Cilfacade.ptrdiff_ikind (), []), mkString "all_index") (* Override output *) diff --git a/src/cdomains/specDomain.ml b/src/cdomains/specDomain.ml deleted file mode 100644 index 75a9d8edc5..0000000000 --- a/src/cdomains/specDomain.ml +++ /dev/null @@ -1,34 +0,0 @@ -(** Domains for finite automaton specification file analysis. *) - -open Batteries - -module D = MvalMapDomain - - -module Val = -struct - type s = string [@@deriving eq, ord, hash] - let name = "Spec value" - let var_state = "" - let string_of_state s = s - - (* transforms May-Sets of length 1 to Must. NOTE: this should only be done if the original set had more than one element! *) - (* let maybe_must = function May xs when Set.cardinal xs = 1 -> Must (Set.choose xs) | x -> x *) - (* let may = function Must x -> May (Set.singleton x) | xs -> xs *) - (* let records = function Must x -> (Set.singleton x) | May xs -> xs *) - (* let list_of_records = function Must x -> [x] | May xs -> List.of_enum (Set.enum xs) *) - (* let vnames x = String.concat ", " (List.map (fun r -> string_of_key r.var) (list_of_records x)) *) -end - - -module Dom = -struct - include D.Domain (D.Value (Val)) - - (* handling state *) - let goto k loc state m = add' k (V.make k loc state) m - let may_goto k loc state m = let v = V.join (find' k m) (V.make k loc state) in add' k v m - let in_state k s m = must k (V.in_state s) m - let may_in_state k s m = may k (V.in_state s) m - let get_states k m = if not (mem k m) then [] else find' k m |> V.map' V.state |> snd |> Set.elements -end diff --git a/src/cdomains/threadIdDomain.ml b/src/cdomains/threadIdDomain.ml index a9646cffd2..d0c3f7b61b 100644 --- a/src/cdomains/threadIdDomain.ml +++ b/src/cdomains/threadIdDomain.ml @@ -280,6 +280,79 @@ struct let name () = "FlagConfiguredTID: " ^ if history_enabled () then H.name () else P.name () end -module Thread = FlagConfiguredTID +type thread = + | Thread of FlagConfiguredTID.t + | UnknownThread +[@@deriving eq, ord, hash] + +module Thread : Stateful with type t = thread = +struct + include Printable.Std + type t = thread [@@deriving eq, ord, hash] + + let name () = "Thread id" + let pretty () t = + match t with + | Thread tid -> FlagConfiguredTID.pretty () tid + | UnknownThread -> Pretty.text "Unknown thread id" + + let show t = + match t with + | Thread tid -> FlagConfiguredTID.show tid + | UnknownThread -> "Unknown thread id" + + let printXml f t = + match t with + | Thread tid -> FlagConfiguredTID.printXml f tid + | UnknownThread -> BatPrintf.fprintf f "\n\nUnknown thread id\n\n\n" + + let to_yojson t = + match t with + | Thread tid -> FlagConfiguredTID.to_yojson tid + | UnknownThread -> `String "Unknown thread id" + + let relift t = + match t with + | Thread tid -> Thread (FlagConfiguredTID.relift tid) + | UnknownThread -> UnknownThread + + let lift t = Thread t + + let threadinit v ~multiple = Thread (FlagConfiguredTID.threadinit v ~multiple) + + let is_main t = + match t with + | Thread tid -> FlagConfiguredTID.is_main tid + | UnknownThread -> false + + let is_unique t = + match t with + | Thread tid -> FlagConfiguredTID.is_unique tid + | UnknownThread -> false + + let may_create t1 t2 = + match t1, t2 with + | Thread tid1, Thread tid2 -> FlagConfiguredTID.may_create tid1 tid2 + | _, _ -> true + + let is_must_parent t1 t2 = + match t1, t2 with + | Thread tid1, Thread tid2 -> FlagConfiguredTID.is_must_parent tid1 tid2 + | _, _ -> false + + module D = FlagConfiguredTID.D + + let threadenter ~multiple (t, d) node i v = + match t with + | Thread tid -> List.map lift (FlagConfiguredTID.threadenter ~multiple (tid, d) node i v) + | UnknownThread -> assert false + + let threadspawn = FlagConfiguredTID.threadspawn + + let created t d = + match t with + | Thread tid -> Option.map (List.map lift) (FlagConfiguredTID.created tid d) + | UnknownThread -> None +end module ThreadLifted = Lift (Thread) diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 774bced523..d1b81dcb08 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -522,7 +522,7 @@ struct let warn_type op x y = if GobConfig.get_bool "dbg.verbose" then - ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Tracing.current_loc pretty x pretty y + ignore @@ printf "warn_type %s: incomparable abstr. values %s and %s at %a: %a and %a\n" op (tag_name (x:t)) (tag_name (y:t)) CilType.Location.pretty !Goblint_tracing.current_loc pretty x pretty y let rec leq x y = match (x,y) with @@ -572,11 +572,9 @@ struct | y, Blob (x,s,o) -> Blob (join (x:t) y, s, o) | (Thread x, Thread y) -> Thread (Threads.join x y) | (Int x, Thread y) - | (Thread y, Int x) -> - Thread y (* TODO: ignores int! *) + | (Thread y, Int x) -> Thread (Threads.join y (Threads.top ())) | (Address x, Thread y) - | (Thread y, Address x) -> - Thread y (* TODO: ignores address! *) + | (Thread y, Address x) -> Thread (Threads.join y (Threads.top ())) | (JmpBuf x, JmpBuf y) -> JmpBuf (JmpBufs.join x y) | (Mutex, Mutex) -> Mutex | (MutexAttr x, MutexAttr y) -> MutexAttr (MutexAttr.join x y) @@ -605,11 +603,9 @@ struct | (Blob x, Blob y) -> Blob (Blobs.widen x y) (* TODO: why no blob special cases like in join? *) | (Thread x, Thread y) -> Thread (Threads.widen x y) | (Int x, Thread y) - | (Thread y, Int x) -> - Thread y (* TODO: ignores int! *) + | (Thread y, Int x) -> Thread (Threads.widen y (Threads.join y (Threads.top ()))) | (Address x, Thread y) - | (Thread y, Address x) -> - Thread y (* TODO: ignores address! *) + | (Thread y, Address x) -> Thread (Threads.widen y (Threads.join y (Threads.top ()))) | (Mutex, Mutex) -> Mutex | (JmpBuf x, JmpBuf y) -> JmpBuf (JmpBufs.widen x y) | (MutexAttr x, MutexAttr y) -> MutexAttr (MutexAttr.widen x y) @@ -728,7 +724,7 @@ struct let v = invalidate_value ask voidType (CArrays.get ask n (array_idx_top)) in Array (CArrays.set ask n (array_idx_top) v) | t , Blob n -> Blob (Blobs.invalidate_value ask t n) - | _ , Thread _ -> state (* TODO: no top thread ID set! *) + | _ , Thread tid -> Thread (Threads.join (Threads.top ()) tid) | _ , JmpBuf _ -> state (* TODO: no top jmpbuf *) | _, Bot -> Bot (* Leave uninitialized value (from malloc) alone in free to avoid trashing everything. TODO: sound? *) | t , _ -> top_value t diff --git a/src/common/cdomains/basetype.ml b/src/common/cdomains/basetype.ml index 55b5dbde07..1b846309aa 100644 --- a/src/common/cdomains/basetype.ml +++ b/src/common/cdomains/basetype.ml @@ -20,8 +20,6 @@ struct | _ -> Local let name () = "variables" let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape (show x)) - - let arbitrary () = MyCheck.Arbitrary.varinfo end module RawStrings: Printable.S with type t = string = @@ -35,12 +33,6 @@ struct let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (XmlUtil.escape (show x)) end -module Strings: Lattice.S with type t = [`Bot | `Lifted of string | `Top] = - Lattice.Flat (RawStrings) (struct - let top_name = "?" - let bot_name = "-" - end) - module RawBools: Printable.S with type t = bool = struct include Printable.StdLeaf @@ -52,12 +44,6 @@ struct let printXml f x = BatPrintf.fprintf f "\n\n%s\n\n\n" (show x) end -module Bools: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] = - Lattice.Flat (RawBools) (struct - let top_name = "?" - let bot_name = "-" - end) - module CilExp = struct include CilType.Exp diff --git a/src/common/common.mld b/src/common/common.mld index 662c789572..2ad88c3758 100644 --- a/src/common/common.mld +++ b/src/common/common.mld @@ -10,6 +10,7 @@ For better context, see {!Goblint_lib} which also documents these modules. Node Edge MyCFG +CfgTools } {2 Specification} @@ -18,19 +19,10 @@ AnalysisState ControlSpecC } -{2 Configuration} -{!modules: -GobConfig -AfterConfig -JsonSchema -Options -} - {1 Domains} {!modules: Printable -Lattice } {2 Analysis-specific} @@ -42,7 +34,6 @@ Lattice {1 I/O} {!modules: Messages -Tracing } @@ -69,6 +60,3 @@ RichVarinfo {2 Standard library} {!modules:GobFormat} - -{2 Other libraries} -{!modules:MyCheck} diff --git a/src/common/domains/printable.ml b/src/common/domains/printable.ml index b0755fb730..cc01718ee8 100644 --- a/src/common/domains/printable.ml +++ b/src/common/domains/printable.ml @@ -233,9 +233,9 @@ struct let arbitrary () = let open QCheck.Iter in let shrink = function - | `Lifted x -> (return `Bot) <+> (MyCheck.shrink (Base.arbitrary ()) x >|= lift) + | `Lifted x -> (return `Bot) <+> (GobQCheck.shrink (Base.arbitrary ()) x >|= lift) | `Bot -> empty - | `Top -> MyCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift + | `Top -> GobQCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift in QCheck.frequency ~shrink ~print:show [ 20, QCheck.map lift (Base.arbitrary ()); @@ -273,6 +273,40 @@ struct | `Right x -> `Right (Base2.relift x) end +module Either3 (Base1: S) (Base2: S) (Base3: S) = +struct + type t = [`Left of Base1.t | `Middle of Base2.t | `Right of Base3.t] [@@deriving eq, ord, hash] + include Std + + let pretty () (state:t) = + match state with + | `Left n -> Pretty.dprintf "%s:%a" (Base1.name ()) Base1.pretty n + | `Middle n -> Pretty.dprintf "%s:%a" (Base2.name ()) Base2.pretty n + | `Right n -> Pretty.dprintf "%s:%a" (Base3.name ()) Base3.pretty n + + let show state = + match state with + | `Left n -> (Base1.name ()) ^ ":" ^ Base1.show n + | `Middle n -> (Base2.name ()) ^ ":" ^ Base2.show n + | `Right n -> (Base3.name ()) ^ ":" ^ Base3.show n + + let name () = "either " ^ Base1.name () ^ " or " ^ Base2.name () ^ " or " ^ Base3.name () + let printXml f = function + | `Left x -> BatPrintf.fprintf f "\n\nLeft\n\n%a\n\n" Base1.printXml x + | `Middle x -> BatPrintf.fprintf f "\n\nMiddle\n\n%a\n\n" Base2.printXml x + | `Right x -> BatPrintf.fprintf f "\n\nRight\n\n%a\n\n" Base3.printXml x + + let to_yojson = function + | `Left x -> `Assoc [ Base1.name (), Base1.to_yojson x ] + | `Middle x -> `Assoc [ Base2.name (), Base2.to_yojson x ] + | `Right x -> `Assoc [ Base3.name (), Base3.to_yojson x ] + + let relift = function + | `Left x -> `Left (Base1.relift x) + | `Middle x -> `Middle (Base2.relift x) + | `Right x -> `Right (Base3.relift x) +end + module Option (Base: S) (N: Name) = struct type t = Base.t option [@@deriving eq, ord, hash] @@ -592,8 +626,8 @@ struct let arbitrary () = let open QCheck.Iter in let shrink = function - | `Lifted x -> MyCheck.shrink (Base.arbitrary ()) x >|= lift - | `Top -> MyCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift + | `Lifted x -> GobQCheck.shrink (Base.arbitrary ()) x >|= lift + | `Top -> GobQCheck.Iter.of_arbitrary ~n:20 (Base.arbitrary ()) >|= lift in QCheck.frequency ~shrink ~print:show [ 20, QCheck.map lift (Base.arbitrary ()); diff --git a/src/common/dune b/src/common/dune index c8f1564782..7994798579 100644 --- a/src/common/dune +++ b/src/common/dune @@ -8,22 +8,18 @@ batteries.unthreaded zarith goblint_std + goblint_config + goblint_tracing goblint-cil fpath yojson - json-data-encoding - cpu goblint_timing - goblint_build_info - goblint.sites qcheck-core.runner) (flags :standard -open Goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash - ppx_deriving_yojson - ppx_blob)) - (preprocessor_deps (file util/options.schema.json))) + ppx_deriving_yojson))) (documentation) diff --git a/src/framework/cfgTools.ml b/src/common/framework/cfgTools.ml similarity index 98% rename from src/framework/cfgTools.ml rename to src/common/framework/cfgTools.ml index 8f98a48e84..78aba17060 100644 --- a/src/framework/cfgTools.ml +++ b/src/common/framework/cfgTools.ml @@ -122,10 +122,6 @@ let rec pretty_edges () = function | [_,x] -> Edge.pretty_plain () x | (_,x)::xs -> Pretty.dprintf "%a; %a" Edge.pretty_plain x pretty_edges xs -let get_pseudo_return_id fd = - let start_id = 10_000_000_000 in (* TODO get max_sid? *) - let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *) - if sid < start_id then sid + start_id else sid let node_scc_global = NH.create 113 @@ -260,7 +256,7 @@ let createCFG (file: file) = if Messages.tracing then Messages.trace "cfg" "adding pseudo-return to the function %s.\n" fd.svar.vname; let fd_end_loc = {fd_loc with line = fd_loc.endLine; byte = fd_loc.endByte; column = fd_loc.endColumn} in let newst = mkStmt (Return (None, fd_end_loc)) in - newst.sid <- get_pseudo_return_id fd; + newst.sid <- Cilfacade.get_pseudo_return_id fd; Cilfacade.StmtH.add Cilfacade.pseudo_return_to_fun newst fd; Cilfacade.IntH.replace Cilfacade.pseudo_return_stmt_sids newst.sid newst; let newst_node = Statement newst in @@ -475,7 +471,7 @@ let createCFG (file: file) = ); if Messages.tracing then Messages.trace "cfg" "CFG building finished.\n\n"; if get_bool "dbg.verbose" then - ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgF) GobHashtbl.pretty_statistics (GobHashtbl.magic_stats cfgB)); + ignore (Pretty.eprintf "cfgF (%a), cfgB (%a)\n" GobHashtbl.pretty_statistics (NH.stats cfgF) GobHashtbl.pretty_statistics (NH.stats cfgB)); cfgF, cfgB, skippedByEdge let createCFG = Timing.wrap "createCFG" createCFG @@ -685,7 +681,7 @@ let getGlobalInits (file: file) : edges = lval in let rec any_index_offset = function - | Index (e,o) -> Index (Offset.Index.Exp.any, any_index_offset o) + | Index (e,o) -> Index (Cilfacade.any_index_exp, any_index_offset o) | Field (f,o) -> Field (f, any_index_offset o) | NoOffset -> NoOffset in diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml index 26a2f082a4..eff97da404 100644 --- a/src/common/util/cilfacade.ml +++ b/src/common/util/cilfacade.ml @@ -531,6 +531,12 @@ let stmt_fundecs: fundec StmtH.t ResettableLazy.t = h ) + +let get_pseudo_return_id fd = + let start_id = 10_000_000_000 in (* TODO get max_sid? *) + let sid = Hashtbl.hash fd.svar.vid in (* Need pure sid instead of Cil.new_sid for incremental, similar to vid in Cilfacade.create_var. We only add one return stmt per loop, so the hash from the functions vid should be unique. *) + if sid < start_id then sid + start_id else sid + let pseudo_return_to_fun = StmtH.create 113 (** Find [fundec] which the [stmt] is in. *) @@ -706,4 +712,10 @@ let add_function_declarations (file: Cil.file): unit = in let fun_decls = List.filter_map declaration_from_GFun functions in let globals = upto_last_type @ fun_decls @ non_types @ functions in - file.globals <- globals \ No newline at end of file + file.globals <- globals + + +(** Special index expression for some unknown index. + Weakly updates array in assignment. + Used for [exp.fast_global_inits]. *) +let any_index_exp = CastE (TInt (ptrdiff_ikind (), []), mkString "any_index") (* TODO: move back to Offset *) diff --git a/src/common/util/messages.ml b/src/common/util/messages.ml index 42a3118978..d7afec43c5 100644 --- a/src/common/util/messages.ml +++ b/src/common/util/messages.ml @@ -339,4 +339,23 @@ let msg_final severity ?(tags=[]) ?(category=Category.Unknown) fmt = else GobPretty.igprintf () fmt -include Tracing + +include Goblint_tracing + +open Pretty + +let tracel sys ?var fmt = + let loc = !current_loc in + let docloc sys doc = + printtrace sys (dprintf "(%a)@?" CilType.Location.pretty loc ++ indent 2 doc); + in + gtrace true docloc sys var ~loc ignore fmt + +let traceli sys ?var ?(subsys=[]) fmt = + let loc = !current_loc in + let g () = activate sys subsys in + let docloc sys doc: unit = + printtrace sys (dprintf "(%a)" CilType.Location.pretty loc ++ indent 2 doc); + traceIndent () + in + gtrace true docloc sys var ~loc g fmt diff --git a/src/common/util/afterConfig.ml b/src/config/afterConfig.ml similarity index 100% rename from src/common/util/afterConfig.ml rename to src/config/afterConfig.ml diff --git a/src/config/config.mld b/src/config/config.mld new file mode 100644 index 0000000000..160eaa9a11 --- /dev/null +++ b/src/config/config.mld @@ -0,0 +1,14 @@ +{0 Library goblint.config} +This library is unwrapped and provides the following top-level modules. +For better context, see {!Goblint_lib} which also documents these modules. + + +{1 Framework} + +{2 Configuration} +{!modules: +GobConfig +AfterConfig +JsonSchema +Options +} diff --git a/src/config/dune b/src/config/dune new file mode 100644 index 0000000000..1508e2553e --- /dev/null +++ b/src/config/dune @@ -0,0 +1,23 @@ +(include_subdirs no) + +(library + (name goblint_config) + (public_name goblint.config) + (wrapped false) ; TODO: wrap + (libraries + batteries.unthreaded + goblint_std + goblint_tracing + fpath + yojson + json-data-encoding + cpu + goblint.sites + qcheck-core.runner) + (flags :standard -open Goblint_std) + (preprocess + (pps + ppx_blob)) + (preprocessor_deps (file options.schema.json))) + +(documentation) diff --git a/src/common/util/gobConfig.ml b/src/config/gobConfig.ml similarity index 96% rename from src/common/util/gobConfig.ml rename to src/config/gobConfig.ml index c517ba150d..24a1701ce6 100644 --- a/src/common/util/gobConfig.ml +++ b/src/config/gobConfig.ml @@ -21,7 +21,6 @@ *) open Batteries -open Tracing open Printf exception ConfigError of string @@ -300,7 +299,7 @@ struct try let st = String.trim st in let x = get_value !json_conf (parse_path st) in - if tracing then trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x; + if Goblint_tracing.tracing then Goblint_tracing.trace "conf-reads" "Reading '%s', it is %a.\n" st GobYojson.pretty x; try f x with Yojson.Safe.Util.Type_error (s, _) -> eprintf "The value for '%s' has the wrong type: %s\n" st s; @@ -332,7 +331,7 @@ struct let wrap_get f x = (* self-observe options, which Spec construction depends on *) - if !building_spec && Tracing.tracing then Tracing.trace "config" "get during building_spec: %s\n" x; + if !building_spec && Goblint_tracing.tracing then Goblint_tracing.trace "config" "get during building_spec: %s\n" x; (* TODO: blacklist such building_spec option from server mode modification since it will have no effect (spec is already built) *) f x @@ -352,7 +351,7 @@ struct (** Helper function for writing values. Handles the tracing. *) let set_path_string st v = - if tracing then trace "conf" "Setting '%s' to %a.\n" st GobYojson.pretty v; + if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Setting '%s' to %a.\n" st GobYojson.pretty v; set_value v json_conf (parse_path st) let set_json st j = @@ -402,7 +401,7 @@ struct | Some fn -> let v = Yojson.Safe.from_channel % BatIO.to_input_channel |> File.with_file_in (Fpath.to_string fn) in merge v; - if tracing then trace "conf" "Merging with '%a', resulting\n%a.\n" GobFpath.pretty fn GobYojson.pretty !json_conf + if Goblint_tracing.tracing then Goblint_tracing.trace "conf" "Merging with '%a', resulting\n%a.\n" GobFpath.pretty fn GobYojson.pretty !json_conf | None -> raise (Sys_error (Printf.sprintf "%s: No such file or diretory" (Fpath.to_string fn))) end diff --git a/src/common/util/jsonSchema.ml b/src/config/jsonSchema.ml similarity index 100% rename from src/common/util/jsonSchema.ml rename to src/config/jsonSchema.ml diff --git a/src/common/util/options.ml b/src/config/options.ml similarity index 98% rename from src/common/util/options.ml rename to src/config/options.ml index 3046f70809..125da3330b 100644 --- a/src/common/util/options.ml +++ b/src/config/options.ml @@ -1,4 +1,4 @@ -(** [src/common/util/options.schema.json] low-level access. *) +(** [src/config/options.schema.json] low-level access. *) open Json_schema diff --git a/src/common/util/options.schema.json b/src/config/options.schema.json similarity index 99% rename from src/common/util/options.schema.json rename to src/config/options.schema.json index 7937bb1699..30bc4f3d8c 100644 --- a/src/common/util/options.schema.json +++ b/src/config/options.schema.json @@ -467,32 +467,6 @@ }, "additionalProperties": false }, - "file": { - "title": "ana.file", - "type": "object", - "properties": { - "optimistic": { - "title": "ana.file.optimistic", - "description": "Assume fopen never fails.", - "type": "boolean", - "default": false - } - }, - "additionalProperties": false - }, - "spec": { - "title": "ana.spec", - "type": "object", - "properties": { - "file": { - "title": "ana.spec.file", - "description": "Path to the specification file.", - "type": "string", - "default": "" - } - }, - "additionalProperties": false - }, "pml": { "title": "ana.pml", "type": "object", diff --git a/src/domains/boolDomain.ml b/src/domain/boolDomain.ml similarity index 72% rename from src/domains/boolDomain.ml rename to src/domain/boolDomain.ml index e088c3605c..08be66a602 100644 --- a/src/domains/boolDomain.ml +++ b/src/domain/boolDomain.ml @@ -4,10 +4,10 @@ module Bool = struct include Basetype.RawBools (* type t = bool - let equal = Bool.equal - let compare = Bool.compare - let relift x = x - let arbitrary () = QCheck.bool *) + let equal = Bool.equal + let compare = Bool.compare + let relift x = x + let arbitrary () = QCheck.bool *) let pretty_diff () (x,y) = GoblintCil.Pretty.dprintf "%s: %a not leq %a" (name ()) pretty x pretty y end @@ -38,4 +38,10 @@ struct let widen = (&&) let meet = (||) let narrow = (||) -end \ No newline at end of file +end + +module FlatBool: Lattice.S with type t = [`Bot | `Lifted of bool | `Top] = + Lattice.Flat (Bool) (struct + let top_name = "?" + let bot_name = "-" + end) diff --git a/src/domains/disjointDomain.ml b/src/domain/disjointDomain.ml similarity index 100% rename from src/domains/disjointDomain.ml rename to src/domain/disjointDomain.ml diff --git a/src/domain/domain.mld b/src/domain/domain.mld new file mode 100644 index 0000000000..ce7e1a5859 --- /dev/null +++ b/src/domain/domain.mld @@ -0,0 +1,21 @@ +{0 Library goblint.domain} +This library is unwrapped and provides the following top-level modules. +For better context, see {!Goblint_lib} which also documents these modules. + + +{1 Domains} +{!modules: +Lattice +} + +{2 General} +{!modules: +BoolDomain +SetDomain +MapDomain +TrieDomain +DisjointDomain +HoareDomain +PartitionDomain +FlagHelper +} diff --git a/src/domain/dune b/src/domain/dune new file mode 100644 index 0000000000..169f4a1d5c --- /dev/null +++ b/src/domain/dune @@ -0,0 +1,19 @@ +(include_subdirs no) + +(library + (name goblint_domain) + (public_name goblint.domain) + (wrapped false) ; TODO: wrap + (libraries + batteries.unthreaded + goblint_std + goblint_common + goblint-cil) + (flags :standard -open Goblint_std) + (preprocess + (pps + ppx_deriving.std + ppx_deriving_hash + ppx_deriving_yojson))) + +(documentation) diff --git a/src/domains/flagHelper.ml b/src/domain/flagHelper.ml similarity index 100% rename from src/domains/flagHelper.ml rename to src/domain/flagHelper.ml diff --git a/src/domains/hoareDomain.ml b/src/domain/hoareDomain.ml similarity index 97% rename from src/domains/hoareDomain.ml rename to src/domain/hoareDomain.ml index 23b1a92240..37b8231b92 100644 --- a/src/domains/hoareDomain.ml +++ b/src/domain/hoareDomain.ml @@ -134,13 +134,15 @@ struct let equal x y = leq x y && leq y x let hash xs = fold (fun v a -> a + E.hash v) xs 0 let compare x y = - if equal x y - then 0 + if equal x y then + 0 + else ( + let caridnality_comp = compare (cardinal x) (cardinal y) in + if caridnality_comp <> 0 then + caridnality_comp else - let caridnality_comp = compare (cardinal x) (cardinal y) in - if caridnality_comp <> 0 - then caridnality_comp - else Map.compare (List.compare E.compare) x y + Map.compare (List.compare E.compare) x y + ) let show x : string = let all_elems : string list = List.map E.show (elements x) in Printable.get_short_list "{" "}" all_elems @@ -234,8 +236,8 @@ struct ) s2 nil with Not_found -> dprintf "choose failed b/c of empty set s1: %d s2: %d" - (cardinal s1) - (cardinal s2) + (cardinal s1) + (cardinal s2) end end @@ -339,8 +341,8 @@ struct ) s2 nil with Not_found -> dprintf "choose failed b/c of empty set s1: %d s2: %d" - (cardinal s1) - (cardinal s2) + (cardinal s1) + (cardinal s2) end end [@@deprecated] diff --git a/src/common/domains/lattice.ml b/src/domain/lattice.ml similarity index 96% rename from src/common/domains/lattice.ml rename to src/domain/lattice.ml index 51306d637f..9ea3f74635 100644 --- a/src/common/domains/lattice.ml +++ b/src/domain/lattice.ml @@ -148,18 +148,14 @@ struct end (* HAS SIDE-EFFECTS ---- PLEASE INSTANCIATE ONLY ONCE!!! *) -module HConsed (Base:S) = +module HConsed (Base:S) (Arg: sig val assume_idempotent: bool end) = struct include Printable.HConsed (Base) - (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *) - (* see https://github.com/goblint/analyzer/issues/1005 *) - let int_refine_active = GobConfig.get_string "ana.int.refinement" <> "never" - let lift_f2 f x y = f (unlift x) (unlift y) - let narrow x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y) + let narrow x y = if Arg.assume_idempotent && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.narrow x y) let widen x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.widen x y) - let meet x y = if (not int_refine_active) && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y) + let meet x y = if Arg.assume_idempotent && x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.meet x y) let join x y = if x.BatHashcons.tag == y.BatHashcons.tag then x else lift (lift_f2 Base.join x y) let leq x y = (x.BatHashcons.tag == y.BatHashcons.tag) || lift_f2 Base.leq x y let is_top = lift_f Base.is_top diff --git a/src/domains/mapDomain.ml b/src/domain/mapDomain.ml similarity index 99% rename from src/domains/mapDomain.ml rename to src/domain/mapDomain.ml index 76dec6f0d2..740da9969e 100644 --- a/src/domains/mapDomain.ml +++ b/src/domain/mapDomain.ml @@ -259,11 +259,12 @@ struct end (* TODO: this is very slow because every add/remove in a fold-loop relifts *) +(* TODO: currently hardcoded to assume_idempotent *) module HConsed (M: S) : S with type key = M.key and type value = M.value = struct - include Lattice.HConsed (M) + include Lattice.HConsed (M) (struct let assume_idempotent = false end) type key = M.key type value = M.value @@ -717,8 +718,8 @@ struct let singleton k v = `Lifted (M.singleton k v) let empty () = `Lifted (M.empty ()) let is_empty = function - | `Bot -> false - | `Lifted x -> M.is_empty x + | `Bot -> false + | `Lifted x -> M.is_empty x let exists f = function | `Bot -> raise (Fn_over_All "exists") | `Lifted x -> M.exists f x diff --git a/src/domains/partitionDomain.ml b/src/domain/partitionDomain.ml similarity index 100% rename from src/domains/partitionDomain.ml rename to src/domain/partitionDomain.ml diff --git a/src/domains/setDomain.ml b/src/domain/setDomain.ml similarity index 100% rename from src/domains/setDomain.ml rename to src/domain/setDomain.ml diff --git a/src/domains/trieDomain.ml b/src/domain/trieDomain.ml similarity index 100% rename from src/domains/trieDomain.ml rename to src/domain/trieDomain.ml diff --git a/src/domains/queries.ml b/src/domains/queries.ml index b9fa28f5be..228320bef3 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -32,7 +32,11 @@ module FlatYojson = Lattice.Flat (Printable.Yojson) (struct let bot_name = "bot yojson" end) -module SD = Basetype.Strings +module SD: Lattice.S with type t = [`Bot | `Lifted of string | `Top] = + Lattice.Flat (Basetype.RawStrings) (struct + let top_name = "?" + let bot_name = "-" + end) module VD = ValueDomain.Compound module AD = ValueDomain.AD diff --git a/src/dune b/src/dune index acd5348acb..eac6640451 100644 --- a/src/dune +++ b/src/dune @@ -6,11 +6,15 @@ (library (name goblint_lib) (public_name goblint.lib) - (modules :standard \ goblint mainspec privPrecCompare apronPrecCompare messagesCompare) - (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_common + (modules :standard \ goblint privPrecCompare apronPrecCompare messagesCompare) + (libraries goblint.sites goblint.build-info goblint-cil.all-features batteries.unthreaded qcheck-core.runner sha json-data-encoding jsonrpc cpu arg-complete fpath yaml yaml.unix uuidm goblint_timing catapult goblint_backtrace fileutils goblint_std goblint_config goblint_common goblint_domain goblint_library goblint_incremental goblint_tracing ; Conditionally compile based on whether apron optional dependency is installed or not. ; Alternative dependencies seem like the only way to optionally depend on optional dependencies. ; See: https://dune.readthedocs.io/en/stable/concepts.html#alternative-dependencies. + (select gobApron.ml from + (apron -> gobApron.apron.ml) + (-> gobApron.no-apron.ml) + ) (select apronDomain.ml from (apron apron.octD apron.boxD apron.polkaMPQ zarith_mlgmpidl -> apronDomain.apron.ml) (-> apronDomain.no-apron.ml) @@ -73,10 +77,10 @@ (copy_files# witness/z3/*.ml) (executables - (names goblint mainspec) - (public_names goblint -) + (names goblint) + (public_names goblint) (modes byte native) ; https://dune.readthedocs.io/en/stable/dune-files.html#linking-modes - (modules goblint mainspec) + (modules goblint) (libraries goblint.lib goblint.sites.dune goblint.build-info.dune goblint_std) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall -open Goblint_std) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index b1bbc73660..77d3a38186 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -12,12 +12,17 @@ module M = Messages (** Lifts a [Spec] so that the domain is [Hashcons]d *) module HashconsLifter (S:Spec) - : Spec with module D = Lattice.HConsed (S.D) - and module G = S.G + : Spec with module G = S.G and module C = S.C = struct - module D = Lattice.HConsed (S.D) + module HConsedArg = + struct + (* We do refine int values on narrow and meet {!IntDomain.IntDomTupleImpl}, which can lead to fixpoint issues if we assume x op x = x *) + (* see https://github.com/goblint/analyzer/issues/1005 *) + let assume_idempotent = GobConfig.get_string "ana.int.refinement" = "never" + end + module D = Lattice.HConsed (S.D) (HConsedArg) module G = S.G module C = S.C module V = S.V @@ -820,13 +825,13 @@ struct ) let tf var getl sidel getg sideg prev_node (_,edge) d (f,t) = - let old_loc = !Tracing.current_loc in - let old_loc2 = !Tracing.next_loc in - Tracing.current_loc := f; - Tracing.next_loc := t; + let old_loc = !Goblint_tracing.current_loc in + let old_loc2 = !Goblint_tracing.next_loc in + Goblint_tracing.current_loc := f; + Goblint_tracing.next_loc := t; Goblint_backtrace.protect ~mark:(fun () -> TfLocation f) ~finally:(fun () -> - Tracing.current_loc := old_loc; - Tracing.next_loc := old_loc2 + Goblint_tracing.current_loc := old_loc; + Goblint_tracing.next_loc := old_loc2 ) (fun () -> let d = tf var getl sidel getg sideg prev_node edge d in d @@ -999,7 +1004,7 @@ struct let dummy_pseudo_return_node f = (* not the same as in CFG, but compares equal because of sid *) - Node.Statement ({Cil.dummyStmt with sid = CfgTools.get_pseudo_return_id f}) + Node.Statement ({Cil.dummyStmt with sid = Cilfacade.get_pseudo_return_id f}) in let add_nodes_of_fun (functions: fundec list) (withEntry: fundec -> bool) = let add_stmts (f: fundec) = @@ -1344,7 +1349,7 @@ struct module EM = struct - include MapDomain.MapBot (Basetype.CilExp) (Basetype.Bools) + include MapDomain.MapBot (Basetype.CilExp) (BoolDomain.FlatBool) let name () = "branches" end @@ -1467,14 +1472,14 @@ struct module V = struct - include Printable.Either (S.V) (Printable.Either (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C))) + include Printable.Either3 (S.V) (Printable.Prod (Node) (C)) (Printable.Prod (CilType.Fundec) (C)) let name () = "longjmp" let s x = `Left x - let longjmpto x = `Right (`Left x) - let longjmpret x = `Right (`Right x) + let longjmpto x = `Middle x + let longjmpret x = `Right x let is_write_only = function | `Left x -> S.V.is_write_only x - | `Right _ -> false + | _ -> false end module G = @@ -1511,7 +1516,7 @@ struct begin match g with | `Left g -> S.query (conv ctx) (WarnGlobal (Obj.repr g)) - | `Right g -> + | _ -> Queries.Result.top q end | InvariantGlobal g -> @@ -1519,7 +1524,7 @@ struct begin match g with | `Left g -> S.query (conv ctx) (InvariantGlobal (Obj.repr g)) - | `Right g -> + | _ -> Queries.Result.top q end | IterSysVars (vq, vf) -> diff --git a/src/framework/control.ml b/src/framework/control.ml index 0c9b61739b..00a6034e27 100644 --- a/src/framework/control.ml +++ b/src/framework/control.ml @@ -142,12 +142,12 @@ struct if List.mem "termination" @@ get_string_list "ana.activated" then ( (* check if we have upjumping gotos *) let open Cilfacade in - let warn_for_upjumps fundec gotos = + let warn_for_upjumps fundec gotos = if FunSet.mem live_funs fundec then ( (* set nortermiantion flag *) AnalysisState.svcomp_may_not_terminate := true; (* iterate through locations to produce warnings *) - LocSet.iter (fun l _ -> + LocSet.iter (fun l _ -> M.warn ~loc:(M.Location.CilLocation l) ~category:Termination "The program might not terminate! (Upjumping Goto)" ) gotos ) @@ -313,7 +313,7 @@ struct if M.tracing then M.trace "con" "Initializer %a\n" CilType.Location.pretty loc; (*incr count; if (get_bool "dbg.verbose")&& (!count mod 1000 = 0) then Printf.printf "%d %!" !count; *) - Tracing.current_loc := loc; + Goblint_tracing.current_loc := loc; match edge with | MyCFG.Entry func -> if M.tracing then M.trace "global_inits" "Entry %a\n" d_lval (var func.svar); @@ -335,9 +335,9 @@ struct in let with_externs = do_extern_inits ctx file in (*if (get_bool "dbg.verbose") then Printf.printf "Number of init. edges : %d\nWorking:" (List.length edges); *) - let old_loc = !Tracing.current_loc in + let old_loc = !Goblint_tracing.current_loc in let result : Spec.D.t = List.fold_left transfer_func with_externs edges in - Tracing.current_loc := old_loc; + Goblint_tracing.current_loc := old_loc; if M.tracing then M.trace "global_inits" "startstate: %a\n" Spec.D.pretty result; result, !funs in diff --git a/src/goblint_lib.ml b/src/goblint_lib.ml index 70f331b5ac..5a2e0d3e0e 100644 --- a/src/goblint_lib.ml +++ b/src/goblint_lib.ml @@ -51,7 +51,7 @@ module VarQuery = VarQuery (** {2 Configuration} Runtime configuration is represented as JSON. - Options are specified and documented by the JSON schema [src/common/util/options.schema.json]. *) + Options are specified and documented by the JSON schema [src/config/options.schema.json]. *) module GobConfig = GobConfig module AfterConfig = AfterConfig @@ -130,7 +130,7 @@ module ExtractPthread = ExtractPthread Analyses related to [longjmp] and [setjmp]. *) module ActiveSetjmp = ActiveSetjmp -module ModifiedSinceLongjmp = ModifiedSinceLongjmp +module ModifiedSinceSetjmp = ModifiedSinceSetjmp module ActiveLongjmp = ActiveLongjmp module PoisonVariables = PoisonVariables module Vla = Vla @@ -147,12 +147,10 @@ module UnitAnalysis = UnitAnalysis (** {2 Other} *) module Assert = Assert -module FileUse = FileUse module LoopTermination = LoopTermination module Uninit = Uninit module Expsplit = Expsplit module StackTrace = StackTrace -module Spec = Spec (** {2 Helper} @@ -263,12 +261,8 @@ module AccessDomain = AccessDomain module MusteqDomain = MusteqDomain module RegionDomain = RegionDomain -module FileDomain = FileDomain module StackDomain = StackDomain -module MvalMapDomain = MvalMapDomain -module SpecDomain = SpecDomain - (** {2 Testing} Modules related to (property-based) testing of domains. *) @@ -331,7 +325,6 @@ module SolverBox = SolverBox Various input/output interfaces and formats. *) module Messages = Messages -module Tracing = Tracing (** {2 Front-end} @@ -447,6 +440,7 @@ module WideningThresholds = WideningThresholds module VectorMatrix = VectorMatrix module SharedFunctions = SharedFunctions +module GobApron = GobApron (** {2 Precision comparison} *) @@ -467,9 +461,3 @@ module ApronPrecCompareUtil = ApronPrecCompareUtil OCaml standard library extensions which are not provided by {!Batteries}. *) module GobFormat = GobFormat - -(** {2 Other libraries} - - External library extensions. *) - -module MyCheck = MyCheck diff --git a/src/util/cilMaps.ml b/src/incremental/cilMaps.ml similarity index 100% rename from src/util/cilMaps.ml rename to src/incremental/cilMaps.ml diff --git a/src/incremental/compareCFG.ml b/src/incremental/compareCFG.ml index 225cbb1c76..55b3fa8fc5 100644 --- a/src/incremental/compareCFG.ml +++ b/src/incremental/compareCFG.ml @@ -17,7 +17,7 @@ let (&&<>) (prev_result: bool * rename_mapping) f : bool * rename_mapping = let eq_node (x, fun1) (y, fun2) ~rename_mapping = let isPseudoReturn f sid = - let pid = CfgTools.get_pseudo_return_id f in + let pid = Cilfacade.get_pseudo_return_id f in sid == pid in match x,y with | Statement s1, Statement s2 -> diff --git a/src/incremental/dune b/src/incremental/dune new file mode 100644 index 0000000000..595dba22f7 --- /dev/null +++ b/src/incremental/dune @@ -0,0 +1,22 @@ +(include_subdirs no) + +(library + (name goblint_incremental) + (public_name goblint.incremental) + (wrapped false) ; TODO: wrap + (libraries + batteries.unthreaded + zarith + goblint_std + goblint_config + goblint_common + goblint-cil + fpath) + (flags :standard -open Goblint_std) + (preprocess + (pps + ppx_deriving.std + ppx_deriving_hash + ppx_deriving_yojson))) + +(documentation) diff --git a/src/incremental/incremental.mld b/src/incremental/incremental.mld new file mode 100644 index 0000000000..bf9b6e6a58 --- /dev/null +++ b/src/incremental/incremental.mld @@ -0,0 +1,16 @@ +{0 Library goblint.incremental} +This library is unwrapped and provides the following top-level modules. +For better context, see {!Goblint_lib} which also documents these modules. + + +{1 Incremental} + +{!modules: +CompareCIL +CompareAST +CompareCFG +UpdateCil +MaxIdUtil +Serialize +CilMaps +} diff --git a/src/index.mld b/src/index.mld index 2afbbc97ae..76b9d230dd 100644 --- a/src/index.mld +++ b/src/index.mld @@ -7,9 +7,21 @@ The following libraries make up Goblint's main codebase. {!modules:Goblint_lib} This library currently contains the majority of Goblint and is in the process of being split into smaller libraries. +{2 Library goblint.config} +This {{!page-config}unwrapped library} contains various configuration modules extracted from {!Goblint_lib}. + {2 Library goblint.common} This {{!page-common}unwrapped library} contains various common modules extracted from {!Goblint_lib}. +{2 Library goblint.domain} +This {{!page-domain}unwrapped library} contains various domain modules extracted from {!Goblint_lib}. + +{2 Library goblint.library} +This {{!page-library}unwrapped library} contains various library specification modules extracted from {!Goblint_lib}. + +{2 Library goblint.incremental} +This {{!page-incremental}unwrapped library} contains various incremental modules extracted from {!Goblint_lib}. + {1 Library extensions} The following libraries provide extensions to other OCaml libraries. @@ -43,6 +55,9 @@ The following libraries provide utilities which are completely independent of Go {2 Library goblint.timing} {!modules:Goblint_timing} +{2 Library goblint.tracing} +{!modules:Goblint_tracing} + {1 Vendored} The following libraries are vendored in Goblint. diff --git a/src/main.camldoc b/src/main.camldoc index ec08a14a7b..0a0e52035f 100644 --- a/src/main.camldoc +++ b/src/main.camldoc @@ -85,7 +85,6 @@ FlagModeDomain LockDomain StackDomain FileDomain -SpecDomain LvalMapDomain } @@ -106,7 +105,6 @@ Glob {!modules: MCP Base -Spec CondVars Contain diff --git a/src/maingoblint.ml b/src/maingoblint.ml index dcee9abb13..2c7d353594 100644 --- a/src/maingoblint.ml +++ b/src/maingoblint.ml @@ -53,7 +53,7 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy ( let add_string l = let f str = l := str :: !l in Arg_complete.String (f, Arg_complete.empty) in let add_int l = let f str = l := str :: !l in Arg_complete.Int (f, Arg_complete.empty) in let set_trace sys = - if Messages.tracing then Tracing.addsystem sys + if Messages.tracing then Goblint_tracing.addsystem sys else (prerr_endline "Goblint has been compiled without tracing, recompile in trace profile (./scripts/trace_on.sh)"; raise Stdlib.Exit) in let configure_html () = @@ -112,8 +112,8 @@ let rec option_spec_list: Arg_complete.speclist Lazy.t = lazy ( ; "--print_options" , Arg_complete.Unit (fun () -> Options.print_options (); exit 0), "" ; "--print_all_options" , Arg_complete.Unit (fun () -> Options.print_all_options (); exit 0), "" ; "--trace" , Arg_complete.String (set_trace, Arg_complete.empty), "" - ; "--tracevars" , add_string Tracing.tracevars, "" - ; "--tracelocs" , add_int Tracing.tracelocs, "" + ; "--tracevars" , add_string Goblint_tracing.tracevars, "" + ; "--tracelocs" , add_int Goblint_tracing.tracelocs, "" ; "--help" , Arg_complete.Unit (fun _ -> print_help stdout),"" ; "--html" , Arg_complete.Unit (fun _ -> configure_html ()),"" ; "--sarif" , Arg_complete.Unit (fun _ -> configure_sarif ()),"" diff --git a/src/mainspec.ml b/src/mainspec.ml deleted file mode 100644 index 4509645f98..0000000000 --- a/src/mainspec.ml +++ /dev/null @@ -1,13 +0,0 @@ -open Goblint_lib -open Batteries (* otherwise open_in would return wrong type for SpecUtil *) -open SpecUtil - -let _ = - (* no arguments -> run interactively (= reading from stdin) *) - let args = Array.length Sys.argv > 1 in - if args && Sys.argv.(1) = "-" then - ignore(parse ~dot:true stdin) - else - let cin = if args then open_in Sys.argv.(1) else stdin in - ignore(parse ~repl:(not args) ~print:true cin) -(* exit 0 *) diff --git a/src/solvers/postSolver.ml b/src/solvers/postSolver.ml index f96ca832a1..e01560c752 100644 --- a/src/solvers/postSolver.ml +++ b/src/solvers/postSolver.ml @@ -154,13 +154,7 @@ struct module VH = Hashtbl.Make (S.Var) (* starts as Hashtbl for quick lookup *) - let starth = - (* VH.of_list S.starts *) (* TODO: BatHashtbl.Make.of_list is broken, use after new Batteries release *) - let starth = VH.create (List.length S.starts) in - List.iter (fun (x, d) -> - VH.replace starth x d - ) S.starts; - starth + let starth = VH.of_list S.starts let system x = match S.system x, VH.find_option starth x with diff --git a/src/spec/dune b/src/spec/dune deleted file mode 100644 index 47c22a0d46..0000000000 --- a/src/spec/dune +++ /dev/null @@ -1,2 +0,0 @@ -(ocamllex specLexer) -(ocamlyacc specParser) diff --git a/src/spec/file.dot b/src/spec/file.dot deleted file mode 100644 index a78c64d3fc..0000000000 --- a/src/spec/file.dot +++ /dev/null @@ -1,37 +0,0 @@ -digraph file { - // changed file pointer {fp} (no longer safe) - - // file handle is not saved! - // overwriting still opened file handle - // file is never closed - // file may be never closed - // closeing unopened file handle - // closeing already closed file handle - // writing to closed file handle - // writing to unopened file handle - // writing to read-only file handle - - // unclosed files: ... - // maybe unclosed files: ... - - w1 [label="file handle is not saved!"]; - w2 [label="closeing unopened file handle"]; - w3 [label="writing to unopened file handle"]; - w4 [label="writing to read-only file handle"]; - w5 [label="closeing already closed file handle"]; - w6 [label="writing to closed file handle"]; - - 1 -> w1 [label="fopen(_)"]; - 1 -> w2 [label="fclose($fp)"]; - 1 -> w3 [label="fprintf($fp, _)"]; - 1 -> open_read [label="$fp = fopen($path, \"r\")"]; - 1 -> open_write [label="$fp = fopen($path, \"w\")"]; - 1 -> open_write [label="$fp = fopen($path, \"a\")"]; - open_read -> w4 [label="fprintf($fp, _)"]; - open_write -> open_write [label="fprintf($fp, _)"]; - open_read -> closed [label="fclose($fp)"]; - open_write -> closed [label="fclose($fp)"]; - closed -> w5 [label="fclose($fp)"]; - closed -> w6 [label="fprintf($fp, _)"]; - closed -> 1 [label="->"]; -} \ No newline at end of file diff --git a/src/spec/render.sh b/src/spec/render.sh deleted file mode 100755 index 91e486c247..0000000000 --- a/src/spec/render.sh +++ /dev/null @@ -1,31 +0,0 @@ -# command -v ls >&- || {echo >&2 bla; exit 1;} -function check(){ - set -e # needed to exit script from function - hash $1 2>&- || (echo >&2 "$1 is needed but not installed! $2"; exit 1;) - set +e # do not exit shell if some command fails (default) -} -check dot -mode=${1-"png"} -file=${2-"file"} -dst=graph -viewcmd=gpicview - -mkdir -p ${dst} -cp ${file}.dot ${dst} -file=${file##*/} # use basename in case the file was somewhere else -cd ${dst} -trap 'cd ..' EXIT # leave dst again on exit -case "$mode" in - png) dot -Tpng -o${file}.png ${file}.dot; - check ${viewcmd} "Please edit viewcmd accordingly." - pkill ${viewcmd}; - ${viewcmd} ${file}.png & - ;; - pdf) rm -f ${file}.tex; - check dot2tex - dot -Txdot ${file}.dot | dot2tex > ${file}.tex; - check pdflatex - pdflatex ${file}.tex - echo "generated $dst/$file.pdf" - ;; -esac diff --git a/src/spec/specCore.ml b/src/spec/specCore.ml deleted file mode 100644 index 9d0ce35624..0000000000 --- a/src/spec/specCore.ml +++ /dev/null @@ -1,152 +0,0 @@ -(* types used by specParser and functions for handling the constructed types *) - -open Batteries - -exception Endl -exception Eof - -(* type value = String of string | Bool of bool | Int of int | Float of float *) -type lval = Ptr of lval | Var of string | Ident of string -type fcall = {fname: string; args: exp list} -and exp = - Fun of fcall | - Exp_ | - Lval of lval | - Regex of string | - String of string | Bool of bool | Int of int | Float of float | - Binop of string * exp * exp | - Unop of string * exp -type stmt = {lval: lval option; exp: exp} -type def = Node of (string * string) (* node warning *) - | Edge of (string * string list * bool * string * stmt) (* start-node, warning-nodes, forwarding, target-node, constraint *) - -(* let stmts edges = List.map (fun (a,b,c) -> c) edges - let get_fun stmt = match stmt.exp with Fun x -> Some x | _ -> None - let fun_records edges = List.filter_map get_fun (stmts edges) - let fun_names edges = fun_records edges |> List.map (fun x -> x.fname) - let fun_by_fname fname edges = List.filter (fun x -> x.fname=fname) (fun_records edges) *) -let fname_is fname stmt = - match stmt.exp with - | Fun x -> x.fname=fname - | _ -> false - -let is_wildcard stmt = stmt.exp = Exp_ - -let branch_exp stmt = - match stmt.exp with - | Fun { fname="branch"; args=[exp; Bool tv] } -> Some (exp,tv) - | _ -> None - -let is_branch stmt = branch_exp stmt <> None - -let startnode edges = - (* The start node of the first transition is the start node of the automaton. *) - let a,ws,fwd,b,c = List.hd edges in a - -let warning state nodes = - try - Some (snd (List.find (fun x -> fst x = state) nodes)) (* find node for state and return its warning *) - with - | Not_found -> None (* no node for state *) - -let get_lval stmt = - let f = function - | Ptr x -> `Ptr (* TODO recursive *) - | Var s -> `Var - | Ident s -> `Ident - in - Option.map f stmt.lval - -let get_exp = function - | Regex x -> `Regex x - | String x -> `String x - | Bool x -> `Bool x - | Int x -> `Int x - | Float x -> `Float x - | Lval (Var x) -> `Var x - | Lval (Ident x) -> `Ident x - | Fun x -> `Error "Functions aren't allowed to have functions as an argument (put the function as a previous state instead)" - | Exp_ -> `Free - | Unop ("!", Bool x) -> `Bool (not x) - | _ -> `Error "Unsupported operation inside function argument, use a simpler expression instead." - -let get_rval stmt = get_exp stmt.exp - -let get_key_variant stmt = - let rec get_from_exp = function - | Fun f -> get_from_args f.args (* TODO for special we only consider constraints where the root of the exp is Fun (see fname_is) *) - | Lval (Var s) -> `Rval s - | _ -> `None - (* walks over arguments until it finds something or returns `None *) - and get_from_argsi i = function - | [] -> `None - | x::xs -> - match get_from_exp x with - | `Rval s -> `Arg(s, i) - | _ -> get_from_argsi (i+1) xs (* matches `None and `Arg -> `Arg of `Arg not supported *) - and get_from_args args = get_from_argsi 0 args (* maybe better use List.findi *) - in - let rec get_from_lval = function - | Ptr x -> get_from_lval x - | Var s -> Some s - | Ident s -> None - in - match stmt.lval with - | Some lval when Option.is_some (get_from_lval lval) -> `Lval (Option.get (get_from_lval lval)) - | _ -> get_from_exp stmt.exp - -let equal_form lval stmt = - match lval, stmt.lval with - | Some _, Some _ - | None, None -> true - | _ -> false - -(* get function arguments with tags corresponding to the type -> should only be called for functions, returns [] for everything else *) -let get_fun_args stmt = match stmt.exp with - | Fun f -> List.map get_exp f.args - | _ -> [] - -(* functions for output *) -let rec lval_to_string = function - | Ptr x -> "*"^(lval_to_string x) - | Var x -> "$"^x - | Ident x -> x -let rec exp_to_string = function - | Fun x -> x.fname^"("^String.concat ", " (List.map exp_to_string x.args)^")" - | Exp_ -> "_" - | Lval x -> lval_to_string x - | Regex x -> "r\""^x^"\"" - | String x -> "\""^x^"\"" - | Bool x -> string_of_bool x - | Int x -> string_of_int x - | Float x -> string_of_float x - | Binop (op, a, b) -> exp_to_string a ^ " " ^ op ^ " " ^ exp_to_string b - | Unop (op, a) -> op ^ " " ^ exp_to_string a -let stmt_to_string stmt = match stmt.lval, stmt.exp with - | Some lval, exp -> lval_to_string lval^" = "^exp_to_string exp - | None, exp -> exp_to_string exp -let arrow_to_string ws fwd = (String.concat "," ws)^if fwd then ">" else "" -let def_to_string = function - | Node(n, m) -> n^"\t\""^m^"\"" - | Edge(a, ws, fwd, b, s) -> a^" -"^arrow_to_string ws fwd^"> "^b^"\t"^stmt_to_string s - -let to_dot_graph defs = - let no_warnings = true in - let def_to_string = function - | Node(n, m) -> - if no_warnings then "" - else n^"\t[style=filled, fillcolor=orange, label=\""^n^": "^m^"\"];" - | Edge(a, ws, fwd, b, s) -> - let style = if fwd then "style=dotted, " else "" in - let ws = if List.is_empty ws then "" else (String.concat "," ws)^" | " in - a^" -> "^b^"\t["^style^"label=\""^ws^String.escaped (stmt_to_string s)^"\"];" - in - let ends,defs = List.partition (function Edge (a,ws,fwd,b,s) -> b="end" && s.exp=Exp_ | _ -> false) defs in - let endstates = List.filter_map (function Edge (a,ws,fwd,b,s) -> Some a | _ -> None) ends in - (* set the default style for nodes *) - let defaultstyle = "node [shape=box, style=rounded];" in - (* style end nodes and then reset *) - let endstyle = if List.is_empty endstates then "" else "node [peripheries=2]; "^(String.concat " " endstates)^"; node [peripheries=1];" in - let lines = "digraph file {"::defaultstyle::endstyle::(List.map def_to_string defs |> List.filter (fun s -> s<>"")) in - (* List.iter print_endline lines *) - String.concat "\n " lines ^ "\n}" diff --git a/src/spec/specLexer.mll b/src/spec/specLexer.mll deleted file mode 100644 index 64ac69359e..0000000000 --- a/src/spec/specLexer.mll +++ /dev/null @@ -1,67 +0,0 @@ -{ - open SpecParser (* The type token is defined in specParser.mli *) - exception Token of string - let line = ref 1 -} - -let digit = ['0'-'9'] -let alpha = ['a'-'z' 'A'-'Z'] -let nl = '\r'?'\n' (* new line *) -let s = [' ' '\t'] (* whitespace *) -let w = '_' | alpha | digit (* word *) -let endlinecomment = "//" [^'\n']* -let multlinecomment = "/*"([^'*']|('*'+[^'*''/'])|nl)*'*'+'/' -let comments = endlinecomment | multlinecomment -let str = ('\"'(([^'\"']|"\\\"")* as s)'\"') | ('\''(([^'\'']|"\\'")* as s)'\'') - -rule token = parse - | s { token lexbuf } (* skip blanks *) - | comments { token lexbuf } (* skip comments *) - | nl { incr line; EOL } - - (* operators *) - | '(' { LPAREN } - | ')' { RPAREN } - | '[' { LBRACK } - | ']' { RBRACK } - | '{' { LCURL } - | '}' { RCURL } - (*| '.' { DOT } *) - (*| "->" { ARROW } *) - | '+' { PLUS } - | '-' { MINUS } - | '*' { MUL } - | '/' { DIV } - | '%' { MOD } - | '<' { LT } - | '>' { GT } - | "==" { EQEQ } - | "!=" { NE } - | "<=" { LE } - | ">=" { GE } - | "&&" { AND } - | "||" { OR } - | '!' { NOT } - | '=' { EQ } - | ',' { COMMA } - | ';' { SEMICOLON } - - (* literals, identifiers *) - | "true" { BOOL(true) } - | "false" { BOOL(false) } - | "null" { NULL } - | digit+ as x { INT(int_of_string x) } - | str { STRING(s) } - | '_' { UNDERS } (* used for spec, but has to be before Ident! *) - | ('_'|alpha) w* as x { IDENT(x) } - - (* spec *) - | ':' { COLON } - | "$"(w+ as x) { VAR(x) } - | "r" str { REGEX(s) } - | (w+ as n) s+ str - { NODE(n, s) } - | (w+ as a) s* "-" ((w+ ("," w+)*)? as ws) (">"? as fwd) ">" s* (w+ as b) s+ - { EDGE(a, BatString.split_on_string ~by:"," ws, fwd=">", b) } - | eof { EOF } - | _ as x { raise(Token (Char.escaped x^": unknown token in line "^string_of_int !line)) } diff --git a/src/spec/specParser.mly b/src/spec/specParser.mly deleted file mode 100644 index fe8fe90ec8..0000000000 --- a/src/spec/specParser.mly +++ /dev/null @@ -1,116 +0,0 @@ -%{ - (* necessary to open a different compilation unit - because exceptions directly defined here aren't visible outside - (e.g. SpecParser.Eof is raised, but Error: Unbound constructor - if used to catch in a different module) *) - open SpecCore -%} - -%token EOL EOF -/* operators */ -%token LPAREN RPAREN LCURL RCURL LBRACK RBRACK -%token PLUS MINUS MUL DIV MOD -%token LT GT EQEQ NE LE GE AND OR NOT -%token EQ COMMA SEMICOLON -/* literals, identifiers */ -%token BOOL -%token NULL -%token INT -%token STRING -%token IDENT -/* spec */ -%token UNDERS COLON -%token VAR -%token REGEX -%token NODE -%token EDGE - -/* precedence groups from low to high */ -%right EQ -%left OR -%left AND -%left EQEQ NE -%left LT GT LE GE -%left PLUS MINUS -%left MUL DIV MOD -%right NOT UPLUS UMINUS DEREF - -%start file -%type file - -%% - -file: - | def EOL { $1 } - | def EOF { $1 } /* no need for an empty line at the end */ - | EOL { raise Endl } /* empty line */ - | EOF { raise Eof } /* end of file */ -; - -def: - | NODE { Node($1) } - | EDGE stmt { let a, ws, fwd, b = $1 in Edge(a, ws, fwd, b, $2) } -; - -stmt: - | lval EQ expr { {lval = Some $1; exp = $3} } /* TODO expression would be better */ - | expr { {lval = None; exp = $1} } -; - -lval: - | MUL lval %prec DEREF { Ptr $2 } - | IDENT { Ident $1 } /* C identifier, e.g. foo, _foo, _1, but not 1b */ - | VAR { Var $1 } /* spec variable, e.g. $foo, $123, $__ */ -; - -expr: - | LPAREN expr RPAREN { $2 } - | REGEX { Regex $1 } - | STRING { String $1 } - | BOOL { Bool $1 } - | lval { Lval $1 } - | IDENT args { Fun {fname=$1; args=$2} } /* function */ - | UNDERS { Exp_ } - | nexpr { Int $1 } - /* | nexpr LT nexpr { Bool ($1<$3) } - | nexpr GT nexpr { Bool ($1>$3) } - | nexpr EQEQ nexpr { Bool ($1=$3) } - | nexpr NE nexpr { Bool ($1<>$3) } - | nexpr LE nexpr { Bool ($1<=$3) } - | nexpr GE nexpr { Bool ($1>=$3) } */ - | expr OR expr { Binop ("||", $1, $3) } - | expr AND expr { Binop ("&&", $1, $3) } - | expr EQEQ expr { Binop ("==", $1, $3) } - | expr NE expr { Binop ("!=", $1, $3) } - | expr LT expr { Binop ("<", $1, $3) } - | expr GT expr { Binop (">", $1, $3) } - | expr LE expr { Binop ("<=", $1, $3) } - | expr GE expr { Binop (">=", $1, $3) } - | expr PLUS expr { Binop ("+", $1, $3) } - | expr MINUS expr { Binop ("-", $1, $3) } - | expr MUL expr { Binop ("*", $1, $3) } - | expr DIV expr { Binop ("/", $1, $3) } - | expr MOD expr { Binop ("%", $1, $3) } - | NOT expr { Unop ("!", $2) } -; - -nexpr: - | INT { $1 } - | MINUS nexpr %prec UMINUS { - $2 } - | PLUS nexpr %prec UPLUS { $2 } - /* | LPAREN nexpr RPAREN { $2 } - | nexpr PLUS nexpr { $1 + $3 } - | nexpr MINUS nexpr { $1 - $3 } - | nexpr MUL nexpr { $1 * $3 } - | nexpr DIV nexpr { $1 / $3 } */ -; - -args: - | LPAREN RPAREN { [] } - | LPAREN expr_list RPAREN { $2 } -; - -expr_list: - | expr { [$1] } - | expr COMMA expr_list { $1 :: $3 } -; diff --git a/src/spec/specUtil.ml b/src/spec/specUtil.ml deleted file mode 100644 index 55e0b51135..0000000000 --- a/src/spec/specUtil.ml +++ /dev/null @@ -1,52 +0,0 @@ -(* functions for driving specParser *) - -open Batteries - -(* config *) -let save_dot = true - -let line = ref 1 -exception Parse_error of string - -let parse ?repl:(repl=false) ?print:(print=false) ?dot:(dot=false) cin = - let lexbuf = Lexing.from_channel cin in - let defs = ref [] in - (* Printf.printf "\nrepl: %B, print: %B, dot: %B, save_dot: %B\n" repl print dot save_dot; *) - try - while true do (* loop over all lines *) - try - let result = SpecParser.file SpecLexer.token lexbuf in - defs := !defs@[result]; - incr line; - if print then (print_endline (SpecCore.def_to_string result); flush stdout) - with - (* just an empty line -> don't print *) - | SpecCore.Endl -> incr line - (* somehow gets raised in some cases instead of SpecCore.Eof *) - | BatInnerIO.Input_closed -> raise SpecCore.Eof - (* catch and print in repl-mode *) - | e when repl -> print_endline (Printexc.to_string e) - done; - ([], []) (* never happens, but ocaml needs it for type *) - with - (* done *) - | SpecCore.Eof -> - let nodes = List.filter_map (function SpecCore.Node x -> Some x | _ -> None) !defs in - let edges = List.filter_map (function SpecCore.Edge x -> Some x | _ -> None) !defs in - if print then Printf.printf "\n#Definitions: %i, #Nodes: %i, #Edges: %i\n" - (List.length !defs) (List.length nodes) (List.length edges); - if save_dot && not dot then ( - let dotgraph = SpecCore.to_dot_graph !defs in - output_file ~filename:"result/graph.dot" ~text:dotgraph; - print_endline ("saved graph as "^Sys.getcwd ()^"/result/graph.dot"); - ); - if dot then ( - print_endline (SpecCore.to_dot_graph !defs) - ); - (nodes, edges) - (* stop on parsing error if not in REPL and include line number *) - | e -> raise (Parse_error ("Line "^string_of_int !line^": "^Printexc.to_string e)) - -let parseFile filename = parse (open_in filename) - -(* print ~first:"[" ~sep:", " ~last:"]" print_any stdout @@ 5--10 *) diff --git a/src/domains/accessKind.ml b/src/util/library/accessKind.ml similarity index 100% rename from src/domains/accessKind.ml rename to src/util/library/accessKind.ml diff --git a/src/util/library/dune b/src/util/library/dune new file mode 100644 index 0000000000..075c01c35d --- /dev/null +++ b/src/util/library/dune @@ -0,0 +1,18 @@ +(include_subdirs no) + +(library + (name goblint_library) + (public_name goblint.library) + (wrapped false) ; TODO: wrap + (libraries + batteries.unthreaded + goblint_common + goblint_domain + goblint_config + goblint-cil) + (preprocess + (pps + ppx_deriving.std + ppx_deriving_hash))) + +(documentation) diff --git a/src/util/library/library.mld b/src/util/library/library.mld new file mode 100644 index 0000000000..f55db3f2ff --- /dev/null +++ b/src/util/library/library.mld @@ -0,0 +1,14 @@ +{0 Library goblint.library} +This library is unwrapped and provides the following top-level modules. +For better context, see {!Goblint_lib} which also documents these modules. + + +{1 Utilities} + +{2 Library specification} +{!modules: +AccessKind +LibraryDesc +LibraryDsl +LibraryFunctions +} diff --git a/src/analyses/libraryDesc.ml b/src/util/library/libraryDesc.ml similarity index 100% rename from src/analyses/libraryDesc.ml rename to src/util/library/libraryDesc.ml diff --git a/src/analyses/libraryDsl.ml b/src/util/library/libraryDsl.ml similarity index 100% rename from src/analyses/libraryDsl.ml rename to src/util/library/libraryDsl.ml diff --git a/src/analyses/libraryDsl.mli b/src/util/library/libraryDsl.mli similarity index 100% rename from src/analyses/libraryDsl.mli rename to src/util/library/libraryDsl.mli diff --git a/src/analyses/libraryFunctions.ml b/src/util/library/libraryFunctions.ml similarity index 96% rename from src/analyses/libraryFunctions.ml rename to src/util/library/libraryFunctions.ml index 8152e5b886..2c65f7ae61 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -1233,88 +1233,88 @@ open Invalidate * We assume that no known functions that are reachable are executed/spawned. For that we use ThreadCreate above. *) (* WTF: why are argument numbers 1-indexed (in partition)? *) let invalidate_actions = [ - "__printf_chk", readsAll;(*safe*) - "printk", readsAll;(*safe*) - "__mutex_init", readsAll;(*safe*) - "__builtin___snprintf_chk", writes [1];(*keep [1]*) - "__vfprintf_chk", writes [1];(*keep [1]*) - "__builtin_va_arg", readsAll;(*safe*) - "__builtin_va_end", readsAll;(*safe*) - "__builtin_va_start", readsAll;(*safe*) - "__ctype_b_loc", readsAll;(*safe*) - "__errno", readsAll;(*safe*) - "__errno_location", readsAll;(*safe*) - "__strdup", readsAll;(*safe*) - "strtoul__extinline", readsAll;(*safe*) - "readdir_r", writesAll;(*unsafe*) - "atoi__extinline", readsAll;(*safe*) - "_IO_getc", writesAll;(*unsafe*) - "pipe", writesAll;(*unsafe*) - "strerror_r", writesAll;(*unsafe*) - "raise", writesAll;(*unsafe*) - "_strlen", readsAll;(*safe*) - "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) - "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) - "waitpid", readsAll;(*safe*) - "__open_alias", readsAll;(*safe*) - "__open_2", readsAll;(*safe*) - "ioctl", writesAll;(*unsafe*) - "fstat__extinline", writesAll;(*unsafe*) - "scandir", writes [1;3;4];(*keep [1;3;4]*) - "bindtextdomain", readsAll;(*safe*) - "textdomain", readsAll;(*safe*) - "dcgettext", readsAll;(*safe*) - "putw", readsAll;(*safe*) - "__getdelim", writes [3];(*keep [3]*) - "__h_errno_location", readsAll;(*safe*) - "__fxstat", readsAll;(*safe*) - "openlog", readsAll;(*safe*) - "umask", readsAll;(*safe*) - "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*) - "svctcp_create", readsAll;(*safe*) - "clntudp_bufcreate", writesAll;(*unsafe*) - "authunix_create_default", readsAll;(*safe*) - "clnt_broadcast", writesAll;(*unsafe*) - "clnt_sperrno", readsAll;(*safe*) - "pmap_unset", writesAll;(*unsafe*) - "svcudp_create", readsAll;(*safe*) - "svc_register", writesAll;(*unsafe*) - "svc_run", writesAll;(*unsafe*) - "dup", readsAll; (*safe*) - "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) - "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) - "__error", readsAll; (*safe*) - "__maskrune", writesAll; (*unsafe*) - "times", writesAll; (*unsafe*) - "timespec_get", writes [1]; - "__tolower", readsAll; (*safe*) - "signal", writesAll; (*unsafe*) - "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*) - "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*) - "uncompress", writes [3;4]; (*keep [3;4]*) - "__xstat", writes [3]; (*keep [1]*) - "__lxstat", writes [3]; (*keep [1]*) - "remove", readsAll; - "BZ2_bzBuffToBuffCompress", writes [3;4]; (*keep [3;4]*) - "compress2", writes [3]; (*keep [3]*) - "__toupper", readsAll; (*safe*) - "BF_set_key", writes [3]; (*keep [3]*) - "PL_NewHashTable", readsAll; (*safe*) - "assert_failed", readsAll; (*safe*) - "munmap", readsAll;(*safe*) - "mmap", readsAll;(*safe*) - "__builtin_va_arg_pack_len", readsAll; - "__open_too_many_args", readsAll; - "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *) - "dev_driver_string", readsAll; - "__spin_lock_init", writes [1]; - "kmem_cache_create", readsAll; - "idr_pre_get", readsAll; - "zil_replay", writes [1;2;3;5]; - (* ddverify *) - "sema_init", readsAll; - "__goblint_assume_join", readsAll; - ] + "__printf_chk", readsAll;(*safe*) + "printk", readsAll;(*safe*) + "__mutex_init", readsAll;(*safe*) + "__builtin___snprintf_chk", writes [1];(*keep [1]*) + "__vfprintf_chk", writes [1];(*keep [1]*) + "__builtin_va_arg", readsAll;(*safe*) + "__builtin_va_end", readsAll;(*safe*) + "__builtin_va_start", readsAll;(*safe*) + "__ctype_b_loc", readsAll;(*safe*) + "__errno", readsAll;(*safe*) + "__errno_location", readsAll;(*safe*) + "__strdup", readsAll;(*safe*) + "strtoul__extinline", readsAll;(*safe*) + "readdir_r", writesAll;(*unsafe*) + "atoi__extinline", readsAll;(*safe*) + "_IO_getc", writesAll;(*unsafe*) + "pipe", writesAll;(*unsafe*) + "strerror_r", writesAll;(*unsafe*) + "raise", writesAll;(*unsafe*) + "_strlen", readsAll;(*safe*) + "stat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) + "lstat__extinline", writesAllButFirst 1 readsAll;(*drop 1*) + "waitpid", readsAll;(*safe*) + "__open_alias", readsAll;(*safe*) + "__open_2", readsAll;(*safe*) + "ioctl", writesAll;(*unsafe*) + "fstat__extinline", writesAll;(*unsafe*) + "scandir", writes [1;3;4];(*keep [1;3;4]*) + "bindtextdomain", readsAll;(*safe*) + "textdomain", readsAll;(*safe*) + "dcgettext", readsAll;(*safe*) + "putw", readsAll;(*safe*) + "__getdelim", writes [3];(*keep [3]*) + "__h_errno_location", readsAll;(*safe*) + "__fxstat", readsAll;(*safe*) + "openlog", readsAll;(*safe*) + "umask", readsAll;(*safe*) + "clntudp_create", writesAllButFirst 3 readsAll;(*drop 3*) + "svctcp_create", readsAll;(*safe*) + "clntudp_bufcreate", writesAll;(*unsafe*) + "authunix_create_default", readsAll;(*safe*) + "clnt_broadcast", writesAll;(*unsafe*) + "clnt_sperrno", readsAll;(*safe*) + "pmap_unset", writesAll;(*unsafe*) + "svcudp_create", readsAll;(*safe*) + "svc_register", writesAll;(*unsafe*) + "svc_run", writesAll;(*unsafe*) + "dup", readsAll; (*safe*) + "__builtin___vsnprintf", writesAllButFirst 3 readsAll; (*drop 3*) + "__builtin___vsnprintf_chk", writesAllButFirst 3 readsAll; (*drop 3*) + "__error", readsAll; (*safe*) + "__maskrune", writesAll; (*unsafe*) + "times", writesAll; (*unsafe*) + "timespec_get", writes [1]; + "__tolower", readsAll; (*safe*) + "signal", writesAll; (*unsafe*) + "BF_cfb64_encrypt", writes [1;3;4;5]; (*keep [1;3;4,5]*) + "BZ2_bzBuffToBuffDecompress", writes [3;4]; (*keep [3;4]*) + "uncompress", writes [3;4]; (*keep [3;4]*) + "__xstat", writes [3]; (*keep [1]*) + "__lxstat", writes [3]; (*keep [1]*) + "remove", readsAll; + "BZ2_bzBuffToBuffCompress", writes [3;4]; (*keep [3;4]*) + "compress2", writes [3]; (*keep [3]*) + "__toupper", readsAll; (*safe*) + "BF_set_key", writes [3]; (*keep [3]*) + "PL_NewHashTable", readsAll; (*safe*) + "assert_failed", readsAll; (*safe*) + "munmap", readsAll;(*safe*) + "mmap", readsAll;(*safe*) + "__builtin_va_arg_pack_len", readsAll; + "__open_too_many_args", readsAll; + "usb_submit_urb", readsAll; (* first argument is written to but according to specification must not be read from anymore *) + "dev_driver_string", readsAll; + "__spin_lock_init", writes [1]; + "kmem_cache_create", readsAll; + "idr_pre_get", readsAll; + "zil_replay", writes [1;2;3;5]; + (* ddverify *) + "sema_init", readsAll; + "__goblint_assume_join", readsAll; +] let invalidate_actions = let tbl = Hashtbl.create 113 in diff --git a/src/analyses/libraryFunctions.mli b/src/util/library/libraryFunctions.mli similarity index 100% rename from src/analyses/libraryFunctions.mli rename to src/util/library/libraryFunctions.mli diff --git a/src/util/std/dune b/src/util/std/dune index c6961a1725..b074a29937 100644 --- a/src/util/std/dune +++ b/src/util/std/dune @@ -9,7 +9,8 @@ goblint-cil fpath yojson - yaml) + yaml + qcheck-core) (preprocess (pps ppx_deriving.std diff --git a/src/util/std/gobHashtbl.ml b/src/util/std/gobHashtbl.ml index c14bafc0cb..c93244eb47 100644 --- a/src/util/std/gobHashtbl.ml +++ b/src/util/std/gobHashtbl.ml @@ -1,9 +1,5 @@ module Pretty = GoblintCil.Pretty -let magic_stats h = - let h: _ Hashtbl.t = Obj.magic h in (* Batteries Hashtables don't expose stats yet...: https://github.com/ocaml-batteries-team/batteries-included/pull/1079 *) - Hashtbl.stats h - let pretty_statistics () (s: Hashtbl.statistics) = let load_factor = float_of_int s.num_bindings /. float_of_int s.num_buckets in Pretty.dprintf "bindings=%d buckets=%d max_length=%d histo=%a load=%f" s.num_bindings s.num_buckets s.max_bucket_length (Pretty.docList (Pretty.dprintf "%d")) (Array.to_list s.bucket_histogram) load_factor diff --git a/src/common/domains/myCheck.ml b/src/util/std/gobQCheck.ml similarity index 91% rename from src/common/domains/myCheck.ml rename to src/util/std/gobQCheck.ml index 98583cd2c3..12809d5b46 100644 --- a/src/common/domains/myCheck.ml +++ b/src/util/std/gobQCheck.ml @@ -56,7 +56,4 @@ struct let gens = List.map gen arbs in let shrinks = List.map shrink arbs in make ~shrink:(Shrink.sequence shrinks) (Gen.sequence gens) - - open GoblintCil - let varinfo: Cil.varinfo arbitrary = QCheck.always (Cil.makeGlobalVar "arbVar" Cil.voidPtrType) (* S TODO: how to generate this *) end diff --git a/src/util/std/goblint_std.ml b/src/util/std/goblint_std.ml index e716d1df5b..0d548cac08 100644 --- a/src/util/std/goblint_std.ml +++ b/src/util/std/goblint_std.ml @@ -19,6 +19,7 @@ module GobUnix = GobUnix module GobFpath = GobFpath module GobPretty = GobPretty +module GobQCheck = GobQCheck module GobYaml = GobYaml module GobYojson = GobYojson module GobZ = GobZ diff --git a/src/util/tracing/dune b/src/util/tracing/dune new file mode 100644 index 0000000000..7e37139567 --- /dev/null +++ b/src/util/tracing/dune @@ -0,0 +1,9 @@ +(include_subdirs no) + +(library + (name goblint_tracing) + (public_name goblint.tracing) + (libraries + goblint_std + goblint-cil + goblint_build_info)) diff --git a/src/common/util/tracing.ml b/src/util/tracing/goblint_tracing.ml similarity index 84% rename from src/common/util/tracing.ml rename to src/util/tracing/goblint_tracing.ml index ad8892c396..0e5580b036 100644 --- a/src/common/util/tracing.ml +++ b/src/util/tracing/goblint_tracing.ml @@ -4,6 +4,7 @@ * large domains we output. The original code generated the document object * even when the subsystem is not activated. *) +open Goblint_std open GoblintCil open Pretty @@ -67,13 +68,6 @@ let trace sys ?var fmt = gtrace true printtrace sys var ignore fmt * c: continue/normal print w/o indent-change *) -let tracel sys ?var fmt = - let loc = !current_loc in - let docloc sys doc = - printtrace sys (dprintf "(%a)@?" CilType.Location.pretty loc ++ indent 2 doc); - in - gtrace true docloc sys var ~loc ignore fmt - let tracei (sys:string) ?var ?(subsys=[]) fmt = let f sys d = printtrace sys d; traceIndent () in let g () = activate sys subsys in @@ -85,13 +79,3 @@ let traceu sys fmt = let f sys d = printtrace sys d; traceOutdent () in let g () = deactivate sys in gtrace true f sys None g fmt - - -let traceli sys ?var ?(subsys=[]) fmt = - let loc = !current_loc in - let g () = activate sys subsys in - let docloc sys doc: unit = - printtrace sys (dprintf "(%a)" CilType.Location.pretty loc ++ indent 2 doc); - traceIndent () - in - gtrace true docloc sys var ~loc g fmt diff --git a/tests/regression/18-file/01-ok.c b/tests/regression/18-file/01-ok.c deleted file mode 100644 index 5c1f21ff1c..0000000000 --- a/tests/regression/18-file/01-ok.c +++ /dev/null @@ -1,12 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - fp = fopen("test.txt", "a"); - fprintf(fp, "Testing...\n"); - fclose(fp); -} - -// All ok! diff --git a/tests/regression/18-file/02-function.c b/tests/regression/18-file/02-function.c deleted file mode 100644 index fc3157c264..0000000000 --- a/tests/regression/18-file/02-function.c +++ /dev/null @@ -1,17 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -void f(){ - fp = fopen("test.txt", "a"); -} - -int main(){ - f(); - fprintf(fp, "Testing...\n"); - fclose(fp); -} - -// All ok! diff --git a/tests/regression/18-file/03-if-close.c b/tests/regression/18-file/03-if-close.c deleted file mode 100644 index b2bf1ebe97..0000000000 --- a/tests/regression/18-file/03-if-close.c +++ /dev/null @@ -1,15 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - int b; - fp = fopen("test.txt", "a"); // WARN: MAYBE file is never closed - - fprintf(fp, "Testing...\n"); - - if (b) - fclose(fp); -} // WARN: MAYBE unclosed files: fp diff --git a/tests/regression/18-file/04-no-open.c b/tests/regression/18-file/04-no-open.c deleted file mode 100644 index 70683f3852..0000000000 --- a/tests/regression/18-file/04-no-open.c +++ /dev/null @@ -1,10 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - fprintf(fp, "Testing...\n"); // WARN: writing to unopened file handle fp - fclose(fp); // WARN: closeing unopened file handle fp -} diff --git a/tests/regression/18-file/05-open-mode.c b/tests/regression/18-file/05-open-mode.c deleted file mode 100644 index 77326d7a70..0000000000 --- a/tests/regression/18-file/05-open-mode.c +++ /dev/null @@ -1,11 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - fp = fopen("test.txt", "r"); - fprintf(fp, "Testing...\n"); // WARN: writing to read-only file handle fp - fclose(fp); -} diff --git a/tests/regression/18-file/06-2open.c b/tests/regression/18-file/06-2open.c deleted file mode 100644 index 2826c2f1dc..0000000000 --- a/tests/regression/18-file/06-2open.c +++ /dev/null @@ -1,12 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - fp = fopen("test1.txt", "a"); // WARN: file is never closed - fp = fopen("test2.txt", "a"); // WARN: overwriting still opened file handle fp - fprintf(fp, "Testing...\n"); - fclose(fp); -} // WARN: unclosed files: fp diff --git a/tests/regression/18-file/07-2close.c b/tests/regression/18-file/07-2close.c deleted file mode 100644 index 0545bf9814..0000000000 --- a/tests/regression/18-file/07-2close.c +++ /dev/null @@ -1,11 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - fp = fopen("test.txt", "a"); - fprintf(fp, "Testing...\n"); - fclose(fp); - fclose(fp); // WARN: closeing already closed file handle fp -} diff --git a/tests/regression/18-file/08-var-reuse.c b/tests/regression/18-file/08-var-reuse.c deleted file mode 100644 index 1caa238517..0000000000 --- a/tests/regression/18-file/08-var-reuse.c +++ /dev/null @@ -1,15 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - fp = fopen("test.txt", "a"); - fprintf(fp, "Testing...\n"); - fclose(fp); - fp = fopen("test2.txt", "a"); - fprintf(fp, "Testing...\n"); - fclose(fp); -} - -// All ok! diff --git a/tests/regression/18-file/09-inf-loop-no-close.c b/tests/regression/18-file/09-inf-loop-no-close.c deleted file mode 100644 index e9563ef195..0000000000 --- a/tests/regression/18-file/09-inf-loop-no-close.c +++ /dev/null @@ -1,17 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - int i; - fp = fopen("test.txt", "a"); // WARN: file is never closed - - while (i){ - fprintf(fp, "Testing...\n"); - i++; - } - - //fclose(fp); -} // WARN: unclosed files: fp diff --git a/tests/regression/18-file/10-inf-loop-ok.c b/tests/regression/18-file/10-inf-loop-ok.c deleted file mode 100644 index d88fde272e..0000000000 --- a/tests/regression/18-file/10-inf-loop-ok.c +++ /dev/null @@ -1,19 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - int i; - fp = fopen("test.txt", "a"); - - while (i){ - fprintf(fp, "Testing...\n"); - i++; - } - - fclose(fp); -} - -// All ok. diff --git a/tests/regression/18-file/11-2if.c b/tests/regression/18-file/11-2if.c deleted file mode 100644 index e24fec6e46..0000000000 --- a/tests/regression/18-file/11-2if.c +++ /dev/null @@ -1,18 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - int b; - fp = fopen("test.txt", "a"); // WARN: MAYBE file is never closed - - if (b) - fclose(fp); - - fprintf(fp, "Testing...\n"); // WARN: MAYBE writing to closed file handle fp - - if (!b) - fclose(fp); // WARN: MAYBE closeing already closed file handle fp -} // WARN: MAYBE unclosed files: fp diff --git a/tests/regression/18-file/12-2close-if.c b/tests/regression/18-file/12-2close-if.c deleted file mode 100644 index 4934b33114..0000000000 --- a/tests/regression/18-file/12-2close-if.c +++ /dev/null @@ -1,15 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - int b; - fp = fopen("test.txt", "a"); - fprintf(fp, "Testing...\n"); - - if (b) - fclose(fp); - - fclose(fp); // WARN: MAYBE closeing already closed file handle fp -} diff --git a/tests/regression/18-file/13-ptr-arith-ok.c b/tests/regression/18-file/13-ptr-arith-ok.c deleted file mode 100644 index f707110957..0000000000 --- a/tests/regression/18-file/13-ptr-arith-ok.c +++ /dev/null @@ -1,16 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - fp = fopen("test.txt", "a"); // WARN: MAYBE file is never closed - fprintf(fp, "Testing...\n"); - - fp++; // WARN: changed pointer fp (no longer safe) - fp--; // WARN: changed pointer fp (no longer safe) - - fclose(fp); // WARN: MAYBE closeing already closed file handle fp -} // WARN: MAYBE unclosed files: fp - -// OPT: All ok! diff --git a/tests/regression/18-file/14-ptr-arith-close.c b/tests/regression/18-file/14-ptr-arith-close.c deleted file mode 100644 index 3f9cd21ee2..0000000000 --- a/tests/regression/18-file/14-ptr-arith-close.c +++ /dev/null @@ -1,13 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - fp = fopen("test.txt", "a"); // WARN: MAYBE file is never closed - fprintf(fp, "Testing...\n"); - - fp++; // WARN: changed pointer fp (no longer safe) - - fclose(fp); // WARN: MAYBE closeing already closed file handle fp -} // WARN: MAYBE unclosed files: fp diff --git a/tests/regression/18-file/15-var-switch.c b/tests/regression/18-file/15-var-switch.c deleted file mode 100644 index d7f74b85db..0000000000 --- a/tests/regression/18-file/15-var-switch.c +++ /dev/null @@ -1,18 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp1; - fp1 = fopen("test.txt", "a"); - fprintf(fp1, "Testing...\n"); - - FILE *fp2; - fp2 = fopen("test.txt", "a"); // WARN: file is never closed - fprintf(fp2, "Testing...\n"); - - fp2 = fp1; - - fclose(fp1); - fclose(fp2); // WARN: closeing already closed file handle fp2 -} // WARN: unclosed files: fp2 diff --git a/tests/regression/18-file/16-var-reuse-close.c b/tests/regression/18-file/16-var-reuse-close.c deleted file mode 100644 index cb1fb5fd22..0000000000 --- a/tests/regression/18-file/16-var-reuse-close.c +++ /dev/null @@ -1,14 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - fp = fopen("test.txt", "a"); - fprintf(fp, "Testing...\n"); - fclose(fp); - - fp = fopen("test.txt", "a"); // WARN: file is never closed - fprintf(fp, "Testing...\n"); - // fclose(fp); -} // WARN: unclosed files: fp diff --git a/tests/regression/18-file/17-myfopen.c b/tests/regression/18-file/17-myfopen.c deleted file mode 100644 index 3e005c6e70..0000000000 --- a/tests/regression/18-file/17-myfopen.c +++ /dev/null @@ -1,21 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - - -FILE* myfopen(){ - // FILE *fp_tmp = fopen("test.txt", "a"); // local! - return fopen("test.txt", "a"); -} - -int main(){ - FILE *fp1; - FILE *fp2; - fp1 = myfopen(); - fp2 = myfopen(); // WARN: file is never closed - - fprintf(fp1, "Testing...\n"); - fclose(fp1); - fprintf(fp2, "Testing...\n"); - // fclose(fp2); -} // WARN: unclosed files: fp2 diff --git a/tests/regression/18-file/18-myfopen-arg.c b/tests/regression/18-file/18-myfopen-arg.c deleted file mode 100644 index 5d98db4c53..0000000000 --- a/tests/regression/18-file/18-myfopen-arg.c +++ /dev/null @@ -1,20 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - - -FILE* myfopen(char* f){ - return fopen(f, "a"); -} - -int main(){ - FILE *fp1; - FILE *fp2; - fp1 = myfopen("test1.txt"); - fp2 = myfopen("test2.txt"); // WARN: file is never closed - - fprintf(fp1, "Testing...\n"); - fclose(fp1); - fprintf(fp2, "Testing...\n"); - // fclose(fp2); -} // WARN: unclosed files: fp2 diff --git a/tests/regression/18-file/19-if-close-else.c b/tests/regression/18-file/19-if-close-else.c deleted file mode 100644 index 049e8454b4..0000000000 --- a/tests/regression/18-file/19-if-close-else.c +++ /dev/null @@ -1,17 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - int b; - fp = fopen("test.txt", "a"); - - if (b) - fclose(fp); - else - fprintf(fp, "Testing...\n"); - - fclose(fp); // WARN: MAYBE closeing already closed file handle fp -} diff --git a/tests/regression/18-file/20-loop-close.c b/tests/regression/18-file/20-loop-close.c deleted file mode 100644 index 981248c152..0000000000 --- a/tests/regression/18-file/20-loop-close.c +++ /dev/null @@ -1,18 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - int i; - fp = fopen("test.txt", "a"); // WARN: MAYBE file is never closed - - while (i){ // May closed (11, 3), open(test.txt, Write) (7, 3) - fprintf(fp, "Testing...\n"); // WARN: MAYBE writing to closed file handle fp - fclose(fp); // WARN: MAYBE closeing already closed file handle fp - i++; - } - // why: fp -> Must open(test.txt, Write) (7, 3) - // -> because loop wouldn't exit? -} // WARN: MAYBE unclosed files: fp diff --git a/tests/regression/18-file/21-for-i.c b/tests/regression/18-file/21-for-i.c deleted file mode 100644 index e41bb9b005..0000000000 --- a/tests/regression/18-file/21-for-i.c +++ /dev/null @@ -1,26 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE *fp; - -int main(){ - int i; - fp = fopen("test.txt", "w"); // WARN: MAYBE file is never closed - - for(i=1; i<10; i++){ // join - // i -> Unknown int - if(i%2){ - // i -> Unknown int - // fprintf(fp, "Testing...%s\n", i); // Segmentation fault! - // actually shouldn't warn because open and close are always alternating... - fprintf(fp, "Testing...%i\n", i); // WARN: MAYBE writing to closed file handle fp - fclose(fp); // WARN: MAYBE closeing already closed file handle fp - }else{ - fp = fopen("test.txt", "a"); // WARN: MAYBE file is never closed - } - // why no join? - } - // fp opened or closed? (last i=9 -> open) - // widening -> Warn: might be unclosed -} // WARN: MAYBE unclosed files: fp diff --git a/tests/regression/18-file/22-f_int.c b/tests/regression/18-file/22-f_int.c deleted file mode 100644 index f0376fc5a9..0000000000 --- a/tests/regression/18-file/22-f_int.c +++ /dev/null @@ -1,13 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int f(int x){ - return 2*x; -} - -int main(){ - int a = 1; - a = f(2); - return 0; -} diff --git a/tests/regression/18-file/23-f_str.c b/tests/regression/18-file/23-f_str.c deleted file mode 100644 index 81224d2e72..0000000000 --- a/tests/regression/18-file/23-f_str.c +++ /dev/null @@ -1,13 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -char* f(char* x){ - return x; -} - -int main(){ - char* a = "foo"; - a = f("bar"); - return 0; -} diff --git a/tests/regression/18-file/24-f_wstr.c b/tests/regression/18-file/24-f_wstr.c deleted file mode 100644 index 2379c1f718..0000000000 --- a/tests/regression/18-file/24-f_wstr.c +++ /dev/null @@ -1,14 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include -#include - -wchar_t* f(wchar_t* x){ - return x; -} - -int main(){ - wchar_t* a = L"foo"; - a = f(L"bar"); - return 0; -} diff --git a/tests/regression/18-file/25-mem-ok.c b/tests/regression/18-file/25-mem-ok.c deleted file mode 100644 index 00ba189b8d..0000000000 --- a/tests/regression/18-file/25-mem-ok.c +++ /dev/null @@ -1,29 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp[3]; - // Array -> varinfo with index-offset - fp[1] = fopen("test.txt", "a"); - fprintf(fp[1], "Testing...\n"); - fclose(fp[1]); - - - struct foo { - int i; - FILE *fp; - } bar; - // Struct -> varinfo with field-offset - bar.fp = fopen("test.txt", "a"); - fprintf(bar.fp, "Testing...\n"); - fclose(bar.fp); - - - // Pointer -> Mem exp - *(fp+2) = fopen("test.txt", "a"); - fprintf(*(fp+2), "Testing...\n"); - fclose(*(fp+2)); -} - -// All ok! diff --git a/tests/regression/18-file/26-open-error-ok.c b/tests/regression/18-file/26-open-error-ok.c deleted file mode 100644 index 5cf3aaf7bb..0000000000 --- a/tests/regression/18-file/26-open-error-ok.c +++ /dev/null @@ -1,15 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main (){ - FILE *fp; - fp = fopen("test.txt", "w"); - - if(fp!=NULL){ - fprintf(fp, "Testing..."); - fclose(fp); - } -} - -// All ok! diff --git a/tests/regression/18-file/27-open-error.c b/tests/regression/18-file/27-open-error.c deleted file mode 100644 index bd3048208f..0000000000 --- a/tests/regression/18-file/27-open-error.c +++ /dev/null @@ -1,13 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main (){ - FILE *fp; - fp = fopen("test.txt", "w"); // WARN: MAYBE file is never closed - - if(fp==NULL){ - fprintf(fp, "Testing..."); // WARN: writing to unopened file handle fp - fclose(fp); // WARN: closeing unopened file handle fp - } -} // WARN: MAYBE unclosed files: fp diff --git a/tests/regression/18-file/28-multiple-exits.c b/tests/regression/18-file/28-multiple-exits.c deleted file mode 100644 index 04fa5abab0..0000000000 --- a/tests/regression/18-file/28-multiple-exits.c +++ /dev/null @@ -1,14 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - fp = fopen("test.txt", "a"); // WARN: MAYBE file is never closed - fprintf(fp, "Testing...\n"); - int b; - if(b) - return 1; // WARN: unclosed files: fp - fclose(fp); - return 0; -} diff --git a/tests/regression/18-file/29-alias-global.c b/tests/regression/18-file/29-alias-global.c deleted file mode 100644 index 17b94748c0..0000000000 --- a/tests/regression/18-file/29-alias-global.c +++ /dev/null @@ -1,22 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE* fp; -FILE* myfopen(char* f){ - fp = fopen(f, "a"); - return fp; -} - -int main(){ - FILE *fp1; - FILE *fp2; - fp1 = myfopen("test1.txt"); - fp2 = myfopen("test2.txt"); - fprintf(fp1, "Testing...\n"); - fclose(fp1); - fprintf(fp2, "Testing...\n"); - fclose(fp2); -} - -// All ok! diff --git a/tests/regression/18-file/30-ptr-of-ptr.c b/tests/regression/18-file/30-ptr-of-ptr.c deleted file mode 100644 index 5a8d1f97a9..0000000000 --- a/tests/regression/18-file/30-ptr-of-ptr.c +++ /dev/null @@ -1,14 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp1; - fp1 = fopen("test.txt", "a"); - FILE **fp2; - - fp2 = &fp1; - - fclose(fp1); - fclose(*fp2); // WARN: closeing already closed file handle fp1 -} diff --git a/tests/regression/18-file/31-var-reuse-fun.c b/tests/regression/18-file/31-var-reuse-fun.c deleted file mode 100644 index 9c0ccb16a2..0000000000 --- a/tests/regression/18-file/31-var-reuse-fun.c +++ /dev/null @@ -1,16 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -FILE* myfopen(char* f){ - FILE* fp; - fp = fopen(f, "a"); - return fp; -} - -int main(){ - FILE *fp; - fp = fopen("test1.txt", "a"); // WARN: file is never closed - fp = myfopen("test2.txt"); // WARN: overwriting still opened file handle fp - fclose(fp); -} // WARN: unclosed files: fp diff --git a/tests/regression/18-file/32-multi-ptr-close.c b/tests/regression/18-file/32-multi-ptr-close.c deleted file mode 100644 index e252d563a5..0000000000 --- a/tests/regression/18-file/32-multi-ptr-close.c +++ /dev/null @@ -1,25 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp1; - fp1 = fopen("test1.txt", "a"); - fprintf(fp1, "Testing...\n"); - - FILE *fp2; - fp2 = fopen("test2.txt", "a"); - fprintf(fp2, "Testing...\n"); - - FILE **fp; - int b; - if(b){ - fp = &fp1; - }else{ - fp = &fp2; - } - - fclose(*fp); - fclose(fp1); // WARN: MAYBE closeing already closed file handle fp1 - fclose(fp2); // WARN: MAYBE closeing already closed file handle fp2 -} diff --git a/tests/regression/18-file/33-multi-ptr-open.c b/tests/regression/18-file/33-multi-ptr-open.c deleted file mode 100644 index b3cfa0ade4..0000000000 --- a/tests/regression/18-file/33-multi-ptr-open.c +++ /dev/null @@ -1,23 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp1; - fp1 = fopen("test1.txt", "a"); // WARN: MAYBE file is never closed - - FILE *fp2; - fp2 = fopen("test2.txt", "r"); // WARN: MAYBE file is never closed - - FILE **fp; - int b; - if(b){ - fp = &fp1; - }else{ - fp = &fp2; - } - - fprintf(*fp, "Testing...\n"); // WARN: MAYBE writing to read-only file handle fp - - fclose(*fp); -} // WARN: MAYBE unclosed files: fp1, fp2 diff --git a/tests/regression/18-file/34-multi-alias-close.c b/tests/regression/18-file/34-multi-alias-close.c deleted file mode 100644 index 0ebb9ddd30..0000000000 --- a/tests/regression/18-file/34-multi-alias-close.c +++ /dev/null @@ -1,25 +0,0 @@ -// SKIP PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp1; - fp1 = fopen("test1.txt", "a"); - fprintf(fp1, "Testing...\n"); - - FILE *fp2; - fp2 = fopen("test2.txt", "a"); - fprintf(fp2, "Testing...\n"); - - FILE *fp; - int b; - if(b){ - fp = fp1; - }else{ - fp = fp2; - } - - fclose(fp); - fclose(fp1); // WARN: MAYBE closeing already closed file handle fp1 - fclose(fp2); // WARN: MAYBE closeing already closed file handle fp2 -} diff --git a/tests/regression/18-file/35-multi-alias-open.c b/tests/regression/18-file/35-multi-alias-open.c deleted file mode 100644 index 21a4a9cca6..0000000000 --- a/tests/regression/18-file/35-multi-alias-open.c +++ /dev/null @@ -1,23 +0,0 @@ -// SKIP PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp1; - fp1 = fopen("test1.txt", "a"); // WARN: MAYBE file is never closed - - FILE *fp2; - fp2 = fopen("test2.txt", "r"); // WARN: MAYBE file is never closed - - FILE *fp; - int b; - if(b){ - fp = fp1; - }else{ - fp = fp2; - } - - fprintf(fp, "Testing...\n"); // WARN: MAYBE writing to read-only file handle fp - - fclose(fp); -} // WARN: MAYBE unclosed files: fp1, fp2 diff --git a/tests/regression/18-file/36-fun-ptr.c b/tests/regression/18-file/36-fun-ptr.c deleted file mode 100644 index 4f70bf7382..0000000000 --- a/tests/regression/18-file/36-fun-ptr.c +++ /dev/null @@ -1,14 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp; - FILE* (*f)(const char *, const char*); - f = fopen; - fp = f("test.txt", "a"); - fprintf(fp, "Testing...\n"); - fclose(fp); -} - -// All ok! diff --git a/tests/regression/18-file/37-var-switch-alias.c b/tests/regression/18-file/37-var-switch-alias.c deleted file mode 100644 index 5dfde5a2d9..0000000000 --- a/tests/regression/18-file/37-var-switch-alias.c +++ /dev/null @@ -1,18 +0,0 @@ -// PARAM: --set ana.activated[+] "'file'" --enable ana.file.optimistic - -#include - -int main(){ - FILE *fp1; - fp1 = fopen("test.txt", "a"); - fprintf(fp1, "Testing...\n"); - - FILE *fp2; - fp2 = fopen("test.txt", "a"); // WARN: file is never closed - fprintf(fp2, "Testing...\n"); - - fp2 = fp1; - - fclose(fp2); - fclose(fp1); // WARN: closeing already closed file handle fp1 -} // WARN: unclosed files: fp2 diff --git a/tests/regression/18-file/README.md b/tests/regression/18-file/README.md new file mode 100644 index 0000000000..0e93e175c6 --- /dev/null +++ b/tests/regression/18-file/README.md @@ -0,0 +1,2 @@ +The file analysis has been removed from recent Goblint versions, please use Release 2.3.0 +Folder is left in place to avoid renumbering all tests diff --git a/tests/regression/18-file/file.c b/tests/regression/18-file/file.c deleted file mode 100644 index fc2ebe1699..0000000000 --- a/tests/regression/18-file/file.c +++ /dev/null @@ -1,44 +0,0 @@ -#include - -int main(){ - - // no errors - FILE *fp; - fp = fopen("test.txt", "a"); - if(fp!=0) { - fprintf(fp, "Testing...\n"); - fclose(fp); - } - - // missing fopen -> compiles, but leads to Segmentation fault - FILE *fp2; - // fp2 = fopen("test.txt", "a"); - fprintf(fp2, "Testing...\n"); // WARN - fclose(fp2); // WARN - - // writing to a read-only file -> doesn't do anything - FILE *fp3; - fp3 = fopen("test.txt", "r"); - fprintf(fp3, "Testing...\n"); // (WARN) - fclose(fp3); - - // accessing closed file -> write doesn't do anything - FILE *fp4; - fp4 = fopen("test.txt", "a"); - fclose(fp4); - fprintf(fp4, "Testing...\n"); // WARN - - // missing fclose - FILE *fp5; - fp5 = fopen("test.txt", "a"); // WARN - fprintf(fp5, "Testing...\n"); - - // missing assignment to file handle - fopen("test.txt", "a"); // WARN - - - // bad style: - // opening file but not doing anything - - return 0; // WARN about all unclosed files -} \ No newline at end of file diff --git a/tests/regression/18-file/file.optimistic.spec b/tests/regression/18-file/file.optimistic.spec deleted file mode 100644 index d42e2217b7..0000000000 --- a/tests/regression/18-file/file.optimistic.spec +++ /dev/null @@ -1,34 +0,0 @@ -w1 "file handle is not saved!" -w2 "closeing unopened file handle $" -w3 "writing to unopened file handle $" -w4 "writing to read-only file handle $" -w5 "closeing already closed file handle $" -w6 "writing to closed file handle $" -w7 "overwriting still opened file handle $" -w8 "unrecognized file open mode for file handle $" - -1 -> w1 fopen(_, _) -1 -> w2 fclose($fp) -1 -> w3 fprintf($fp, _) -1 -> open_read $fp = fopen(path, "r") -1 -> open_write $fp = fopen(path, r"[wa]") // see OCaml doc for details (e.g. \\| for alternatives) -1 -> w8 $fp = fopen(path, _) - -open_read -> w4 fprintf($fp, _) - -open_read -w7>> 1 $fp = fopen(path, _) -open_write -w7>> 1 $fp = fopen(path, _) - -open_read -> closed fclose($fp) -open_write -> closed fclose($fp) - -closed -> w5 fclose($fp) -closed -> w6 fprintf($fp, _) -closed ->> 1 _ // let state 1 handle the rest - -// setup which states are end states -1 -> end _ -closed -> end _ -// warning for all entries that are not in an end state -_end "file is never closed" -_END "unclosed files: $" \ No newline at end of file diff --git a/tests/regression/18-file/file.spec b/tests/regression/18-file/file.spec deleted file mode 100644 index aeb747abfd..0000000000 --- a/tests/regression/18-file/file.spec +++ /dev/null @@ -1,57 +0,0 @@ -w1 "file handle is not saved!" -w2 "closeing unopened file handle $" -w3 "writing to unopened file handle $" -w4 "writing to read-only file handle $" -w5 "closeing already closed file handle $" -w6 "writing to closed file handle $" -w7 "overwriting still opened file handle $" -w8 "unrecognized file open mode for file handle $" - -// TODO later add fputs and stuff -1 -> w1 fopen(_, _) -1 -> w2 fclose($fp) -1 -> w3 fprintf($fp, _) -//1 -> open_read $fp = fopen(path, "r") -//1 -> open_write $fp = fopen(path, r"[wa]") // see OCaml doc for details (e.g. \\| for alternatives) -//1 -> w8 $fp = fopen(path, _) - -// go to unchecked states first -1 -> u_open_read $fp = fopen(path, "r") -1 -> u_open_write $fp = fopen(path, r"[wa]") -1 -> w8 $fp = fopen(path, _) -// once branch(exp, tv) is matched, return dom with 1. arg (lval = exp) and true/false -// forwarding from branch is not possible (would need an extra map for storing states) -> ignore it -// warnings are also ignored -// then in branch take out lval, check exp and do the transition to a checked state -u_open_read -> 1 branch($key==0, true) -u_open_read -> open_read branch($key==0, false) -u_open_write -> 1 branch($key==0, true) -u_open_write -> open_write branch($key==0, false) - -// alternative: forward everything. Problem: saving arguments of call (special_fn -> branch -> special_fn) -// 1 ->> open_check $fp = fopen(path, _) -// open_check ->> 1 branch($fp==0, true) -// open_check ->> open branch($fp==0, false) -// open -> open_read $fp = fopen(path, "r") -// open -> open_write $fp = fopen(path, "[wa]") -// open -> w8 $fp = fopen(path, _) - -open_read -> w4 fprintf($fp, _) -// open_write -> open_write fprintf($fp, _) // not needed, but changes loc - -open_read -w7>> 1 $fp = fopen(path, _) -open_write -w7>> 1 $fp = fopen(path, _) - -open_read -> closed fclose($fp) -open_write -> closed fclose($fp) - -closed -> w5 fclose($fp) -closed -> w6 fprintf($fp, _) -closed ->> 1 _ // let state 1 handle the rest - -// setup which states are end states -1 -> end _ -closed -> end _ -// warning for all entries that are not in an end state -_end "file is never closed" -_END "unclosed files: $" \ No newline at end of file diff --git a/tests/regression/19-spec/01-malloc-free.c b/tests/regression/19-spec/01-malloc-free.c deleted file mode 100644 index 43ee527dba..0000000000 --- a/tests/regression/19-spec/01-malloc-free.c +++ /dev/null @@ -1,19 +0,0 @@ -#include -#include - -int main(){ - int *ip; - //*ip = 5; // segfault - //printf("%i", *ip); // segfault - ip = malloc(sizeof(int)); // assume malloc never fails - - // do stuff - //*ip = 5; - - free(ip); - //free(ip); // crash: double free or corruption - *ip = 5; // undefined but no crash - printf("%i", *ip); // undefined but printed 5 - ip = NULL; // make sure the pointer is not used anymore - *ip = 5; // segfault -} diff --git a/tests/regression/19-spec/02-mutex_rc.c b/tests/regression/19-spec/02-mutex_rc.c deleted file mode 100644 index 82c1642a93..0000000000 --- a/tests/regression/19-spec/02-mutex_rc.c +++ /dev/null @@ -1,23 +0,0 @@ -#include -#include - -int myglobal; -pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; -pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; - -void *t_fun(void *arg) { - pthread_mutex_lock(&mutex1); - myglobal=myglobal+1; // RACE! - pthread_mutex_unlock(&mutex1); - return NULL; -} - -int main(void) { - pthread_t id; - pthread_create(&id, NULL, t_fun, NULL); - pthread_mutex_lock(&mutex2); - myglobal=myglobal+1; // RACE! - pthread_mutex_unlock(&mutex2); - pthread_join (id, NULL); - return 0; -} diff --git a/tests/regression/19-spec/README.md b/tests/regression/19-spec/README.md new file mode 100644 index 0000000000..d7e3ae3c8e --- /dev/null +++ b/tests/regression/19-spec/README.md @@ -0,0 +1,2 @@ +The spec analysis has been removed from recent Goblint versions, please use Release 2.3.0 +Folder is left in place to avoid renumbering all tests diff --git a/tests/regression/19-spec/malloc.optimistic.spec b/tests/regression/19-spec/malloc.optimistic.spec deleted file mode 100644 index 860c573814..0000000000 --- a/tests/regression/19-spec/malloc.optimistic.spec +++ /dev/null @@ -1,23 +0,0 @@ -w1 "pointer is not saved [leak]" -w2 "freeing unallocated pointer $ [segfault?]" -w3 "writing to unallocated pointer $ [segfault?]" -w4 "overwriting unfreed pointer $ [leak]" -w5 "freeing already freed pointer $ [double free!]" - -1 -w1> 1 malloc(_) -1 -w2> 1 free($p) -1 -w3> 1 *$p = _ -1 -> alloc $p = malloc(_) // TODO does compiler check size? - -alloc -w4> alloc $p = malloc(_) -alloc -> freed free($p) - -freed -w5> freed free($p) -freed ->> 1 _ // let state 1 handle the rest - -// setup which states are end states -1 -> end _ -freed -> end _ -// warning for all entries that are not in an end state -_end "pointer is never freed" -_END "unfreed pointers: $" \ No newline at end of file diff --git a/tests/regression/19-spec/malloc.spec b/tests/regression/19-spec/malloc.spec deleted file mode 100644 index 9f09430051..0000000000 --- a/tests/regression/19-spec/malloc.spec +++ /dev/null @@ -1,26 +0,0 @@ -w1 "pointer is not saved [leak]" -w2 "freeing unallocated pointer $ [segfault?]" -w3 "writing to unallocated pointer $ [segfault?]" -w4 "overwriting unfreed pointer $ [leak]" -w5 "freeing already freed pointer $ [double free!]" - -1 -w1> 1 malloc(_) -1 -w2> 1 free($p) -1 -w3> 1 *$p = _ -1 -> u_alloc $p = malloc(_) - -u_alloc -> 1 branch($key==0, true) -u_alloc -> alloc branch($key==0, false) - -alloc -w4> alloc $p = malloc(_) -alloc -> freed free($p) - -freed -w5> freed free($p) -freed ->> 1 _ // let state 1 handle the rest - -// setup which states are end states -1 -> end _ -freed -> end _ -// warning for all entries that are not in an end state -_end "pointer is never freed" -_END "unfreed pointers: $" \ No newline at end of file diff --git a/tests/regression/19-spec/mutex-lock.spec b/tests/regression/19-spec/mutex-lock.spec deleted file mode 100644 index 1ec8264078..0000000000 --- a/tests/regression/19-spec/mutex-lock.spec +++ /dev/null @@ -1,31 +0,0 @@ -w1 "unlocking not locked mutex" -w2 "locking already locked mutex" - -1 -w1> 1 pthread_mutex_unlock($p) -1 -> lock pthread_mutex_lock($p) - -lock -w2> lock pthread_mutex_lock($p) -lock -> 1 pthread_mutex_unlock($p) - -// setup which states are end states -1 -> end _ -// warning for all entries that are not in an end state -_end "mutex is never unlocked" -_END "locked mutexes: $" - - - -//w1 "joining not created thread" -//w2 "overwriting id of already created thread" -// -//1 -w1> 1 pthread_join ($p, _) -//1 -> created pthread_create($p, _, _, _) -// -//created -w2> created pthread_create($p, _, _, _) -//created -> 1 pthread_join ($p, _) -// -//// setup which states are end states -//1 -> end _ -//// warning for all entries that are not in an end state -//_end "thread is never joined" -//_END "unjoined threads: $" \ No newline at end of file diff --git a/tests/regression/39-signed-overflows/06-abs.c b/tests/regression/39-signed-overflows/06-abs.c index e56cc9ff7d..1323434cbc 100644 --- a/tests/regression/39-signed-overflows/06-abs.c +++ b/tests/regression/39-signed-overflows/06-abs.c @@ -17,6 +17,13 @@ int main() { __goblint_check(-100 <= data); int result = data * data; //NOWARN } + + if(abs(data) - 1 <= 99) + { + __goblint_check(data <= 100); + __goblint_check(-100 <= data); + int result = data * data; //NOWARN + } } return 8; } \ No newline at end of file diff --git a/tests/regression/51-threadjoins/07-trivial-unknowntid.c b/tests/regression/51-threadjoins/07-trivial-unknowntid.c new file mode 100644 index 0000000000..2797291ee3 --- /dev/null +++ b/tests/regression/51-threadjoins/07-trivial-unknowntid.c @@ -0,0 +1,34 @@ +//PARAM: --set ana.activated[+] threadJoins +#include + +int g = 10; +int h = 10; +pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + g++; // RACE! + return NULL; +} + +void *t_benign(void *arg) { + h++; // NORACE + pthread_t id2; + pthread_create(&id2, NULL, t_fun, NULL); + foo(&id2); + pthread_join(id2, NULL); + return NULL; +} + +int main(void) { + int t; + + pthread_t id2; + pthread_create(&id2, NULL, t_benign, NULL); + pthread_join(id2, NULL); + // t_benign and t_fun should be in here + + g++; // RACE! + h++; // NORACE + + return 0; +} diff --git a/unittest/dune b/unittest/dune index 7313aa964b..a08a4b2323 100644 --- a/unittest/dune +++ b/unittest/dune @@ -2,7 +2,7 @@ (test (name mainTest) - (libraries ounit2 qcheck-ounit goblint.lib goblint.sites.dune goblint.build-info.dune) + (libraries ounit2 qcheck-ounit goblint.std goblint.lib goblint.sites.dune goblint.build-info.dune) (preprocess (pps ppx_deriving.std ppx_deriving_hash ppx_deriving_yojson)) (flags :standard -linkall)) diff --git a/unittest/util/intOpsTest.ml b/unittest/util/intOpsTest.ml index 611f2f546f..307d9e84b0 100644 --- a/unittest/util/intOpsTest.ml +++ b/unittest/util/intOpsTest.ml @@ -1,4 +1,5 @@ open OUnit2 +open Goblint_std open Goblint_lib (* If the first operand of a div is negative, Zarith rounds the result away from zero. @@ -10,13 +11,13 @@ let old_div a b = if Z.lt a Z.zero then Z.neg (Z.ediv (Z.neg a) b) else Z.ediv a let old_rem a b = Z.sub a (Z.mul b (old_div a b)) let test_bigint_div = - QCheck.(Test.make ~name:"div" (pair MyCheck.Arbitrary.big_int MyCheck.Arbitrary.big_int) (fun (x, y) -> + QCheck.(Test.make ~name:"div" (pair GobQCheck.Arbitrary.big_int GobQCheck.Arbitrary.big_int) (fun (x, y) -> assume (Z.compare y Z.zero <> 0); Z.equal (Z.div x y) (old_div x y) )) let test_bigint_rem = - QCheck.(Test.make ~name:"rem" (pair MyCheck.Arbitrary.big_int MyCheck.Arbitrary.big_int) (fun (x, y) -> + QCheck.(Test.make ~name:"rem" (pair GobQCheck.Arbitrary.big_int GobQCheck.Arbitrary.big_int) (fun (x, y) -> assume (Z.compare y Z.zero <> 0); Z.equal (Z.rem x y) (old_rem x y) ))