diff --git a/QCVEngine.cabal b/QCVEngine.cabal index 1603eb2..5ca014e 100644 --- a/QCVEngine.cabal +++ b/QCVEngine.cabal @@ -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, diff --git a/src/QuickCheckVEngine/Main.hs b/src/QuickCheckVEngine/Main.hs index 10c5d9c..03f01ef 100644 --- a/src/QuickCheckVEngine/Main.hs +++ b/src/QuickCheckVEngine/Main.hs @@ -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) ] where andPs = foldl (\k p x -> p x && k x) (const True) diff --git a/src/QuickCheckVEngine/Templates/GenUnstructured.hs b/src/QuickCheckVEngine/Templates/GenUnstructured.hs new file mode 100644 index 0000000..d4fce4f --- /dev/null +++ b/src/QuickCheckVEngine/Templates/GenUnstructured.hs @@ -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 +import InstrCodec + +gen_unstructured :: Template +gen_unstructured = random $ do + instBits <- bits 32 + return $ inst $ MkInstruction instBits