Merge branch 'develop-misra-2012'. Close #472.

**Description**

The code generated by Copilot is not fully compliant with MISRA C. At
present, it complies with all but one rules, and all but two directives
of MISRA C 2012.

Due to the nature of this project and the environment where it is meant
to be used, we want to have compliance with all MISRA C rules, and if
possible with all MISRA C directives.

Any deviations should be properly justified and documented.

**Type**

- Feature: Compliance with MISRA C 2012.

**Additional context**

None.

**Requester**

- Patrick Quach (NASA)

**Method to check presence of bug**

Not applicable (not a bug).

**Expected result**

The code produced by Copilot complies with all rules in MISRA C 2012.
Any deviations from any rules or directives are documented and
justified.

**Solution implemented**

Modify `copilot-c99` to add keyword `static` to guards and generator
functions. That requires using language-c99-simple >= 0.3.

Modify `copilot-c99` backend to explicitly cast constants to `size_t` in
manipulations of the ring buffers.

Add a tool to the CI process that checks for compliance with the standard.

**Further notes**

The solution includes a new test in the CI setup that uses cppcheck to
check that a Copilot-generated C file complies with MISRA C. The test is
being executed by the CI setup (see:
https://app.travis-ci.com/github/Copilot-Language/copilot/jobs/615908458#L1976-L1978).

Furthermore, Parasoft has been used to manually check the same example
for compliance. Parasoft's tool reports a violation of one advisory
only: Directive 4.6. Complying with that recommendation would require
using specific types that indicate the size and signedness instead of
float and double. Although we could call those float32_t and float64_t,
there is in principle no guarantee that those will be the sizes in all
architectures, making such names potentially misleading. Since this is a
recommendation, we decide to accept non-compliance with this directive.

This change does not modify the README, contrary to the solution
originally proposed. This is intentional: there is no suitable place to
indicate information about compliance, or lack thereof, with MISRA C.
We decide to defer this change, and suggest extending the README to show
the features of Copilot more prominently. That will create the space to
talk about MISRA compliance and also list the advisory we do not
currently comply with.

Author: ivanperez-keera

.travis.yml

@@ -1,3 +1,6 @@
+# dist should be at least focal because we need cppcheck >= 1.88.
+dist: focal
+
 # NB: don't set `language: haskell` here
 
 # The following enables several GHC versions to be tested; often it's enough to
@@ -16,9 +19,9 @@ before_install:
   - travis_retry sudo apt-get update
   - travis_retry sudo apt-get install cabal-install-$CABALVER ghc-$GHCVER # see note about happy/alex
 
-  # We install z3 only for the tests, since it is not needed for normal
-  # compilation.
-  - if [ "${GHCVER}" == "8.10.4" ]; then travis_retry sudo apt-get install --yes z3; fi
+  # We install z3 and cppcheck only for the tests, since they are not needed
+  # for normal compilation.
+  - if [ "${GHCVER}" == "8.10.4" ]; then travis_retry sudo apt-get install --yes z3 cppcheck; fi
 
   - export PATH=/opt/ghc/$GHCVER/bin:/opt/cabal/$CABALVER/bin:$PATH
   - cabal --version
@@ -27,7 +30,10 @@ before_install:
   - git submodule update --remote
 
 script:
-  - travis_wait 30 cabal v2-install --lib copilot
+  # We explicitly install all libraries so that they are exposed and we can use
+  # them for tests (e.g., with runhaskell). There is no harm in doing this
+  # instead of installing just copilot.
+  - travis_wait 30 cabal v2-install --lib copilot copilot-core copilot-c99 copilot-language copilot-libraries copilot-theorem copilot-interpreter copilot-prettyprinter
 
   # Run tests only on GHC 8.10.4
   #
@@ -37,3 +43,8 @@ script:
   # conditional installation, and keep GHC version numbers in both places in
   # sync.
   - if [ "${GHCVER}" == "8.10.4" ]; then cabal v2-test -j1 copilot-core copilot-language copilot-interpreter copilot-c99 copilot-theorem copilot-libraries; fi
+
+  # Check that the code produced by Copilot complies with MISRA C 2012. We
+  # explicitly make cppcheck produce a non-zero exit code on non-compliance
+  # with the standard to make the CI build fail.
+  - if [ "${GHCVER}" == "8.10.4" ]; then runhaskell copilot/examples/Heater.hs; cppcheck --force --addon=misra.py --suppress=misra-c2012-14.4 --error-exitcode=2 heater.c; fi

copilot-c99/CHANGELOG

@@ -1,7 +1,8 @@
-2023-12-19
+2024-01-06
         * Change return type of main generated for tests. (#468)
         * Print constants in tests using portable suffixes. (#471).
         * Pass output arrays as arguments to trigger argument functions. (#431)
+        * Compliance with MISRA C 2023 / MISRA C 2012. (#472)
 
 2023-11-07
         * Version bump (3.17). (#466)

copilot-c99/copilot-c99.cabal

@@ -47,7 +47,7 @@ library
 
                           , copilot-core        >= 3.17  && < 3.18
                           , language-c99        >= 0.2.0 && < 0.3
-                          , language-c99-simple >= 0.2.2 && < 0.3
+                          , language-c99-simple >= 0.3   && < 0.4
 
   exposed-modules         : Copilot.Compile.C99
 

copilot-c99/src/Copilot/Compile/C99/CodeGen.hs

@@ -100,11 +100,18 @@ mkIndexDecln sId = C.VarDecln (Just C.Static) cTy name initVal
 
 -- | Define an accessor functions for the ring buffer associated with a stream.
 mkAccessDecln :: Id -> Type a -> [a] -> C.FunDef
-mkAccessDecln sId ty xs = C.FunDef cTy name params [] [C.Return (Just expr)]
+mkAccessDecln sId ty xs =
+    C.FunDef static cTy name params [] [C.Return (Just expr)]
   where
+    static     = Just C.Static
     cTy        = C.decay $ transType ty
     name       = streamAccessorName sId
-    buffLength = C.LitInt $ fromIntegral $ length xs
+
+    -- We cast the buffer length to a size_t to make sure that there are no
+    -- implicit conversions. This is a requirement for compliance with MISRA C
+    -- (Rule 10.4).
+    buffLength = C.Cast sizeT $ C.LitInt $ fromIntegral $ length xs
+    sizeT      = C.TypeName $ C.TypeSpec $ C.TypedefName "size_t"
     params     = [C.Param (C.TypeSpec $ C.TypedefName "size_t") "x"]
     index      = (C.Ident (indexName sId) C..+ C.Ident "x") C..% buffLength
     expr       = C.Index (C.Ident (streamName sId)) index
@@ -113,16 +120,19 @@ mkAccessDecln sId ty xs = C.FunDef cTy name params [] [C.Return (Just expr)]
 
 -- | Write a generator function for a stream.
 mkGenFun :: String -> Expr a -> Type a -> C.FunDef
-mkGenFun name expr ty = C.FunDef cTy name [] cVars [C.Return $ Just cExpr]
+mkGenFun name expr ty =
+    C.FunDef static cTy name [] cVars [C.Return $ Just cExpr]
   where
+    static         = Just C.Static
     cTy            = C.decay $ transType ty
     (cExpr, cVars) = runState (transExpr expr) mempty
 
 -- | Write a generator function for a stream that returns an array.
 mkGenFunArray :: String -> String -> Expr a -> Type a -> C.FunDef
 mkGenFunArray name nameArg expr ty@(Array _) =
-    C.FunDef funType name [ outputParam ] varDecls stmts
+    C.FunDef static funType name [ outputParam ] varDecls stmts
   where
+    static  = Just C.Static
     funType = C.TypeSpec C.Void
 
     -- The output value is an array
@@ -145,7 +155,7 @@ mkGenFunArray _name _nameArg _expr _ty =
 -- | Define the step function that updates all streams.
 mkStep :: CSettings -> [Stream] -> [Trigger] -> [External] -> C.FunDef
 mkStep cSettings streams triggers exts =
-    C.FunDef void (cSettingsStepFunctionName cSettings) [] declns stmts
+    C.FunDef Nothing void (cSettingsStepFunctionName cSettings) [] declns stmts
   where
     void = C.TypeSpec C.Void
 
@@ -194,8 +204,12 @@ mkStep cSettings streams triggers exts =
 
           indexUpdate = C.Expr $ indexVar C..= (incIndex C..% buffLength)
             where
-              buffLength = C.LitInt $ fromIntegral $ length buff
-              incIndex   = indexVar C..+ C.LitInt 1
+              -- We cast the buffer length and the literal one to a size_t to
+              -- make sure that there are no implicit conversions. This is a
+              -- requirement for compliance with MISRA C (Rule 10.4).
+              buffLength = C.Cast sizeT $ C.LitInt $ fromIntegral $ length buff
+              incIndex   = indexVar C..+ C.Cast sizeT (C.LitInt 1)
+              sizeT      = C.TypeName $ C.TypeSpec $ C.TypedefName "size_t"
 
           tmpVar   = streamName sId ++ "_tmp"
           buffVar  = C.Ident $ streamName sId

copilot/CHANGELOG

@@ -1,7 +1,8 @@
-2023-12-27
+2024-01-06
         * Enable tests for copilot-theorem in CI script. (#474)
         * Enable tests for copilot-libraries in CI script. (#475)
         * Replace uses of forall with forAll. (#470)
+        * Update CI job to check for MISRA compliance with cppcheck. (#472)
 
 2023-11-07
         * Version bump (3.17). (#466)