Skip to content

Commit

Permalink
clear compiler options to use bcs and adopt additional_named_address (#…
Browse files Browse the repository at this point in the history 
…114)
  • Loading branch information
@beer-1
beer-1 authored Aug 23, 2024
1 parent f4aabeb commit 35a5621
Show file tree
Hide file tree
Showing 27 changed files with 1,067 additions and 1,867 deletions.
255 changes: 13 additions & 242 deletions api/bindings_compiler.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,22 +14,6 @@
#include <stdlib.h>


enum CoverageOption {
/**
* Display a coverage summary for all modules in this package
*/
CoverageOption_Summary = 0,
/**
* Display coverage information about the module against source code
*/
CoverageOption_Source = 1,
/**
* Display coverage information about the module against disassembled bytecode
*/
CoverageOption_Bytecode = 2,
};
typedef uint8_t CoverageOption;

enum ErrnoValue {
ErrnoValue_Success = 0,
ErrnoValue_Other = 1,
Expand Down Expand Up @@ -97,253 +81,40 @@ typedef struct {
size_t len;
} ByteSliceView;

typedef struct {
/**
* Compile in 'dev' mode. The 'dev-addresses' and 'dev-dependencies' fields will be used if
* this flag is set. This flag is useful for development of packages that expose named
* addresses that are not set to a specific value.
*/
bool dev_mode;
/**
* Compile in 'test' mode. The 'dev-addresses' and 'dev-dependencies' fields will be used
* along with any code in the 'tests' directory.
*/
bool test_mode;
/**
* Generate documentation for packages
*/
bool generate_docs;
/**
* Generate ABIs for packages
*/
bool generate_abis;
/**
* Installation directory for compiled artifacts. Defaults to current directory.
*/
ByteSliceView install_dir;
/**
* Force recompilation of all packages
*/
bool force_recompilation;
/**
* Only fetch dependency repos to MOVE_HOME
*/
bool fetch_deps_only;
/**
* Skip fetching latest git dependencies
*/
bool skip_fetch_latest_git_deps;
/**
* bytecode version. set 0 to unset and to use default
*/
uint32_t bytecode_version;
/**
* Compiler version. set 0 to unset and to use default
*/
uint32_t compiler_version;
/**
* language version. set 0 to unset and to use default
*/
uint32_t language_version;
} CompilerBuildConfig;

typedef struct {
/**
* Path to a package which the command should be run with respect to.
*/
ByteSliceView package_path;
/**
* Print additional diagnostics if available.
*/
bool verbose;
/**
* Package build options
*/
CompilerBuildConfig build_config;
} CompilerArgument;

typedef struct {
ByteSliceView module_name;
} CompilerCoverageBytecodeOption;

typedef struct {
ByteSliceView module_name;
} CompilerCoverageSourceOption;

typedef struct {
/**
* Whether function coverage summaries should be displayed
*/
bool functions;
/**
* Output CSV data of coverage
*/
bool output_csv;
} CompilerCoverageSummaryOption;

typedef struct {
/**
* Whether to include private declarations and implementations into the generated
* documentation. Defaults to false.
*/
bool include_impl;
/**
* Whether to include specifications in the generated documentation. Defaults to false.
*/
bool include_specs;
/**
* Whether specifications should be put side-by-side with declarations or into a separate
* section. Defaults to false.
*/
bool specs_inlined;
/**
* Whether to include a dependency diagram. Defaults to false.
*/
bool include_dep_diagram;
/**
* Whether details should be put into collapsed sections. This is not supported by
* all markdown, but the github dialect. Defaults to false.
*/
bool collapsed_sections;
/**
* Package-relative path to an optional markdown template which is a used to create a
* landing page. Placeholders in this file are substituted as follows: `> {{move-toc}}` is
* replaced by a table of contents of all modules; `> {{move-index}}` is replaced by an index,
* and `> {{move-include NAME_OF_MODULE_OR_SCRIP}}` is replaced by the the full
* documentation of the named entity. (The given entity will not longer be placed in
* its own file, so this can be used to create a single manually populated page for
* the package.)
*/
ByteSliceView landing_page_template;
/**
* Package-relative path to a file whose content is added to each generated markdown file.
* This can contain common markdown references fpr this package (e.g. `[move-book]: <url>`).
*/
ByteSliceView references_file;
} CompilerDocgenOption;

typedef struct {
ByteSliceView verbosity;
/**
* Filters targets out from the package. Any module with a matching file name will
* be a target, similar as with `cargo test`.
*/
ByteSliceView filter;
/**
* Whether to display additional information in error reports. This may help
* debugging but also can make verification slower.
*/
bool trace;
/**
* Whether to use cvc5 as the smt solver backend. The environment variable
* `CVC5_EXE` should point to the binary.
*/
bool cvc5;
/**
* The depth until which stratified functions are expanded.
*/
size_t stratification_depth;
/**
* A seed for the prover.
*/
size_t random_seed;
/**
* The number of cores to use for parallel processing of verification conditions.
*/
size_t proc_cores;
/**
* A (soft) timeout for the solver, per verification condition, in seconds.
*/
size_t vc_timeout;
/**
* Whether to check consistency of specs by injecting impossible assertions.
*/
bool check_inconsistency;
/**
* Whether to keep loops as they are and pass them on to the underlying solver.
*/
bool keep_loops;
/**
* Number of iterations to unroll loops. set 0 to unset
*/
uint64_t loop_unroll;
/**
* Whether output for e.g. diagnosis shall be stable/redacted so it can be used in test
* output.
*/
bool stable_test_output;
/**
* Whether to dump intermediate step results to files.
*/
bool dump;
/**
* indicating that this prover run is for a test.
*/
bool for_test;
} CompilerProveOption;

typedef struct {
/**
* A filter string to determine which unit tests to run. A unit test will be run only if it
* contains this string in its fully qualified (<addr>::<module_name>::<fn_name>) name.
*/
ByteSliceView filter;
/**
* Report test statistics at the end of testing
*/
bool report_statistics;
/**
* Show the storage state at the end of execution of a failing test
*/
bool report_storage_on_error;
/**
* Ignore compiler's warning, and continue run tests
*/
bool ignore_compile_warnings;
/**
* Collect coverage information for later use with the various `package coverage` subcommands
*/
bool compute_coverage;
} CompilerTestOption;

UnmanagedVector build_move_package(UnmanagedVector *errmsg, CompilerArgument compiler_args);
UnmanagedVector build_move_package(UnmanagedVector *errmsg, ByteSliceView compiler_args_paylod);

UnmanagedVector clean_move_package(UnmanagedVector *errmsg,
CompilerArgument compiler_args,
ByteSliceView compiler_args_paylod,
bool clean_cache,
bool clean_byproduct,
bool force);

UnmanagedVector coverage_bytecode_move_package(UnmanagedVector *errmsg,
CompilerArgument compiler_args,
CompilerCoverageBytecodeOption coverage_opt);
ByteSliceView compiler_args_paylod,
ByteSliceView coverage_opt_payload);

UnmanagedVector coverage_source_move_package(UnmanagedVector *errmsg,
CompilerArgument compiler_args,
CompilerCoverageSourceOption coverage_opt);
ByteSliceView compiler_args_paylod,
ByteSliceView coverage_opt_payload);

UnmanagedVector coverage_summary_move_package(UnmanagedVector *errmsg,
CompilerArgument compiler_args,
CompilerCoverageSummaryOption coverage_opt);
ByteSliceView compiler_args_paylod,
ByteSliceView coverage_opt_payload);

UnmanagedVector create_new_move_package(UnmanagedVector *errmsg,
CompilerArgument compiler_args,
ByteSliceView compiler_args_paylod,
ByteSliceView name_view);

void destroy_unmanaged_vector(UnmanagedVector v);

UnmanagedVector docgen_move_package(UnmanagedVector *errmsg,
CompilerArgument compiler_args,
CompilerDocgenOption docgen_opt);
ByteSliceView compiler_args_paylod,
ByteSliceView docgen_opt_payload);

UnmanagedVector new_unmanaged_vector(bool nil, const uint8_t *ptr, size_t length);

UnmanagedVector prove_move_package(UnmanagedVector *errmsg,
CompilerArgument compiler_args,
CompilerProveOption prove_opt);

UnmanagedVector test_move_package(UnmanagedVector *errmsg,
CompilerArgument compiler_args,
CompilerTestOption test_opt);
ByteSliceView compiler_args_paylod,
ByteSliceView test_opt_payload);

#endif /* __LIBCOMPILER__ */
Loading

0 comments on commit 35a5621

Please sign in to comment.