[Blocked on #1435] Support proptest arbitrary generation for bool and tuple#1467

Closed

YoshikiTakashima wants to merge 95 commits intomodel-checking:mainfrom YoshikiTakashima:yoshi-arbitrary-proptest

+3,846-12

Commits on Jul 1, 2022

Added proptest test cases.
Yoshi Takashima
committed

Commits on Jul 5, 2022

Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
Added prototype translator.
Yoshi Takashima
committed
Added missing recurisve case. Separated to helper.
Yoshi Takashima
committed

Commits on Jul 6, 2022

Removed panic put in for debugging.
Yoshi Takashima
committed
Changed name of translator
Yoshi Takashima
committed
Refactored test case for proptest integration.
Yoshi Takashima
committed
Fixed typo in variable name.
Yoshi Takashima
committed
Added multi-argument and combo tests for proptest.
Yoshi Takashima
committed
purged redundant spaces.
Yoshi Takashima
committed

Commits on Jul 8, 2022

Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
Rustfmt on library/kani_macros/src/lib.rs
Yoshi Takashima
committed
Initial prototype to hijack proptest.
Yoshi Takashima
committed

Commits on Jul 9, 2022

Added todo not for hard-coded path.
Yoshi Takashima
committed
Partially working cargo kani hack. Recovery is not running though.
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
fixed empty var check
Yoshi Takashima
committed

Commits on Jul 11, 2022

Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed

Commits on Jul 14, 2022

Added expanded macro printing to kani-compiler. Remove later.
Yoshi Takashima
committed
Added flags to mark rules in expanded form.
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed

Commits on Jul 15, 2022

Make the var names unique to detect rule firing.
Yoshi Takashima
committed
Prototyped new BODY2 rule. Need to push the API side for testing.
Yoshi Takashima
committed

Commits on Jul 18, 2022

Moved macros out to proper sugar.rs file.
Yoshi Takashima
committed
Supported Minimum Strategy.
Yoshi Takashima
committed

Commits on Jul 19, 2022

Got new proptest to type check. TODO: cleanup
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
Removed expansion. Somehow fixes the "finding proof" issue.
Yoshi Takashima
committed
Fixed missing tuple implementation.
Yoshi Takashima
committed

Commits on Jul 20, 2022

Externalized arbitrary value generation. (Commit before macro try)
Yoshi Takashima
committed
Added hack translator for from strategy to kani.
Yoshi Takashima
committed
Implemented Invariant for tuples.
Yoshi Takashima
committed
Just use kani::any by itself for now.
Yoshi Takashima
committed

Commits on Jul 22, 2022

Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed

Commits on Jul 26, 2022

Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed

Commits on Jul 28, 2022

Reverted proptest macro.
Yoshi Takashima
committed

Commits on Jul 29, 2022

Temporary commit: hard-coded kani output path.
Yoshi Takashima
committed
Implemented custom compile script to get symtabs for proptest.
Yoshi Takashima
committed
Added automatic local target detection.
Yoshi Takashima
committed

Commits on Jul 30, 2022

Ignored expected error message.
Yoshi Takashima
committed
implemented search of kani extern path for symtabs.
Yoshi Takashima
committed
Added proptest refresh to kani and cargo kani scripts..
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
Removed redundant part after PR1420 merged.
Yoshi Takashima
committed

Commits on Aug 2, 2022

Added back floating point support.
Yoshi Takashima
committed
Cleaned up warnings and clippy complaints.
Yoshi Takashima
committed
Added support for booleans.
Yoshi Takashima
committed
Removed proptest translator not needed.
Yoshi Takashima
committed
Fixed infinite recursion.
Yoshi Takashima
committed
Fixed recompiling criteria.
Yoshi Takashima
committed
Added prelude module.
Yoshi Takashima
committed
Fixed license for PR.
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
Applied cargo fmt.
Yoshi Takashima
committed
Added license to proptest Cargo.toml
Yoshi Takashima
committed
Fixed clippy warning
Yoshi Takashima
committed
Added license to proptest module.
Yoshi Takashima
committed

Commits on Aug 3, 2022

Merge branch 'main' of github.com:model-checking/kani into proptest-dev
Yoshi Takashima
committed
Purged non-basic proptest files.
Yoshi Takashima
committed
Adjust license tag.
Yoshi Takashima
committed
Purged unused code.
Yoshi Takashima
committed
Added todo message.
Yoshi Takashima
committed
Reverted invariant.rs.
Yoshi Takashima
committed
Added basic test case.
Yoshi Takashima
committed
Added proptest syntax sugar macros.
Yoshi Takashima
committed
Reverted Cargo.toml of proptest testcase. The old one works.
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
Yoshi Takashima
committed
Rustfmt.
Yoshi Takashima
committed
Supressed warnings caused by kani-specific panic! macro.
Yoshi Takashima
committed

Commits on Aug 4, 2022

Reverted invariant.
Yoshi Takashima
committed
Temporarily removed refresh script.
Yoshi Takashima
committed
Cleaner path to root workspace.
Yoshi Takashima
committed
Made extended linking paths dependent on env being set for proptest.
Yoshi Takashima
committed
Fixed proptest refresh taht was occuring too frequently.
Yoshi Takashima
committed
Remove proptest import. They break since only strategies are loaded.
Yoshi Takashima
committed
Purged tests not needed at this sub-PR.
Yoshi Takashima
committed
Cleaned up paths.
Yoshi Takashima
committed
Purged debug comment on macro expansion.
Yoshi Takashima
committed
Fixed license.
Yoshi Takashima
committed
Fixed license for new test case.
Yoshi Takashima
committed
More temporary disabling of proptest
YoshikiTakashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-proptest-primitive
YoshikiTakashima
committed
Reverted files for arbitrary and boolean. TODO: cleanup
Yoshi Takashima
committed

Commits on Aug 5, 2022

Fixed license
Yoshi Takashima
committed
Added note
Yoshi Takashima
committed
Exported the reverted code back.
Yoshi Takashima
committed
Added proptest for arbitrary and tuples.
Yoshi Takashima
committed
Implemented tuple arbitrary pattern.
Yoshi Takashima
committed
Adjusted test case to test more complex any();
Yoshi Takashima
committed
Rustfmt.
Yoshi Takashima
committed
Merge branch 'main' of github.com:model-checking/kani into yoshi-arbitrary-proptest
Yoshi Takashima
committed
Merge branch 'main' into yoshi-arbitrary-proptest
Yoshiki Takashima
authored

Commits on Aug 7, 2022

Merge branch 'main' into yoshi-arbitrary-proptest
Yoshiki Takashima
authored