GOTO-SYNTHESIZER(1)

📦
version 6.8.0 · 3 versions
, in fedora 44, nixos 26.05

💖 GOTO-SYNTHESIZER 💖

okay bestie, sit down, hydrate, because we're about to talk about goto-synthesizer from the User Commands section of the manual (yes, section 1, iykyk). she's the one who rolls up to your GOTO binary and is like "not to be dramatic but I'm going to make you a loop contract and then rebuild you" 🦋✨

✨ NAME ✨

goto-synthesizer — Synthesize and apply loop contracts of goto binaries.

like. she synthesizes. she applies. she does it to goto binaries. that's the whole vibe 🎀

🌸 SYNOPSIS 🌸

goto-synthesizer [-?] [-h] [--help]
       show help

goto-synthesizer --version
       show version and exit

goto-synthesizer [options] in [out]
       perform synthesis and loop-contracts transformation

three whole modes, bestie, pick your fighter 💅

  • [-?] [-h] [--help] — show help (the classic "hello what are u")
  • --version — show version and exit (the classic "who even are u")
  • [options] in [out] — perform synthesis and loop-contracts transformation (the classic "let's GO")

👑 DESCRIPTION 👑

goto-synthesis reads a GOTO binary, performs loop-contracts synthesis and program transformation for the synthesized contracts, and then writes the resulting program as GOTO binary on disk.

fr fr. she reads the binary, she synthesizes the loop contracts, she transforms the program to match those synthesized contracts, and then she writes the whole glow-up back out to disk as a GOTO binary. main character energy, no cap 💖

💅 OPTIONS 💅

  • -loop-contracts-no-unwind — do not unwind transformed loops after applying the synthesized loop contracts. like, we're leaving those loops exactly as they are, bestie, no take-backs 🔥
  • --dump-loop-contracts — dump the synthesized loop contracts as JSON. dump it, queen, let it all out 💀
  • --json-pt file — specify the output destination of the loop-contracts JSON. file is where that JSON is going. tell her where, she'll put it there 🫶

🌈 Accepts all of cbmc's options plus the following backend options 🌈

yes bestie, ALL of cbmc's options. every single one. plus these backend ones below 👇
  • --object-bits n — number of bits used for object addresses
  • --sat-solver solver — use specified SAT solver
  • --external-sat-solver cmd — command to invoke SAT solver process
  • --no-sat-preprocessor — disable the SAT solver's simplifier
  • --dimacs — generate CNF in DIMACS format
  • --beautify — beautify the counterexample (greedy heuristic)
  • --smt1 — use default SMT1 solver (obsolete). obsolete, girlie, you've been warned 🍓
  • --smt2 — use default SMT2 solver (Z3)
  • --bitwuzla — use Bitwuzla
  • --boolector — use Boolector
  • --cprover-smt2 — use CPROVER SMT2 solver
  • --cvc3 — use CVC3
  • --cvc4 — use CVC4
  • --cvc5 — use CVC5
  • --mathsat — use MathSAT
  • --yices — use Yices
  • --z3 — use Z3
  • --fpa — use theory of floating-point arithmetic
  • --external-smt2-solver cmd — Use cmd to invoke the SMT2 solver. Combine with one of the solver choices for solver-specific constraints. 🧚
  • --refine — use refinement procedure (experimental). experimental!! she said it herself 🙈
  • --refine-arrays — use refinement for arrays only
  • --refine-arithmetic — refinement of arithmetic expressions only
  • --max-node-refinement — maximum refinement iterations for arithmetic expressions
  • --incremental-smt2-solver cmd — Use the incremental SMT backend where cmd is the command to invoke the SMT solver of choice.

Example invocations:

--incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver).
--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental'
(use the CVC5 solver).

Note that:

  • The solver name must be in the "PATH" or be an executable with full path.
  • The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin.
  • The SMT solver should support the QF_AUFBV logic.

ok literally read those three bullets twice bestie, they're the whole assignment ⭐

  • --outfile filename — output formula to given file
  • --dump-smt-formula filename — output smt incremental formula to the given file
  • --write-solver-stats-to json-file — collect the solver query complexity
  • --arrays-uf-never — never turn arrays into uninterpreted functions
  • --arrays-uf-always — always turn arrays into uninterpreted functions

🎀 User-interface options 🎀

  • --xml-ui — use XML-formatted output
  • --json-ui — use JSON-formatted output
  • --verbosity n — verbosity level

🦋 ENVIRONMENT 🦋

All tools honor the TMPDIR environment variable when generating temporary files and directories.

so if you want your temp files somewhere specific, set TMPDIR and she'll respect it. she's polite like that 💜

💀 BUGS 💀

If you encounter a problem please create an issue at https://github.com/diffblue/cbmc/issues

not me telling you to file a bug report but like. if something's broken, tell the devs, they literally want to know 😭

🌟 SEE ALSO 🌟

cbmc(1), goto-cc(1) goto-instrument(1)

the whole friend group, honestly 💖

2022, Qinheping Hu

periodt. that's the copyright, we respect it 👑

and that's the page bestie!! this one's from goto-synthesizer-5.59.0, dated December 2022, and it lives in the GOTO-SYNTHESIZER(1) manual section. go synthesize something iconic 🎀✨💅

📦 where this page comes from