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

Add 'unstructured' template that tests random instruction bit patterns #64

Merged
merged 1 commit into from
Jan 15, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
1 change: 1 addition & 0 deletions QCVEngine.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -52,6 +52,7 @@ executable QCVEngine
QuickCheckVEngine.Templates.GenCHERI,
QuickCheckVEngine.Templates.GenAll,
QuickCheckVEngine.Templates.GenTransExec,
QuickCheckVEngine.Templates.GenUnstructured,
QuickCheckVEngine.Templates.RandomTest
other-extensions: FlexibleInstances, MultiParamTypeClasses,
FunctionalDependencies, OverloadedStrings,
Expand Down
1 change: 1 addition & 0 deletions src/QuickCheckVEngine/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -271,6 +271,7 @@
, ("caprvcrandom", "Xcheri RVC Extension Random Template", andPs [has_cheri, has_c], randomCHERIRVCTest)
, ("all", "All Verification", const True, genAll)
, ("random", "Random Template", const True, randomTest)
, ("unstructured", "Unstructured random instruction bit Template", const True, T.repeatTillEnd gen_unstructured)

Check failure on line 274 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Build the QuickCheck Verification Engine

Variable not in scope: gen_unstructured :: T.Template
]
where andPs = foldl (\k p x -> p x && k x) (const True)

Expand All @@ -282,7 +283,7 @@
(flags, _) <- commandOpts rawArgs
let verbosity = optVerbosity flags
when (verbosity > 1) $ print flags
let checkRegex incReg excReg str = (str =~ (fromMaybe ".*" incReg)) && (not $ str =~ fromMaybe "a^" excReg)

Check warning on line 286 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Move brackets to avoid $ ▫︎ Found: "(str =~ (fromMaybe \".*\" incReg))\n && (not $ str =~ fromMaybe \"a^\" excReg)" ▫︎ Perhaps: "(str =~ (fromMaybe \".*\" incReg))\n && not (str =~ fromMaybe \"a^\" excReg)"

Check warning on line 286 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Redundant bracket ▫︎ Found: "str =~ (fromMaybe \".*\" incReg)" ▫︎ Perhaps: "str =~ fromMaybe \".*\" incReg"
let archDesc = arch flags
let csrFilter idx = checkRegex (csrIncludeRegex flags) (csrExcludeRegex flags) (fromMaybe "reserved" $ csrs_nameFromIndex idx)
let testParams = T.TestParams { T.archDesc = archDesc
Expand All @@ -300,7 +301,7 @@
quickCheckWithResult (Args Nothing 1 1 len (verbosity > 0) (if doShrink then 1000 else 0))
(prop implA m_implB alive onFail archDesc (timeoutDelay flags) verbosity Nothing (optIgnoreAsserts flags) (optStrict flags) (return test))
let check_mcause_on_trap :: Test TestResult -> Test TestResult
check_mcause_on_trap (trace :: Test TestResult) = if or (hasTrap <$> trace) then filterTest p trace <> wrapTest testSuffix else trace

Check warning on line 304 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Warning in main in module Main: Use any ▫︎ Found: "or (hasTrap <$> trace)" ▫︎ Perhaps: "any hasTrap trace"
where hasTrap (_, a, b) = maybe False rvfiIsTrap a || maybe False rvfiIsTrap b
testSuffix = noShrink $ singleSeq [ csrrs 1 (unsafe_csrs_indexFromName "mcause") 0
, csrrs 1 (unsafe_csrs_indexFromName "mtval" ) 0
Expand Down Expand Up @@ -342,7 +343,7 @@
let checkResult = if verbosity > 1 then verboseCheckWithResult else quickCheckWithResult
let checkGen gen remainingTests =
checkResult (Args Nothing remainingTests 1 (testLen flags) (verbosity > 0) (if optShrink flags then 1000 else 0))
(prop implA m_implB alive (checkTrapAndSave Nothing) archDesc (timeoutDelay flags) verbosity (if (optSaveAll flags) then (saveDir flags) else Nothing) (optIgnoreAsserts flags) (optStrict flags) gen)

Check warning on line 346 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Redundant bracket ▫︎ Found: "if (optSaveAll flags) then (saveDir flags) else Nothing" ▫︎ Perhaps: "if optSaveAll flags then (saveDir flags) else Nothing"

Check warning on line 346 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Redundant bracket ▫︎ Found: "if (optSaveAll flags) then (saveDir flags) else Nothing" ▫︎ Perhaps: "if (optSaveAll flags) then saveDir flags else Nothing"
failuresRef <- newIORef 0
let checkFile (memoryInitFile :: Maybe FilePath) (skipped :: Int) (fileName :: FilePath)
| skipped == 0 = do putStrLn $ "Reading trace from " ++ fileName
Expand Down Expand Up @@ -382,7 +383,7 @@
where attemptTest (label, description, archReqs, template) =
if archReqs archDesc then do
putStrLn $ label ++ " -- " ++ description ++ ":"
(if optContinueOnFail flags then repeatTillTarget else (\f t -> f t >> return ())) ((numTests <$>) . (doCheck (wrapTest <$> (T.genTest testParams template)))) (nTests flags)

Check warning on line 386 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Use void ▫︎ Found: "f t >> return ()" ▫︎ Perhaps: "void (f t)"

Check warning on line 386 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Redundant bracket ▫︎ Found: "(numTests <$>)\n . (doCheck (wrapTest <$> (T.genTest testParams template)))" ▫︎ Perhaps: "(numTests <$>)\n . doCheck (wrapTest <$> (T.genTest testParams template))"

Check warning on line 386 in src/QuickCheckVEngine/Main.hs

View workflow job for this annotation

GitHub Actions / Run HLint on the QuickCheck Verification Engine codebase

Suggestion in main in module Main: Redundant bracket ▫︎ Found: "wrapTest <$> (T.genTest testParams template)" ▫︎ Perhaps: "wrapTest <$> T.genTest testParams template"
else
putStrLn $ "Warning: skipping " ++ label ++ " since architecture requirements not met"
repeatTillTarget f t = if t <= 0 then return () else f t >>= (\x -> repeatTillTarget f (t - x))
Expand Down
45 changes: 45 additions & 0 deletions src/QuickCheckVEngine/Templates/GenUnstructured.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
--
-- SPDX-License-Identifier: BSD-2-Clause
--
-- Copyright (c) 2025 Peter Rugg
-- All rights reserved.
--
-- This software was developed by SRI International and the University of
-- Cambridge Computer Laboratory (Department of Computer Science and
-- Technology) under DARPA contract HR0011-18-C-0016 ("ECATS"), as part of the
-- DARPA SSITH research programme.
--
-- Redistribution and use in source and binary forms, with or without
-- modification, are permitted provided that the following conditions
-- are met:
-- 1. Redistributions of source code must retain the above copyright
-- notice, this list of conditions and the following disclaimer.
-- 2. 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.
--
-- THIS SOFTWARE IS PROVIDED BY THE AUTHOR 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 AUTHOR 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.
--

module QuickCheckVEngine.Templates.GenUnstructured (
gen_unstructured
) where

import QuickCheckVEngine.Template
import QuickCheckVEngine.Templates.Utils

Check failure on line 39 in src/QuickCheckVEngine/Templates/GenUnstructured.hs

View workflow job for this annotation

GitHub Actions / Build the QuickCheck Verification Engine

Could not find module ‘QuickCheckVEngine.Templates.Utils’.
import InstrCodec

gen_unstructured :: Template
gen_unstructured = random $ do
instBits <- bits 32
return $ inst $ MkInstruction instBits
Loading