Skip to content
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

(Closes #2394) add support char logical in psydata #2509

Merged
merged 24 commits into from
Jan 20, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
8b8d9b6
#2394 Support logical and character for nan and readonly.
hiker Nov 9, 2023
1c54119
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker Feb 22, 2024
b61f169
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker May 14, 2024
76f2a28
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker Dec 8, 2024
92388d6
#2394 Fixed character handling.
hiker Dec 9, 2024
a2f86f7
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker Dec 10, 2024
1d13b02
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker Dec 18, 2024
ecb0571
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker Jan 6, 2025
8debe33
#2394 Removed the bits field from ALL_TYPES.
hiker Jan 7, 2025
69b9938
#2394 Fixed bug (int arrays not checked for value range).
hiker Jan 7, 2025
ae62916
#2394 Added generic read-only verification library, and added example…
hiker Jan 9, 2025
42259f5
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker Jan 9, 2025
b3f9904
#2394 Fixed coding style.
hiker Jan 9, 2025
fa19a9b
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker Jan 9, 2025
96d917d
#2394 fix whitespace errors in xdsl makefile
arporter Jan 10, 2025
9533be1
#2394 Fix typo.
hiker Jan 14, 2025
3358e77
#2394 Updated documentation and comments.
hiker Jan 14, 2025
e970ccf
#2394 Fix makefile to avoid running psyclone unnecessary.
hiker Jan 14, 2025
2f1497a
#2394 Added more comments.
hiker Jan 14, 2025
b0003bf
#2394 Updated comments, fixed link.
hiker Jan 14, 2025
761099c
#2394 Fixed incorrect links in READMEs.
hiker Jan 14, 2025
3c80cb8
Merge branch '2394_support_char_logical_in_psydata' of github.com:stf…
hiker Jan 14, 2025
d0562cf
Merge remote-tracking branch 'origin/master' into 2394_support_char_l…
hiker Jan 14, 2025
96f7618
#2394 update UG and changelog
arporter Jan 20, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions changelog
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,9 @@
11) PR #2814 for #2704. Adds backward accesses capabilities to the
DefinitionUseChain tool.

12) PR #2509 for #2394. Adds support for logical and character types
to the PSyData tooling.

release 3.0.0 6th of December 2024

1) PR #2477 for #2463. Add support for Fortran Namelist statements.
Expand Down
5 changes: 3 additions & 2 deletions doc/user_guide/libraries.rst
Original file line number Diff line number Diff line change
Expand Up @@ -99,8 +99,9 @@ Read-only libraries check that a field declared as read-only is not
modified during a kernel call. More information can be found in the
:ref:`Read-Only Verification <psydata_read_verification>` section.

The libraries for :ref:`LFRic <lfric-api>` and
:ref:`GOcean <gocean-api>` APIs are included with PSyclone in
The libraries for :ref:`LFRic <lfric-api>`,
:ref:`GOcean <gocean-api>` APIs and generic Fortran code
are included with PSyclone in
the ``lib/read_only`` `directory
<https://github.com/stfc/PSyclone/tree/master/lib/read_only>`__.
For detailed instructions on how to build and use these libraries
Expand Down
26 changes: 23 additions & 3 deletions doc/user_guide/psy_data.rst
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,7 @@ be printed at runtime, e.g.::
The transformation that adds read-only-verification to an application
can be applied for both the :ref:`LFRic <lfric-api>` and
:ref:`GOcean API <gocean-api>` - no API-specific transformations are required.
It can also be used to verify existing Fortran code.
Below is an example that searches for each loop in a PSyKAl invoke code (which
will always surround kernel calls) and applies the transformation to each one.
This code has been successfully used as a global transformation with the LFRic
Expand All @@ -136,10 +137,10 @@ Gravity Wave application (the executable is named ``gravity_wave``)
read_only_verify.apply(loop)

Besides the transformation, a library is required to do the actual
verification at runtime. There are two implementations of the
verification at runtime. There are three implementations of the
read-only-verification library included in PSyclone: one for LFRic,
and one for GOcean.
Both libraries support the environment variable ``PSYDATA_VERBOSE``.
one for GOcean, and one for generic Fortran code.
These libraries support the environment variable ``PSYDATA_VERBOSE``.
This can be used to control how much output is generated
by the read-only-verification library at runtime. If the
variable is not specified or has the value '0', warnings will only
Expand Down Expand Up @@ -230,6 +231,25 @@ An executable example for using the GOcean read-only-verification
library is included in ``examples/gocean/eg5/readonly``, see
:ref:`gocean_example_readonly`.


Read-Only-Verification Library for Generic Fortran
++++++++++++++++++++++++++++++++++++++++++++++++++

This library is contained in the ``lib/read_only/generic`` directory and
it must be compiled before linking any existing Fortran code that uses
read-only verification.

Compilation of the library is done by invoking ``make`` and setting
the required variables:

.. code-block:: shell

make F90=ifort F90FLAGS="--some-flag"

This will create a library called ``lib_read_only.a``.
An executable example for using the generic read-only-verification
library is included in ``examples/nemo/eg6/``.

.. _psydata_value_range_check:

Value Range Check
Expand Down
8 changes: 8 additions & 0 deletions doc/user_guide/tutorials_and_examples.rst
Original file line number Diff line number Diff line change
Expand Up @@ -783,6 +783,14 @@ compilation instructions are in the ``README.md`` file, including how
to switch from using the stand-alone extraction library to the NetCDF-based
one (see :ref:`extraction_libraries` for details).

Example 6: Read-only Verification
arporter marked this conversation as resolved.
Show resolved Hide resolved
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

This example shows the use of read-only verification with PSyclone for
generic Fortran code. It instruments each kernel in a small Fortran
program with the PSyData-based read-only verification code. Detailed
compilation instructions are in the ``README.md`` file.


Scripts
^^^^^^^
Expand Down
6 changes: 6 additions & 0 deletions examples/nemo/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -140,3 +140,9 @@ benchmark.

Extraction of kernel data. Using the tra_adv benchmark, this example
shows the extraction of kernel input- and output-data.

## Example 6

A simple stand-alone example that shows verification that read-only data
is not modified, e.g. by out-of-bounds accesses to other variables.
This uses the PSyData interface to instrument generic Fortran code.
83 changes: 83 additions & 0 deletions examples/nemo/eg6/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,83 @@
# -----------------------------------------------------------------------------
# BSD 3-Clause License
#
# Copyright (c) 2023-2025, Science and Technology Facilities Council.
# All rights reserved.
#
# Redistribution and use in source and binary forms, with or without
# modification, are permitted provided that the following conditions are met:
#
# * Redistributions of source code must retain the above copyright notice, this
# list of conditions and the following disclaimer.
#
# * Redistributions in binary form must reproduce the above copyright notice,
# this list of conditions and the following disclaimer in the documentation
# and/or other materials provided with the distribution.
#
# * Neither the name of the copyright holder nor the names of its
# contributors may be used to endorse or promote products derived from
# this software without specific prior written permission.
#
# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
# FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
# COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
# INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
# BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
# LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
# CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
# LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
# ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
# POSSIBILITY OF SUCH DAMAGE.
# ------------------------------------------------------------------------------
# Author: A. R. Porter, STFC Daresbury Lab
# Modified J. Henrichs, Bureau of Meteorology

# This example uses PSyclone (which must be installed) to generate Fortran for
# the tracer-advection benchmark. The script provided here instruments code to
# check that read-only variables are not modified.

# The compiler to use may be specified via the F90 environment variable,
# it defaults to:
# export F90=gfortran
# export F90FLAGS="-g -O0"

include ../../common.mk

TYPE ?= standalone

GENERATED_FILES += psy.f90 psy.o dummy

PSYROOT=../../..
READ_ONLY_CHECK_DIR ?= $(PSYROOT)/lib/read_only/generic

F90FLAGS += -I$(READ_ONLY_CHECK_DIR)
LIB_NAME = lib_read_only.a

.PHONY: allclean

compile: dummy

run: compile
./dummy

dummy: psy.o $(READ_ONLY_CHECK_DIR)/$(LIB_NAME)
$(F90) psy.o -o dummy $(READ_ONLY_CHECK_DIR)/$(LIB_NAME) $(LDFLAGS)

transform: kernels

# Need `-l all` to ensure line-lengths in generated code are less than the
# standard-mandated 132 chars.
kernels: read_only_check.py
$(PSYCLONE) -l all -s ./read_only_check.py -o psy.f90 dummy.f90

$(READ_ONLY_CHECK_DIR)/$(LIB_NAME):
make -C $(READ_ONLY_CHECK_DIR)

# Compilation uses the 'kernels' transformed code
psy.f90: dummy.f90 read_only_check.py
psy.o: $(READ_ONLY_CHECK_DIR)/$(LIB_NAME)

%.o: %.f90
$(F90) $(F90FLAGS) -c $<
100 changes: 100 additions & 0 deletions examples/nemo/eg6/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,100 @@
# PSyclone NEMO Example 6 - Read-only Verification
arporter marked this conversation as resolved.
Show resolved Hide resolved

**Author:** J. Henrichs, Bureau of Meteorology

This example demonstrates the use of PSyclone to add code that checks
if variables that are only read are actually modified (e.g. because
of memory overwrite).

Once you have installed PSyclone, you can transform the file using:

```sh
psyclone -s ./read_only_check.py dummy.f90
```

Executing this will output the transformed Fortran code with the
read-only-verification code added.

The generic read-only verification library in
``../../../lib/read_only/generic`` is used, and will also be
automatically compiled if required.

## Compiling and Execution

To create and compile the example, type ``make compile``.
This example can be compiled and executed. It will report nothing,
since no read-only variable is overwritten. But you can verify that
the variables are checked by setting ``PSYDATA_VERBOSE=2``:

```sh
$ PSYDATA_VERBOSE=2 ./dummy
PSyData: PreStart dummy r0
PSyData: DeclareScalarChar: dummy r0: char_var
PSyData: DeclareScalarLogical: dummy r0: logical_var
PSyData: DeclareScalarChar: dummy r0: char_var
PSyData: DeclareScalarLogical: dummy r0: logical_var
PSyData: checked variable char_var
PSyData: checked variable logical_var
PSyData: PostEnd dummy r0
3.00000000 F
```

If you copy the lines 68 and 69 from ``dummy.f90`` into ``psy.f90``,
the code will modify ``logical_var`` (by using out-of-bound array accesses.
Or you could just manually set ``logical_var = .true.``). If you then
compile again (using `make compile`, otherwise the original file would
get processed again, overwriting your changes), an error will be produced.

```sh
$ ./dummy
------------- PSyData -------------------------
Logical(kind=4) variable logical_var has been modified in dummy : r0
Original value: F
New value: T
------------- PSyData -------------------------
3.00000000 T
```

Note that adding the assignment to ``logical_var`` as above to the original
``dummy.f90`` file would mean that ``logical_var`` is not a read-only variable
anymore, so no test and therefore no error will be produced for this variable.
The code commented out can also not be processed by PSyclone (missing support
for ``loc`` and ``sizeof``, which are non-standard Fortran extensions).

## Licence

-----------------------------------------------------------------------------

BSD 3-Clause License

Copyright (c) 2025, Science and Technology Facilities Council.
All rights reserved.

Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:

* Redistributions of source code must retain the above copyright notice, this
list of conditions and the following disclaimer.

* Redistributions in binary form must reproduce the above copyright notice,
this list of conditions and the following disclaimer in the documentation
and/or other materials provided with the distribution.

* Neither the name of the copyright holder nor the names of its
contributors may be used to endorse or promote products derived from
this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
POSSIBILITY OF SUCH DAMAGE.

-----------------------------------------------------------------------------
74 changes: 74 additions & 0 deletions examples/nemo/eg6/dummy.f90
Original file line number Diff line number Diff line change
@@ -0,0 +1,74 @@
! -----------------------------------------------------------------------------
! BSD 3-Clause License
!
! Copyright (c) 2025, Science and Technology Facilities Council.
! All rights reserved.
!
! Redistribution and use in source and binary forms, with or without
! modification, are permitted provided that the following conditions are met:
!
! * Redistributions of source code must retain the above copyright notice, this
! list of conditions and the following disclaimer.
!
! * Redistributions in binary form must reproduce the above copyright notice,
! this list of conditions and the following disclaimer in the documentation
! and/or other materials provided with the distribution.
!
! * Neither the name of the copyright holder nor the names of its
! contributors may be used to endorse or promote products derived from
! this software without specific prior written permission.
!
! THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
! AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
! IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
! DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
! FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
! DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
! SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
! CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
! OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
! OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
! -----------------------------------------------------------------------------
! Author: J. Henrichs, Bureau of Meteorology

! This is a very simple program that is used to show how PSyclone can
! detect if a read-only variable is modified (typically because of a
! memory overwrite elsewhere). In order to actually trigger the warning,
! you need to modify the code after processing it with PSyclone, see
! details in lines 68-69.

program dummy
arporter marked this conversation as resolved.
Show resolved Hide resolved
real, dimension(10, 10) :: umask
character(len=10) :: char_var
integer :: ji, jj
logical :: logical_var
integer(kind=8) :: offset
integer, intrinsic :: loc, sizeof

logical_var = .false.
char_var = "test"

do jj = 1, 10
do ji = 1, 10
if (char_var .eq. "abc" .and. logical_var) then
umask(ji,jj) = 1
else
umask(ji,jj) = 3
endif
end do

! VERY NAUGHTY CODE AHEAD - there be dragon!!
! We modify the values of some read-only fields by using offsets
! in a written array. This will abort if the code is compiled
! with array bound check of course.
! TODO: Unfortunately, PSyclone does not support loc or sizeof (which
! are non-standard extensions), so the code below does not work. But
! you can create the psy-layer, and then copy the following lines into
! psy.f90, and recompile the program (use `make compile`). This will then
! issue a warning about `logical_var` being overwritten.
! offset = ( loc(logical_var) - loc(umask(1,1)) ) / sizeof(logical_var)
! umask(1+offset, 1) = 123.0
end do

print *,umask(1,1), logical_var
end program dummy
Loading
Loading