JANALYZER(1)

📦
version 6.6.0 · 2 versions
  • 6.6.0 · debian trixie, ubuntu questing, ubuntu resolute, ubuntu stonking (latest)
  • 5.12 · ubuntu jammy
, in debian trixie, ubuntu questing, ubuntu resolute, ubuntu stonking

🌸 NAME 🌸

janalyzer — data-flow analysis for Java bytecode 💖 (yes bestie, this is the JANALYZER(1) page, we're doing this together)

✨ SYNOPSIS ✨

janalyzer [-?] [-h] [--help]
       show help

janalyzer method-name
       Use the fully qualified name of a method as entry point, e.g.,
       'mypackage.Myclass.foo:(I)Z'

janalyzer class-name
       The entry point is the method specified by --function, or
       otherwise, the public static void main(String[]) method of the
       given class class-name.

janalyzer -jar jarfile
       JAR file to be checked.  The entry point is the method specified
       by --function or otherwise, the public static void main(String[])
       method of the class specified by --main-class or the main class
       specified in the JAR manifest (checked in this order).

janalyzer --gb goto-binary
       GOTO binary file to be checked.  The entry point is the method
       specified by --function, or otherwise, the public static void
       main(String[]) of the class specified by --main-class (checked in
       this order).

ok so like. here's the vibe 💅 you can feed this thing a method name, a class name, a -jar file, or a --gb GOTO binary, and it'll figure out where to start. the entry-point rules are very specific and they go in a specific order, so pay attention bestie 👑

🎀 DESCRIPTION 🎀

the original left this section empty, so... we match energy. no notes. moving on 🫶

🔥 OPTIONS 🔥

  • -classpath dirs/jars, -cp dirs/jars, --classpath dirs/jars — sets the class search path for directories and jar files. it's a colon-separated list of directories and JAR archives, and that's what gets searched for class files. 📂
  • --main-class class-name — sets the name of the main class. that's it. that's the whole thing.
  • --function name — sets the entry point function name. main character selection, basically ✨

🌈 Task options:

  • --show — displays a domain for every instruction in the GOTO binary. the format and the info it shows depend on which domain got selected. so like, results may vary depending on the vibe you picked 🦋
  • --verify — every property in the program gets checked to see if it's true (it always holds), unreachable, false if it is reachable (and ngl, because the analysis is over-approximate, it's not clear whether locations are actually reachable or whether it's just an overapproximation — so this is literally the best that can be achieved), or unknown. if multiple points of execution reach the same location, each one gets checked and the answers get combined, with unknown taking precedence. so unknown wins every fight, no cap 💀
  • --simplify file_name — writes a new version of the input program to file_name, with the program simplified using info from the abstract interpreter. the exact simplification depends on the domain used, but typically it might be replacing any expression that has a constant value. if this makes instructions unreachable (like if a GOTO can be shown to never be taken), they get removed 🗑️. you can deactivate that removal by passing --no-simplify-slicing. ideally simplify would be idempotent (i.e. running it a second time wouldn't simplify anything more than the first run did). but there are edge cases that are difficult or prohibitively expensive to handle in the domain, and those can make a second (or more) run give more simplification. submitting bug reports for these is helpful but they may not be viable to fix. it's giving "we tried our best" 😭
  • --no-simplify-slicing — don't remove instructions from which no property can be reached. use it with --simplify. 🫶
  • --unreachable-instructions — lists which instructions have a domain that is bottom (i.e. unreachable). if --function was used to set the program entry point, then this can flag things like the main function as unreachable. rude but valid 🙈
  • --unreachable-functions — same vibe as --unreachable-instructions, but it reports which functions are definitely unreachable rather than just instructions. glow-up from instructions to whole functions, slay.
  • --reachable-functions — the negation of --unreachable-functions. reports which functions may be reachable. heads up though: because the analysis is over-approximate, it's possible this will mark functions as reachable when a more precise analysis (possibly using jbmc(1)) would show there are no execution traces that reach them. so it's a little optimistic. it's giving hopeful 💖

🧚 Abstract interpreter options:

  • --location-sensitive — use location-sensitive abstract interpreter. yes bestie, location-sensitive, it's in the name ✨
  • --concurrent — this extends abstract interpretation with very restricted and special purpose handling of threads. ⚠️ this needs the domain to have certain unusual properties for it to give a correct answer. at the time of writing, only --dependence-graph is compatible with it. so like, don't freestyle this one.

👑 Domain options:

  • --constants — the default option. stores one constant value per variable. this means it's fast but it will only find things that can be resolved by constant propagation. the domain has some handling of arrays but limited support for pointers, which means it can potentially give unsound behavior. 🚩 noted, bestie.
  • --intervals — a domain that stores an interval for each integer and float variable. at the time of writing, not all operations are supported, so the results can be quite over-approximate at points. it also has limitations in the handling of pointers, so it can give unsound results. 😬 same warning energy.
  • --non-null — this domain is intended to find which pointers are not null. its implementation is very limited and it is not recommended. that's the whole review. not recommended. periodt. 💀
  • --dependence-graph — tracks data flow and information flow dependencies between instructions and produces a graph. this includes doing points-to analysis and tracking reaching definitions (i.e. use-def chains). this is one of the most extensive, correct and feature complete domains. it's the main character of domains, honestly 👑✨

🎀 Output options:

these options control how the result of the task is output. the default is text to the standard output. in the case of tasks that produce goto-programs (--simplify for example), the output options only affect the logging and not the final form of the program. so like, don't expect them to reshape your program, they're just here for the logging vibes 🦋

  • --text file_name — output results in plain text to the given file.
  • --json file_name — writes the output as a JSON object to file_name. 🍓
  • --xml file_name — output results in XML format to file_name.
  • --dot file_name — writes the output in dot(1) format to file_name. this is only supported by some domains and tasks (for example --show --dependence-graph). so like, check before you commit 💅

🌸 Specific analyses:

  • --taint file_name — perform taint analysis using rules in the given file. 🔥
  • --show-taint — print taint analysis results on stdout. right there, on your screen, taint.
  • --show-local-may-alias — perform procedure-local may alias analysis.

🦋 Java Bytecode frontend options:

  • --disable-uncaught-exception-check — ignore uncaught exceptions and errors. 🙈
  • --throw-assertion-error — throw java.lang.AssertionError on violated assert statements instead of failing at the location of the assert statement.
  • --throw-runtime-exceptions — make implicit runtime exceptions explicit. ✨
  • --assert-no-exceptions-thrown — transform throw instructions into assert FALSE followed by assume FALSE.
  • --max-nondet-array-length N — limit nondet (e.g. input) array size to at most N.
  • --max-nondet-tree-depth N — limit size of nondet (e.g. input) object tree; at level N references are set to null.
  • --java-assume-inputs-non-null — never initialize reference-typed parameter to the entry point with null.
  • --java-assume-inputs-interval [L:U] or [L:] or [:U] — force numerical primitive-typed inputs (byte, short, int, long, float, double) to be initialized within the given range; lower bound L and upper bound U must be integers; does not work for arrays. 📏
  • --java-assume-inputs-integral — force float and double inputs to have integer values; does not work for arrays;
  • --java-max-vla-length N — limit the length of user-code-created arrays to N.
  • --java-cp-include-files r — regular expression or JSON list of files to load (with '@' prefix).
  • --java-load-class CLASS — also load code from class CLASS.
  • --java-no-load-class CLASS — never load code from class CLASS.
  • --ignore-manifest-main-class — ignore Main-Class entries in JAR manifest files. if this option is specified and the options --function and --main-class are not, we can be certain that all classes in the JAR file are loaded. certainty is kinda iconic ngl 👑
  • --context-include i, --context-exclude e — only analyze code matching specification i that does not match specification e, if --context-exclude e is also used. all other methods are excluded, i.e., we load their signatures and meta-information, but not their bodies. a specification is any prefix of a package, class or method name, e.g. "org.cprover." or "org.cprover.MyClass." or "org.cprover.MyClass.methodToStub:(I)Z". these options can be given multiple times. the default for context-include is 'all included'; default for context-exclude is 'nothing excluded'. 🎀
  • --no-lazy-methods — load and translate all methods given on the command line and in --classpath. default is to load methods that appear to be reachable from the --function entry point or main class. note that --show-symbol-table, --show-goto-functions and --show-properties output are restricted to loaded methods by default.
  • --lazy-methods-extra-entry-point METHODNAME — treat METHODNAME as a possible program entry point for the purpose of lazy method loading. METHODNAME can be a regular expression that will be matched against all symbols. if missing, a java:: prefix will be added. if no descriptor is found, all overloads of a method will also be added. ✨
  • --static-values f — load initial values of static fields from the given JSON file. we assign static fields to these values instead of calling the normal static initializer (clinit) method. the argument can be a relative or absolute path to the file. 🍓
  • --java-lift-clinit-calls — lifts clinit calls in function bodies to the top of the function. this may reduce the overall cost of static initialisation, but may be unsound if there are cyclic dependencies between static initializers due to potentially changing their order of execution, or if static initializers have side-effects such as updating another class' static field. ⚠️ big caveat energy, read it twice bestie.

more coming in part 2, don't go anywhere 🫶

✨ Platform options ✨

  • --arch arch — sets the analysis architecture, and bestie it defaults to the host architecture. Pick one of: alpha, arm, arm64, armel, armhf, hppa, i386, ia64, mips, mips64, mips64el, mipsel, mipsn32, mipsn32el, powerpc, ppc64, ppc64le, riscv64, s390, s390x, sh4, sparc, sparc64, v850, x32, x86_64, or none. (yeah none is a whole mood but it's valid 💅)
  • --os os — sets the analysis operating system, defaults to whatever your host is running. Your options are: freebsd, linux, macos, netbsd, openbsd, solaris, hurd, or windows.
  • --i386-linux, --i386-win32, --i386-macos, --ppc-macos, --win32, --winx64 — these are the two-for-one specials, they set both the analysis architecture AND the operating system in one go. slay ✨
  • --LP64, --ILP64, --LLP64, --ILP32, --LP32 — sets the width of int, long and pointers, but lowkey does NOT override the default architecture and operating system. it's giving "just the widths, thanks" 🎀
  • --16, --32, --64 — the shorties. --16 is equivalent to --LP32, --32 is equivalent to --ILP32, and --64 is equivalent to --LP64 (or --LLP64 if you're on Windows, iykyk).
  • --little-endian — allows little-endian word-byte conversions 🦋
  • --big-endian — allows big-endian word-byte conversions 🌸
  • --gcc — uses GCC as the preprocessor 💅

✨ Program representations ✨

  • --show-parse-tree — shows the parse tree 🌳
  • --show-symbol-table — shows the loaded symbol table
  • --show-goto-functions — shows the loaded goto program
  • --list-goto-functions — lists the loaded goto functions (yes bestie, list and show are different things, we respect the distinction here)
  • --show-properties — shows the properties, but fr fr does NOT run the analysis. look only, no touching 👑

✨ Program instrumentation options ✨

  • --no-assertions — ignores user assertions 🫶
  • --no-assumptions — ignores user assumptions
  • --property id — enables selected properties only. like a guest list but for properties 🎀

✨ Other options ✨

  • --version — shows the version and exits. dramatic exit, love that for it 💅
  • --verbosity n — sets the verbosity level
  • --timestamp [monotonic|wall] — prints microsecond-precision timestamps. monotonic: the stamps increase monotonically (they only ever go up, no cap 📈). wall: ISO-8601 wall clock timestamps.

🌈 ENVIRONMENT 🌈

Every single tool out here honors the TMPDIR environment variable whenever it's generating temporary files and directories. so if you want your temp stuff to live somewhere specific, that's the vibe check right there ✨

💀 BUGS 💀

If you encounter a problem (and bestie, we hope you don't, but if you do 😭), please create an issue at:

https://github.com/diffblue/cbmc/issues

👀 SEE ALSO 👀

2016-2018, Daniel Kroening, Diffblue

and that's the whole page, bestie! this was janalyzer-5.59.0 from June 2022, aka JANALYZER(1). you ate that read, periodt 🎀✨🦋💅

📦 where this page comes from