Skip to content

Commit

Permalink
Add 'unstructured' template that tests random instruction bit patterns
Browse files Browse the repository at this point in the history
This is intended to be used in single-implementation mode to check
that unknown bit patterns at least do not wedge the processor.
  • Loading branch information
PeterRugg committed Jan 15, 2025
1 parent 9932abb commit 73aa7b4
Show file tree
Hide file tree
Showing 3 changed files with 47 additions and 0 deletions.
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 @@ allTests = [
, ("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 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

0 comments on commit 73aa7b4

Please sign in to comment.