No crucible prefix

[brianhuffman]

Add new saw-script function names without "crucible_" prefix.

LLVM-specific function names with the prefix "crucible_" have been switched to use the prefix "llvm_".

The original names remain in place, with documentation strings referring to the new names.

[brianhuffman]

See #382.

[brianhuffman]

Here's the full list of renamings:

crucible_java_extract -> jvm_extract
crucible_llvm_cfg -> llvm_cfg
crucible_llvm_extract -> llvm_extract
crucible_llvm_compositional_extract -> llvm_compositional_extract
crucible_fresh_var -> llvm_fresh_var
crucible_fresh_cryptol_var -> llvm_fresh_cryptol_var
crucible_alloc -> llvm_alloc
crucible_alloc_aligned -> llvm_alloc_aligned
crucible_alloc_readonly -> llvm_alloc_readonly
crucible_alloc_readonly_aligned -> llvm_alloc_readonly_aligned
crucible_alloc_with_size -> llvm_alloc_with_size
crucible_symbolic_alloc -> llvm_symbolic_alloc
crucible_alloc_global -> llvm_alloc_global
crucible_fresh_pointer -> llvm_fresh_pointer
crucible_fresh_expanded_val -> llvm_fresh_expanded_val
crucible_points_to -> llvm_points_to
crucible_conditional_points_to -> llvm_conditional_points_to
crucible_points_to_untyped -> llvm_points_to_untyped
crucible_conditional_points_to_untyped -> llvm_conditional_points_to_untyped
crucible_points_to_array_prefix -> llvm_points_to_array_prefix
crucible_equal -> llvm_equal
crucible_precond -> llvm_precond
crucible_postcond -> llvm_postcond
crucible_execute_func -> llvm_execute_func
crucible_return -> llvm_return
crucible_llvm_verify -> llvm_verify
crucible_llvm_unsafe_assume_spec -> llvm_unsafe_assume_spec
crucible_llvm_array_size_profile -> llvm_array_size_profile
crucible_llvm_verify_x86 -> llvm_verify_x86
crucible_array -> llvm_array_value
crucible_struct -> llvm_struct_value
crucible_packed_struct -> llvm_packed_struct_value
crucible_elem -> llvm_elem
crucible_field -> llvm_field
crucible_null -> llvm_null
crucible_global -> llvm_global
crucible_global_initializer -> llvm_global_initializer
crucible_term -> llvm_term
crucible_declare_ghost_state -> llvm_declare_ghost_state
crucible_ghost_value -> llvm_ghost_value
crucible_spec_solvers -> llvm_spec_solvers
crucible_spec_size -> llvm_spec_size

The pattern is quite regular, but for a few exceptions: The SetupValue constructors crucible_array and crucible_struct would have been renamed to llvm_array and llvm_struct, except those names were already taken as constructors for LLVMType. So to avoid a clash, they have been renamed to llvm_array_value and llvm_struct_value. For consistency, crucible_packed_struct has also been renamed to llvm_packed_struct_value. It would be nicer to have shorter names for these things, but at least they are not nearly so commonly-used as the other renamed functions that did get significantly shorter.

I have not updated CHANGES.md to mention the new function names; we should probably do that.

Also, it would be nice to similarly rename a couple of saw-script type names like CrucibleMethodSpec and CrucibleSetup to avoid the Crucible prefix; LLVMMethodSpec (or just LLVMSpec) and LLVMSetup would be better names.

[atomb]

Would you be able to add some text to CHANGES.md as part of this PR?

I like the LLVMSpec and LLVMSetup names for the related types.

[atomb]

This looks great. Thanks for going as far as updating the help text for the crucible_ commands to mention that they're legacy. We can perhaps deprecate them for the next release.