1----------------------------------------------------------------------------- 2-- | 3-- Module : Documentation.SBV.Examples.CodeGeneration.Uninterpreted 4-- Copyright : (c) Levent Erkok 5-- License : BSD3 6-- Maintainer: erkokl@gmail.com 7-- Stability : experimental 8-- 9-- Demonstrates the use of uninterpreted functions for the purposes of 10-- code generation. This facility is important when we want to take 11-- advantage of native libraries in the target platform, or when we'd 12-- like to hand-generate code for certain functions for various 13-- purposes, such as efficiency, or reliability. 14----------------------------------------------------------------------------- 15 16{-# OPTIONS_GHC -Wall -Werror #-} 17 18module Documentation.SBV.Examples.CodeGeneration.Uninterpreted where 19 20import Data.Maybe (fromMaybe) 21 22import Data.SBV 23import Data.SBV.Tools.CodeGen 24 25-- | A definition of shiftLeft that can deal with variable length shifts. 26-- (Note that the ``shiftL`` method from the 'Bits' class requires an 'Int' shift 27-- amount.) Unfortunately, this'll generate rather clumsy C code due to the 28-- use of tables etc., so we uninterpret it for code generation purposes 29-- using the 'cgUninterpret' function. 30shiftLeft :: SWord32 -> SWord32 -> SWord32 31shiftLeft = cgUninterpret "SBV_SHIFTLEFT" cCode hCode 32 where -- the C code we'd like SBV to spit out when generating code. Note that this is 33 -- arbitrary C code. In this case we just used a macro, but it could be a function, 34 -- text that includes files etc. It should essentially bring the name SBV_SHIFTLEFT 35 -- used above into scope when compiled. If no code is needed, one can also just 36 -- provide the empty list for the same effect. Also see 'cgAddDecl', 'cgAddLDFlags', 37 -- and 'cgAddPrototype' functions for further variations. 38 cCode = ["#define SBV_SHIFTLEFT(x, y) ((x) << (y))"] 39 -- the Haskell code we'd like SBV to use when running inside Haskell or when 40 -- translated to SMTLib for verification purposes. This is good old Haskell 41 -- code, as one would typically write. 42 hCode x = select [x * literal (bit b) | b <- [0.. bs x - 1]] (literal 0) 43 bs x = fromMaybe (error "SBV.Example.CodeGeneration.Uninterpreted.shiftLeft: Unexpected non-finite usage!") (bitSizeMaybe x) 44 45-- | Test function that uses shiftLeft defined above. When used as a normal Haskell function 46-- or in verification the definition is fully used, i.e., no uninterpretation happens. To wit, 47-- we have: 48-- 49-- >>> tstShiftLeft 3 4 5 50-- 224 :: SWord32 51-- 52-- >>> prove $ \x y -> tstShiftLeft x y 0 .== x + y 53-- Q.E.D. 54tstShiftLeft :: SWord32 -> SWord32 -> SWord32 -> SWord32 55tstShiftLeft x y z = x `shiftLeft` z + y `shiftLeft` z 56 57-- | Generate C code for "tstShiftLeft". In this case, SBV will *use* the user given definition 58-- verbatim, instead of generating code for it. (Also see the functions 'cgAddDecl', 'cgAddLDFlags', 59-- and 'cgAddPrototype'.) 60genCCode :: IO () 61genCCode = compileToC Nothing "tst" $ do 62 [x, y, z] <- cgInputArr 3 "vs" 63 cgReturn $ tstShiftLeft x y z 64