-
Notifications
You must be signed in to change notification settings - Fork 10
Simplify assert subroutine and support LFortran #56
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Closed
Closed
Changes from all commits
Commits
Show all changes
10 commits
Select commit
Hold shift + click to select a range
be7576d
feat: rm diagnostic_data arg & related types
rouson aed8470
build(lfortran): use stringify workaround in macro
rouson 7bf1441
Remove submodule
certik 37ed09d
Get rid of an interface
certik 535434d
XX: direcly use exit_status value
Pranavchiku f6e1671
fix(test): rm module in proc interf
rouson 52f5efe
Merge pull request #3 from rouson/fix-test
rouson f5ed2f9
doc(README): reorg, update commands, add lfortran
rouson c555ab8
fix(test): restrict output to image 1
rouson a01c636
build(fpm.toml): rm unnecessary project metadata
rouson File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -19,7 +19,6 @@ This assertion utility contains four public entities: | |
|
|
||
| The `assert` subroutine | ||
| * Error-terminates with a variable stop code when a caller-provided logical assertion fails, | ||
| * Includes user-supplied diagnostic data in the output if provided by the calling procedure, | ||
| * Is callable inside `pure` procedures, and | ||
| * Can be eliminated at compile-time, as controlled by the `ASSERTIONS` preprocessor define. | ||
|
|
||
|
|
@@ -42,10 +41,6 @@ If instead `fpm install` is used, then either the user must copy `include/assert | |
| the user must invoke `assert` directly (via `call assert(...)`). | ||
| In the latter approach when the assertions are disabled, the `assert` procedure will start and end with `if (.false.) then ... end if`, which might facilitate automatic removal of `assert` during the dead-code removal phase of optimizing compilers. | ||
|
|
||
| The `characterizable_t` type defines an `as_character()` deferred binding that produces `character` strings for use as diagnostic output from a user-defined derived type that extends `characterizable_t` and implements the deferred binding. | ||
|
|
||
| The `intrinsic_array_t` type that extends `characterizable_t` provides a convenient mechanism for producing diagnostic output from arrays of intrinsic type `complex`, `integer`, `logical`, or `real`. | ||
|
|
||
| Use Cases | ||
| --------- | ||
| Two common use cases include | ||
|
|
@@ -63,27 +58,49 @@ The requirements and assurances might be constraints of three kinds: | |
|
|
||
| The [example/README.md] file shows examples of writing constraints in notes on class diagrams using the formal syntax of the Object Constraint Language ([OCL]). | ||
|
|
||
| Downloading, Building, and Running Examples | ||
| ------------------------------------------- | ||
| Running the Examples | ||
| -------------------- | ||
| See the [./example](./example) subdirectory. | ||
|
|
||
| Building and Testing | ||
| -------------------- | ||
|
|
||
| - [Cray Compiler Environment (CCE) `ftn`](#cray-compiler-environment-cce-ftn) | ||
| - [GNU Compiler Collection (GCC) `gfortran`](#gnu-compiler-collection-gcc-gfortran)) | ||
| - [Intel `ifx`](#intel-ifx)) | ||
| - [LFortran `lfortran`](#lfortran-lfortran) | ||
| - [LLVM `flang-new`](#llvm-flang-new) | ||
| - [Numerical Algorithms Group (NAG) `nagfor`](#numerical-algorithms-group-nag-nagfor) | ||
|
|
||
| ### Downloading Assert | ||
| ### Cray Compiler Environment (CCE) `ftn` | ||
| Because `fpm` uses the compiler name to determine the compiler identity and because | ||
| CCE provides one compiler wrapper, `ftn`, for invoking all compilers, you will | ||
| need to invoke `ftn` in a shell script named to identify CCE compiler. For example, | ||
| place a script named `crayftn.sh` in your path with the following contents and with | ||
| executable privileges set appropriately: | ||
| ``` | ||
| git clone [email protected]:berkeleylab/assert | ||
| cd assert | ||
| #!/bin/bash | ||
|
|
||
| ftn $@ | ||
| ``` | ||
| Then build and test Assert with the command | ||
| ``` | ||
| fpm test --compiler crayftn.sh --profile release | ||
| ``` | ||
|
|
||
| ### GNU Compiler Collection (GCC) `gfortran` | ||
|
|
||
| ### Building and testing with `gfortran` | ||
| #### Single-image (serial) execution | ||
| The command below builds Assert and runs the full test suite in a single image. | ||
| For `gfortran` 14 or later, use | ||
| With `gfortran` 14 or later, use | ||
| ``` | ||
| fpm test --profile release | ||
| ``` | ||
| For `gfortran` 13 or earlier, use | ||
| With `gfortran` 13 or earlier, use | ||
| ``` | ||
| fpm test --profile release --flag "-ffree-line-length-0" | ||
| ``` | ||
| The above commands build the Assert library (with the default of assertion enforcement disabled) and runs the test suite. | ||
|
|
||
| #### Multi-image (parallel) execution | ||
| With `gfortran` 14 or later versions and OpenCoarrays installed, use | ||
| ``` | ||
|
|
@@ -93,60 +110,65 @@ With `gfortran` 13 or earlier versions and OpenCoarrays installed, | |
| ``` | ||
| fpm test --compiler caf --profile release --runner "cafrun -n 2" --flag "-ffree-line-length-0" | ||
| ``` | ||
| To build and test with the Numerical Algorithms Group (NAG) Fortran compiler version | ||
| 7.1 or later, use | ||
| ``` | ||
| fpm test --compiler=nagfor --profile release --flag "-coarray=cosmp -fpp -f2018" | ||
| ``` | ||
|
|
||
| ### Building and testing with the Intel `ifx` compiler | ||
| ### Intel `ifx` | ||
|
|
||
| #### Single-image (serial) execution | ||
| ``` | ||
| fpm test --compiler ifx --profile release | ||
| ``` | ||
|
|
||
| #### Multi-image (parallel) execution | ||
| With Intel Fortran and Intel MPI installed, | ||
| ``` | ||
| fpm test --compiler ifx --profile release --flag "-coarray -DASSERT_MULTI_IMAGE" | ||
| ``` | ||
|
|
||
| ### Building and testing with the LLVM `flang-new` compiler | ||
| #### LLVM version 19 | ||
| ### LLVM `flang-new` | ||
|
|
||
| #### Single-image (serial) execution | ||
| With `flang-new` version 19, use | ||
| ``` | ||
| fpm test --compiler flang-new --flag "-mmlir -allow-assumed-rank -O3" | ||
| ``` | ||
| #### LLVM version 20 or later | ||
| With `flang-new` version 20 or later, use | ||
| ``` | ||
| fpm test --compiler flang-new --flag "-O3" | ||
| ``` | ||
|
|
||
| ### Building and testing with the Numerical Algorithms Group (NAG) compiler | ||
| #### Multi-image (parallel) execution | ||
| With `flang-new` version 21 built from the SiPearl llvm-project fork's | ||
| [prif branch](https://github.com/SiPearl/llvm-project/tree/prif), use | ||
| ``` | ||
| fpm test --compiler nagfor --profile release --flag "-fpp -coarray=cosmp" | ||
| fpm test --compiler -caffeine -L<path-to-libcaffeine> -l<gasnet-conduit> -L<path-to-libgasnet> | ||
| ``` | ||
| where, for example, `<gasnet-conduit>` might be `gasnet-smp-seq` for | ||
| shared-memory execution. | ||
|
|
||
| ### Building and testing with the Cray Compiler Environment (CCE) | ||
| Because `fpm` uses the compiler name to determine the compiler identity and because | ||
| CCE provides one compiler wrapper, `ftn`, for invoking all compilers, you will | ||
| need to invoke `ftn` in a shell script named to identify CCE compiler. For example, | ||
| place a script named `crayftn.sh` in your path with the following contents and with | ||
| executable privileges set appropriately: | ||
| ``` | ||
| #!/bin/bash | ||
| ### LFortran `lfortran` | ||
|
|
||
| ftn $@ | ||
| ``` | ||
| Then build and test Assert with the command | ||
| #### Single-image (serial) execution | ||
| ``` | ||
| fpm test --compiler crayftn.sh --profile release | ||
| fpm test --compiler lfortran --profile release --flag --cpp | ||
| ``` | ||
|
|
||
| ### Numerical Algorithms Group (NAG) `nagfor` | ||
|
|
||
| ### Building and testing with other compilers | ||
| To use Assert with other compilers, please submit an issue or pull request. | ||
| #### Single-image (serial) execution | ||
| With `nagfor` version 7.1 or later, use | ||
| ``` | ||
| fpm test --compiler nagfor --profile release --flag -fpp | ||
| ``` | ||
|
|
||
| ### Running the examples | ||
| See the [./example](./example) subdirectory. | ||
| #### Multi-image execution | ||
| With `nagfor` 7.1, use | ||
| ``` | ||
| fpm test --compiler nagfor --profile release --flag "-fpp -coarray=cosmp -f2018" | ||
| ``` | ||
| With `nagfor` 7.2 or later, use | ||
| ``` | ||
| fpm test --compiler nagfor --profile release --flag -fpp | ||
| ``` | ||
|
|
||
| Documentation | ||
| ------------- | ||
|
|
@@ -208,19 +230,19 @@ character for line-breaks in a macro invocation: | |
|
|
||
| ```fortran | ||
| ! OK for flang-new and gfortran | ||
| call_assert_diagnose( computed_checksum == expected_checksum, \ | ||
| "Checksum mismatch failure!", \ | ||
| expected_checksum ) | ||
| call_assert_describe( computed_checksum == expected_checksum, \ | ||
| "Checksum mismatch failure!" \ | ||
| ) | ||
| ``` | ||
|
|
||
| Whereas Cray Fortran wants `&` line continuation characters, even inside | ||
| a macro invocation: | ||
|
|
||
| ```fortran | ||
| ! OK for Cray Fortran | ||
| call_assert_diagnose( computed_checksum == expected_checksum, & | ||
| "Checksum mismatch failure!", & | ||
| expected_checksum ) | ||
| call_assert_describe( computed_checksum == expected_checksum, & | ||
| "Checksum mismatch failure!" & | ||
| ) | ||
| ``` | ||
|
|
||
| There appears to be no syntax acceptable to all compilers, so when writing | ||
|
|
@@ -237,29 +259,29 @@ after macro expansion (on gfortran and flang-new): | |
|
|
||
| ```fortran | ||
| ! INCORRECT: cannot use Fortran comments inside macro invocation | ||
| call_assert_diagnose( computed_checksum == expected_checksum, ! ensured since version 3.14 | ||
| "Checksum mismatch failure!", ! TODO: write a better message here | ||
| computed_checksum ) | ||
| call_assert_describe( computed_checksum == expected_checksum, ! ensured since version 3.14 | ||
| "Checksum mismatch failure!" ! TODO: write a better message here | ||
| ) | ||
| ``` | ||
|
|
||
| Depending on your compiler it *might* be possible to use a C-style block | ||
| comment (because they are often removed by the preprocessor), for example with | ||
| gfortran one can instead write the following: | ||
|
|
||
| ```fortran | ||
| call_assert_diagnose( computed_checksum == expected_checksum, /* ensured since version 3.14 */ \ | ||
| "Checksum mismatch failure!", /* TODO: write a better message here */ \ | ||
| computed_checksum ) | ||
| call_assert_describe( computed_checksum == expected_checksum, /* ensured since version 3.14 */ \ | ||
| "Checksum mismatch failure!" /* TODO: write a better message here */ \ | ||
| ) | ||
| ``` | ||
|
|
||
| However that capability might not be portable to other Fortran compilers. | ||
| When in doubt, one can always move the comment outside the macro invocation: | ||
|
|
||
| ```fortran | ||
| ! assert a property ensured since version 3.14 | ||
| call_assert_diagnose( computed_checksum == expected_checksum, \ | ||
| "Checksum mismatch failure!", \ | ||
| computed_checksum ) ! TODO: write a better message above | ||
| call_assert_describe( computed_checksum == expected_checksum, \ | ||
| "Checksum mismatch failure!" \ | ||
| ) ! TODO: write a better message above | ||
| ``` | ||
|
|
||
| Legal Information | ||
|
|
||
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -10,82 +10,34 @@ The [simple_assertions.f90] example demonstrates a precondition and a | |
| postcondition, each with an assertion that checks the truth of a logical | ||
| expression based on scalar, real values. | ||
|
|
||
| Derived type diagnostic data | ||
| ---------------------------- | ||
|
|
||
| See [derived_type_diagnostic.f90]. For reasons related to runtime performance, | ||
| it is desirable to ensure that any computation required to extract diagnostic | ||
| data from an object only take place if the assertion fails. This is one of the | ||
| main motivations for allowing objects to be passed to the `diagnostic_data` | ||
| argument of `assert`. The generic programming facilities planned for | ||
| "Fortran 202y" (two standards after Fortran 2018) will ultimately provide the | ||
| best way to facilitate the extraction of diagnostic data from objects by | ||
| empowering developers to express requirements on types such as that the types | ||
| must support a specific procedure binding that can be used to extract output | ||
| in character form, the form that `assert` uses for its error stop code. For | ||
| now, we impose such a requirement through an `as_character` deferred binding | ||
| on the provided `characterizable_t` abstract type. | ||
|
|
||
| Because it might prove problematic to require that a user type to extend the | ||
| `characterizable_t` abstract type, the [derived_type_diagnostic.f90] example | ||
| shows a workaround based on the class hierarchy described in the figure below. | ||
| The figure shows a Unified Modeling Language ([UML]) class diagram with the | ||
| `characterizable_t` abstract class, an example user's `stuff_t` class, and a | ||
| `characterizable_stuff_t` class. The pattern expressed in the workaround | ||
| aggregates the example user type, `stuff_t`, as a component inside the | ||
| encapsulating `characterizable_stuff_t` type defined to extend `characterizable_t` | ||
| for purposes of implementing `characterizable_t` parent type's deferred | ||
| `as_character()` binding. | ||
|
|
||
| The figure below also shows two constraints written in UML's Object Constraint | ||
| Language ([OCL]). The constraints describe the precondition and postcondition | ||
| checked in [derived_type_diagnostic.f90] and the context for those constraints. | ||
|
|
||
| The UML diagram below was generated in the [Atom] editor [PlantUML] package | ||
| from the PlantUML script in this repository's [doc] folder. | ||
|
|
||
|  | ||
|
|
||
| Running the examples | ||
| -------------------- | ||
|
|
||
| ### Single-image execution | ||
| ``` | ||
| fpm run --example simple_assertions | ||
| fpm run --example derived_type_diagnostic | ||
| ``` | ||
| where `fpm run` automatically invokes `fpm build` if necessary, .e.g., if the package's source code | ||
| has changed since the most recent build. If `assert` is working correctly, the first `fpm run` above | ||
| will error-terminate with the character stop code | ||
| ``` | ||
| Assertion "reciprocal: abs(error) < tolerance" failed on image 1 with diagnostic data "-1.00000000" | ||
| has changed since the most recent build. If `assert` is working correctly, the `fpm run` above | ||
| will error-terminate with the character stop code similar to the following | ||
| ``` | ||
| and the second `fpm run` above will error-terminate with the character stop code | ||
| ``` | ||
| Assertion "stuff_t%z(): self%defined()" failed on image 1 with diagnostic data "(none provided)" | ||
| Assertion failure on image 1: reciprocal: abs(error) < tolerance | ||
| ``` | ||
|
|
||
| ### Multi-image execution with `gfortran` and OpenCoarrays | ||
| ``` | ||
| git clone [email protected]/sourceryinstitute/assert | ||
| cd assert | ||
| fpm run --compiler caf --runner "cafrun -n 2" --example simple_assertions | ||
| fpm run --compiler caf --runner "cafrun -n 2" --example derived_type_diagnostic | ||
| ``` | ||
| Replace either instance of `2` above with the desired number of images to run for parallel execution. | ||
| If `assert` is working correctly, both of the latter `fpm run` commands will error-terminate with one | ||
| or more images providing stop codes analogous to those quoted in the [Single-image execution] section. | ||
|
|
||
| ## Derived-type diagnostic data output | ||
| To demonstrate the derived-type diagnostic data output capability, try replacing the | ||
| `i%defined()` assertion in the [derived_type_diagnostic.f90](./derived_type_diagnostic.f90) | ||
| with `.false.`. | ||
|
|
||
| [Hyperlinks]:# | ||
| [OpenCoarrays]: https://github.com/sourceryinstitute/opencoarrays | ||
| [Enforcing programming contracts]: #enforcing-programming-contracts | ||
| [Single-image execution]: #single-image-execution | ||
| [derived_type_diagnostic.f90]: ./derived_type_diagnostic.f90 | ||
| [simple_assertions.f90]: ./simple_assertions.f90 | ||
| [UML]: https://en.wikipedia.org/wiki/Unified_Modeling_Language | ||
| [OCL]: https://en.wikipedia.org/wiki/Object_Constraint_Language | ||
|
|
||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.