Skip to content

v1.6

Latest
Latest

Choose a tag to compare

View all tags
@aschwerdfeger-galois aschwerdfeger-galois released this 17 Sep 21:42
· 51 commits to master since this release
v1.6
0897511

This release supports version 13 of mir-json's schema.

New Features

  • SAWScript now supports optional named arguments. These can be passed anywhere in a function application using the syntax name=val. If val requires parentheses you can also enclose the name in the parentheses as well. The syntax in a type signature is name?type. The parameter syntax in a function declaration is either name?=val or name@alt?=val, where val is the default value to use when the caller doesn't provide one. By default the name is both the external call name and the internal variable name for the parameter. If alt is present, it can be an identifier or a pattern, and specifies a different name or names for internal use. The alternate name, or parts of it, can be set to _ if unused.

  • The builtin str_concats now accepts an optional argument sep to use as a separator between the given strings. For example, str_concats ["a", "b"] will produce "ab" as before, but str_concats sep=", " ["a", "b"] produces "a, b".

  • The SAWScript typechecker will now (sometimes, at least) guess when you forgot a semicolon.

  • The new subproof builtin is similar to "bullets" in Rocq: When there are multiple remaining proof goals, it runs the given inner proof script on the first goal alone, and then checks that the inner script completely proves the goal.

  • The SAW proof commands prove and prove_print now accept SAWCore terms of type Prop, in addition to predicates returning Bool. Previously this required a special proof command prove_extcore, which is now deprecated in favor of prove_print.

  • The REPL once again accepts pure expressions as well as monadic statements. These are not accepted in monadic contexts in SAWScript files, as should be the case. (That was not, however, the historic behavior.)

  • SAW now includes map : {a, b} (a -> b) -> [a] -> [b] as a primitive.

  • Add new SAWScript commands timeout_handle and timeout for adding time limits to scripts.

  • Add new SAWScript MIR commands mir_field_value and mir_field_ref for accessing fields of structs by value and by reference.

  • Added the :llvmdis REPL command. When in the REPL and working with an LLVMModule, this allows examination of the text form of the LLVMModule bitcode. The requested output can be either: (1) a function, (2) the LLVM corresponding to a source file and source line number, or (3) the unnamed Metadata at the requested index.

  • Add basic support for Cryptol Rational values in SAWCore.

  • Add support for derived Cryptol instances in SAWCore.

  • Added llvm_alloc_all_globals, llvm_alloc_constant_globals and llvm_alloc_no_globals to determine the automatic allocation globals. Previously, only constant globals were allocated by default. The globals allocation occurs before the LLVMSetup operation for llvm_verify, so the global allocation disposition must be set as a TopLevel operation.

  • Add mir_set_exception_context_{none,limited,no_limit}, which configures how much call-stack-related context to include when displaying MIR-related exceptions. The default setting is mir_set_exception_context_limited 10 (i.e., 10 call stack frames).

Bug Fixes

  • include_once no longer gets confused by different ../dir/file.saw pathnames starting from different directories.

  • The SAWScript typechecker no longer allows _ <- e as the last statement in a block. Use the plain expression instead.

  • The Rocq exporter now generates more or less normal width output instead of cramming everything onto one very long line.

  • Fix bug in the rme solver causing the < operator to be treated as <=.

  • Avoid exponential blow-up when generating uninterpreted functions.

  • SAW no longer spuriously rejects mir_array_values that use a signed integer type (e.g., mir_i32) as an element type.

  • Using a fractional Cryptol literal (e.g., 0.5 : Rational) no longer causes SAW to emit a type error.

  • Don't raise spurious type errors when importing Cryptol record or tuple update expressions.

  • Don't raise spurious type errors when importing Cryptol case expressions whose scrutinee types have sophisticated numeric types.

  • Fix a panic when importing Cryptol list patterns (e.g., (x, y) where [x, y] = [0x1, 0x2]).

  • LLVM module importing now supports DISubrangeType (metadata ID 48) and DIFixedPointType (metadata ID 49) elements.

  • SAW no longer panics when defining Cryptol functions using numeric constraint guards in let {{ ... }} blocks.

  • Fix a bug that would cause the offline_w4_unint_yices proof script to always throw an error.

Deprecations

  • As noted above, prove_extcore is deprecated in favor of just using prove_print.

  • add_prelude_eqs and add_cryptol_eqs are now deprecated; use add_core_thms instead.

  • The assume_unsat builtin has been deprecated, after five years' notice that this was coming. Use admit instead.

  • The old type names CrucibleSetup and CrucibleMethodSpec have been deprecated and will now cause warnings. Use LLVMSetup and LLVMSpec instead respectively. CrucibleSetup remains a reserved word, and will likely remain one until it is finally removed.

  • The (less old) name SetupValue is deprecated and will now cause warnings. USe LLVMValue instead.

  • The deprecated CVC4 builtins are now hidden by default. Use CVC5. Boolector remains for now.

  • The old crucible_* names that have long been changed to llvm_* names are now hidden by default, except for the ones that never made it past experimental and were already hidden by default; those have now been removed. Exception: crucible_verify_llvm_x86 was left off the original deprecation list and is now hidden by default.

  • llvm_declare_ghost_state and crucible_declare_ghost_state, which are old names for declare_ghost_state, are now hidden by default.

  • The following other deprecated items are also now hidden by default:

    • The coq-based names for the Rocq exporter. Use the rocq versions instead.
    • external_aig_solver (old name for arbitrary_aig)
    • external_cnf_solver (old name for arbitrary_cnf)
    • w4_offline_smtlib2 (old name for offline_w4_smtlib2)

  • The deprecated env builtin has been removed. Use the :env REPL command instead.

Other changes

  • The REPL no longer prints result values you explicitly throw away with _ <- .

  • The way the :search REPL command matches function types has been adjusted. It should be more predictable and more useful now. Feedback is welcome.

  • crux-mir-comp has been unbundled from the SAW release distribution in preparation for creating a standalone Crux release.

Assets 23
Loading