diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c)2013, Galois, Inc + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * 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. + + * Neither the name of Galois, Inc nor the names of its contributors + may be used to endorse or promote products derived from this software + without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS 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 COPYRIGHT +OWNER 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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ivory-stdlib.cabal b/ivory-stdlib.cabal new file mode 100644 --- /dev/null +++ b/ivory-stdlib.cabal @@ -0,0 +1,39 @@ +name: ivory-stdlib +version: 0.1.0.0 +author: Galois, Inc. +maintainer: pat@galois.com +copyright: 2013 Galois, Inc. +category: Language +synopsis: Ivory standard library. +description: A standard library for Ivory. +homepage: http://smaccmpilot.org/languages/ivory-introduction.html +build-type: Simple +cabal-version: >= 1.10 +license: BSD3 +license-file: LICENSE +data-files: support/ivory_stdlib_string_prim.h, + support/ivory_stdlib_string_prim.c +source-repository this + type: git + location: https://github.com/GaloisInc/ivory + tag: hackage-stdlib-0100 + +library + exposed-modules: Ivory.Stdlib, + Ivory.Stdlib.Control, + Ivory.Stdlib.Memory, + Ivory.Stdlib.Operators, + Ivory.Stdlib.String, + Ivory.Stdlib.Trig, + Ivory.Stdlib.SearchDir, + Ivory.Stdlib.Maybe + + other-modules: Paths_ivory_stdlib + + build-depends: base >= 4.6 && < 4.7, + filepath, + ivory + + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall diff --git a/src/Ivory/Stdlib.hs b/src/Ivory/Stdlib.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Stdlib.hs @@ -0,0 +1,23 @@ + +module Ivory.Stdlib + ( module Ivory.Stdlib.Control + , module Ivory.Stdlib.Memory + , module Ivory.Stdlib.Operators + , module Ivory.Stdlib.String + , module Ivory.Stdlib.Maybe + , stdlibModules + ) where + +import Ivory.Language (Module) + +import Ivory.Stdlib.Control +import Ivory.Stdlib.Memory +import Ivory.Stdlib.Operators +import Ivory.Stdlib.String +import Ivory.Stdlib.Maybe + +stdlibModules :: [Module] +stdlibModules = + [ stdlibStringModule + ] + diff --git a/src/Ivory/Stdlib/Control.hs b/src/Ivory/Stdlib/Control.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Stdlib/Control.hs @@ -0,0 +1,87 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} + +module Ivory.Stdlib.Control + ( ifte + , when + , unless + , cond_, cond, (==>) + ) where + +import Ivory.Language + +ifte :: ( IvoryStore a + , IvoryZero (Stored a) + , GetAlloc eff ~ Scope s + ) => IBool + -> Ivory eff a + -> Ivory eff a + -> Ivory eff a +ifte c t f = do + r <- local izero + ifte_ c + (t >>= store r) + (f >>= store r) + deref r + +when :: IBool -> Ivory eff () -> Ivory eff () +when c t = ifte_ c t (return ()) + +unless :: IBool -> Ivory eff () -> Ivory eff () +unless c f = ifte_ c (return ()) f + +data Cond eff a = Cond IBool (Ivory eff a) + +(==>) :: IBool -> Ivory eff a -> Cond eff a +(==>) = Cond + +infix 0 ==> + +-- | A multi-way if. This is useful for avoiding an explosion of +-- nesting and parentheses in complex conditionals. +-- +-- Instead of writing nested chains of ifs: +-- +-- > ifte_ (x >? 100) +-- > (store result 10) +-- > (ifte_ (x >? 50) +-- > (store result 5) +-- > (ifte_ (x >? 0) +-- > (store result 1) +-- > (store result 0))) +-- +-- You can write: +-- +-- > cond_ +-- > [ x >? 100 ==> store result 10 +-- > , x >? 50 ==> store result 5 +-- > , x >? 0 ==> store result 1 +-- > , true ==> store result 0 +-- > ] +-- +-- Note that "==>" is non-associative and has precedence 0, so you +-- will need parentheses to call functions with "$" on the left-hand +-- side: +-- +-- > cond_ [ (f $ g x) ==> y ] +-- +-- rather than: +-- +-- > cond_ [ f $ g x ==> y ] +cond_ :: [Cond eff ()] -> Ivory eff () +cond_ [] = return () +cond_ ((Cond b f):cs) = ifte_ b f (cond_ cs) + +cond :: ( IvoryStore a + , IvoryZero (Stored a) + , GetAlloc eff ~ Scope s + ) => [Cond eff a] -> Ivory eff a +cond as = do + r <- local izero + aux as r + deref r + where + aux [] _ = return () + aux ((Cond b f):cs) r = ifte_ b (f >>= store r) (aux cs r) diff --git a/src/Ivory/Stdlib/Maybe.hs b/src/Ivory/Stdlib/Maybe.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Stdlib/Maybe.hs @@ -0,0 +1,178 @@ +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE FlexibleContexts #-} +-- +-- Maybe.hs --- Optional Ivory values. +-- +-- Copyright (C) 2013, Galois, Inc. +-- All Rights Reserved. +-- +-- This software is released under the "BSD3" license. Read the file +-- "LICENSE" for more information. +-- + +-- | This module provides an interface for a nullable Ivory type. +-- +-- To define a type like Haskell's @Maybe Float@, define an +-- Ivory structure type, and make the structure an instance +-- of 'MaybeType'. +-- +-- > [ivory| +-- > struct maybe_float +-- > { mf_valid :: Stored IBool +-- > ; mf_value :: Stored IFloat +-- > } +-- > |] +-- > +-- > instance MaybeType "maybe_float" IFloat where +-- > maybeValidLabel = mf_valid +-- > maybeValueLabel = mf_value +-- +-- With this definition in place, any of the functions in this +-- module will accept a @Struct \"maybe_float\"@. +-- +-- These structure types must be defined in an Ivory module as +-- usual, and it is recommended to make them private unless they +-- are necessary as part of the module's public interface. +module Ivory.Stdlib.Maybe + ( + -- * Interface + MaybeType(..) + + -- * Initialization + , initJust, initNothing + + -- * Getting + , getMaybe + + -- * Setting + , setJust, setNothing + , setDefault, setDefault_ + + -- * Modifying + , mapMaybe + , mapMaybeM, mapMaybeM_ + , forMaybeM, forMaybeM_ + ) where + +import GHC.TypeLits + +import Ivory.Language + +class (IvoryStruct sym, IvoryExpr t, IvoryStore t, IvoryInit t) => + MaybeType (sym :: Symbol) t | sym -> t where + -- | Return a boolean field indicating whether the value is valid. + maybeValidLabel :: Label sym (Stored IBool) + -- | Return the field containing a value, if it is valid. + maybeValueLabel :: Label sym (Stored t) + +-- | Return an initializer for a maybe type with a valid value. +initJust :: MaybeType sym a => a -> Init (Struct sym) +initJust x = + istruct + [ maybeValidLabel .= ival true + , maybeValueLabel .= ival x + ] + +-- | Return an initializer for a maybe type with no value. +initNothing :: MaybeType sym a => Init (Struct sym) +initNothing = + istruct + [ maybeValidLabel .= ival false + ] + +-- | Retrieve a maybe's value given a default if it is nothing. +getMaybe :: MaybeType sym a + => ConstRef s1 (Struct sym) + -> a + -> Ivory eff a +getMaybe ref def = do + valid <- deref (ref ~> maybeValidLabel) + value <- deref (ref ~> maybeValueLabel) + assign (valid ? (value, def)) + +-- | Set a maybe's value to a default if it is nothing, returning +-- the current value. +setDefault :: MaybeType sym a + => Ref s1 (Struct sym) + -> a + -> Ivory eff a +setDefault ref def = do + setDefault_ ref def + deref (ref ~> maybeValueLabel) + +-- | Set a maybe's value to a default value if it is nothing. +setDefault_ :: MaybeType sym a + => Ref s1 (Struct sym) + -> a + -> Ivory eff () +setDefault_ ref def = do + valid <- deref (ref ~> maybeValidLabel) + ifte_ (iNot valid) + (do store (ref ~> maybeValidLabel) true + store (ref ~> maybeValueLabel) def) + (return ()) + +-- | Modify a maybe value by an expression if it is not nothing. +mapMaybe :: MaybeType sym a + => (a -> a) + -> Ref s1 (Struct sym) + -> Ivory eff () +mapMaybe f ref = mapMaybeM (return . f) ref + +-- | Modify a maybe value by an action if it is not nothing. +mapMaybeM :: MaybeType sym a + => (a -> Ivory eff a) + -> Ref s1 (Struct sym) + -> Ivory eff () +mapMaybeM f ref = do + valid <- deref (ref ~> maybeValidLabel) + ifte_ valid + (do value <- deref (ref ~> maybeValueLabel) + value' <- f value + store (ref ~> maybeValueLabel) value') + (return ()) + +-- | Flipped version of 'mapMaybeM'. +forMaybeM :: MaybeType sym a + => Ref s1 (Struct sym) + -> (a -> Ivory eff a) + -> Ivory eff () +forMaybeM = flip mapMaybeM + +-- | Call an action with a maybe value if it is not nothing. +mapMaybeM_ :: MaybeType sym a + => (a -> Ivory eff ()) + -> Ref s1 (Struct sym) + -> Ivory eff () +mapMaybeM_ f ref = do + valid <- deref (ref ~> maybeValidLabel) + ifte_ valid + (do value <- deref (ref ~> maybeValueLabel) + f value) + (return ()) + +-- | Flipped version of 'mapMaybeM_'. +forMaybeM_ :: MaybeType sym a + => Ref s1 (Struct sym) + -> (a -> Ivory eff ()) + -> Ivory eff () +forMaybeM_ = flip mapMaybeM_ + +-- | Set a maybe value to a valid value. +setJust :: MaybeType sym a + => Ref s1 (Struct sym) + -> a + -> Ivory eff () +setJust ref x = do + store (ref ~> maybeValidLabel) true + store (ref ~> maybeValueLabel) x + +-- | Set a maybe value to an invalid value. +setNothing :: MaybeType sym a + => Ref s1 (Struct sym) + -> Ivory eff () +setNothing ref = store (ref ~> maybeValidLabel) false + diff --git a/src/Ivory/Stdlib/Memory.hs b/src/Ivory/Stdlib/Memory.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Stdlib/Memory.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Ivory.Stdlib.Memory + ( resultInto + , into + , arrayCopy + ) where + +import Ivory.Language +import Ivory.Stdlib.Control + +-- | handy shorthand for transfering members +resultInto :: IvoryStore a => + Ivory eff a -> Ref s (Stored a) -> Ivory eff () +resultInto a b = store b =<< a + +into :: IvoryStore a => + Ref s (Stored a) -> Ref s' (Stored a) -> Ivory eff () +into a b = store b =<< deref a + +-- XXX Belongs with Pack.hs and SafePack.hs. + +-- | Copies a prefix of an array into a postfix of another array. That is, copy +-- from array @from@ (either a 'Ref' or a 'ConstRef') into array @to@ starting +-- at index @toOffset@ in @to@. Copying continues until either the from array +-- is fully copied, the @to@ array is full, or index @end@ in the @from@ array +-- is reached (index @end@ is not copied). to copy the full @from@ array, let +-- @end@ equal 'arrayLen from'. +arrayCopy :: forall n m r s0 s1 s2 eff t. + ( SingI n, SingI m, IvoryRef r + , IvoryExpr (r s2 (Array m (Stored t))) + , IvoryExpr (r s2 (Stored t)) + , IvoryStore t + , GetAlloc eff ~ Scope s0 + ) + => Ref s1 (Array n (Stored t)) + -> r s2 (Array m (Stored t)) + -> Sint32 + -> Sint32 + -> Ivory eff () +arrayCopy to from toOffset end = do + assert (toOffset >=? 0 .&& toOffset =? 0 .&& end <=? frLen) + arrayMap $ go + where + -- The index is w.r.t. the from array. + go ix = + cond_ + [ -- We've reached the @end@ index: stop copying. + (fromIx ix >=? end) + ==> return () + , -- We've reached the end of the @to@ array: stop copying. + (fromIx ix + toOffset >=? toLen) + ==> return () + , true + ==> (deref (from ! ix) >>= store (to ! mkIx ix)) + ] + + toLen = arrayLen to + frLen = arrayLen from + + mkIx :: Ix m -> Ix n + mkIx ix = toIx (toOffset + fromIx ix) + diff --git a/src/Ivory/Stdlib/Operators.hs b/src/Ivory/Stdlib/Operators.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Stdlib/Operators.hs @@ -0,0 +1,39 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleContexts #-} + +module Ivory.Stdlib.Operators where + +import Ivory.Language + +-- | Infix structure field access and dereference. +-- This is a shorthand for 'deref $ s~>x'. +(~>*) :: (IvoryVar a, IvoryStruct sym, IvoryRef ref, + IvoryExpr (ref s (Stored a)), + IvoryExpr (ref s (Struct sym))) => + ref s (Struct sym) -> Label sym (Stored a) -> Ivory eff a +struct ~>* label = deref $ struct~>label +infixl 8 ~>* + + +-- | Modify the value stored at a reference by a function. +(%=) :: IvoryStore a => + Ref s (Stored a) -> (a -> a) -> Ivory eff () +ref %= f = do + val <- deref ref + store ref (f val) + +-- | Modify the value stored at a reference by a function that returns +-- a value in the Ivory monad +(%=!) :: IvoryStore a => + Ref s (Stored a) -> (a -> Ivory eff a) -> Ivory eff () +ref %=! mf = do + val <- deref ref + val' <- mf val + store ref val' + +-- | Increment the value stored at a reference. +(+=) :: (Num a, IvoryStore a) => + Ref s (Stored a) -> a -> Ivory eff () +ref += x = ref %= (+ x) + diff --git a/src/Ivory/Stdlib/SearchDir.hs b/src/Ivory/Stdlib/SearchDir.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Stdlib/SearchDir.hs @@ -0,0 +1,13 @@ + +module Ivory.Stdlib.SearchDir where + +import System.FilePath + +import qualified Paths_ivory_stdlib + +searchDir :: IO FilePath +searchDir = do + base <- Paths_ivory_stdlib.getDataDir + return $ base "support" + + diff --git a/src/Ivory/Stdlib/String.hs b/src/Ivory/Stdlib/String.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Stdlib/String.hs @@ -0,0 +1,264 @@ +{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE QuasiQuotes #-} +-- +-- String.hs --- C-string utilities for Ivory. +-- +-- Copyright (C) 2013, Galois, Inc. +-- All Rights Reserved. +-- + +module Ivory.Stdlib.String where + -- ( copy_istring , strcpy , strncpy , strncpy_uint8 , strncmp + -- , stdlibStringModule + -- ) where + +import Data.Char (ord) +import GHC.TypeLits + +import Ivory.Language + +import qualified Control.Monad as M + +---------------------------------------------------------------------- +-- Yet Another Ivory String Type + +-- TODO: Should we generate a warning or error if the string +-- is too long for the string type? +gen_stringInit :: (IvoryStruct name, SingI len) + => Label name (Array len (Stored Uint8)) + -> Label name (Stored (Ix len)) + -> String + -> Init (Struct name) +gen_stringInit l_data l_len xs = + istruct + [ l_data .= iarray (map (ival . fromIntegral . ord) xs) + , l_len .= ival (toIx len) + ] + where + len :: Sint32 + len = fromIntegral (length xs) + +stringInit :: IvoryString str => String -> Init str +stringInit = gen_stringInit stringDataL stringLengthL + +---------------------------------------------------------------------- +-- Generic Functions + +stringCapacity :: forall ref str s. + (IvoryString str, IvoryRef ref) + => ref s str -> Sint32 +stringCapacity _ = len + where + len :: Sint32 + len = fromIntegral (fromSing (sing :: Sing (Capacity str))) + +-- Polymorphic "stringLength" function allowing read/write access +-- to the string length. This is not exported, only a specialized +-- read-only version. +stringLength :: ( IvoryString str + , IvoryRef ref + , IvoryExpr (ref s (Stored (Ix (Capacity str)))) + , IvoryExpr (ref s str)) + => ref s str -> ref s (Stored (Ix (Capacity str))) +stringLength x = x ~> stringLengthL + +stringData :: ( IvoryString str + , IvoryRef ref + , IvoryExpr (ref s (Array (Capacity str) (Stored Uint8))) + , IvoryExpr (ref s (CArray (Stored Uint8))) + , IvoryExpr (ref s str)) + => ref s str -> ref s (CArray (Stored Uint8)) +stringData x = toCArray (x ~> stringDataL) + +-- | Binding to the C "memcmp" function. +memcmp :: Def ('[ ConstRef s1 (CArray (Stored Uint8)) + , ConstRef s2 (CArray (Stored Uint8)) + , Sint32] :-> Sint32) +memcmp = importProc "memcmp" "string.h" + +-- | Binding to the C "memcpy" function. +memcpy :: Def ('[ Ref s1 (CArray (Stored Uint8)) + , ConstRef s2 (CArray (Stored Uint8)) + , Sint32] :-> Sint32) +memcpy = importProc "memcpy" "string.h" + +-- | Return the length of a string. +istr_len :: IvoryString str + => ConstRef s str + -> Ivory eff (Ix (Capacity str)) +istr_len str = do + len <- deref (stringLength str) + assert (fromIx len Ref s1 str + -> ConstRef s2 str + -> Ivory eff () +istr_copy dest src = do + len <- istr_len src + call_ memcpy (stringData dest) (stringData src) (fromIx len) + store (stringLength dest) len + +-- | Copy one string to another of a possibly different type. If +-- the destination string is too small, the output may be truncated. +-- This returns true if the string fit, and false if it was +-- truncated to fit the destination. +-- +-- TODO: Implement this once it's needed. +istr_convert :: (IvoryString str1, IvoryString str2) + => Ref s1 str1 + -> ConstRef s2 str2 + -> Ivory eff IBool +istr_convert = undefined + +-- | Internal function to compare strings for equality. +do_istr_eq :: Def ('[ ConstRef s1 (CArray (Stored Uint8)) + , Sint32 + , ConstRef s2 (CArray (Stored Uint8)) + , Sint32 + ] :-> IBool) +do_istr_eq = proc "ivory_string_eq" $ \s1 len1 s2 len2 -> body $ do + ifte_ (len1 ==? len2) + (do r <- call memcmp s1 s2 len1 + ret (r ==? 0)) + (ret false) + +-- | Compare strings (of possibly different types) for equality. +-- Returns true if the strings are the same length and contain the +-- same bytes. +istr_eq :: (IvoryString str1, IvoryString str2) + => ConstRef s1 str1 + -> ConstRef s2 str2 + -> Ivory eff IBool +istr_eq s1 s2 = do + len1 <- istr_len s1 + ptr1 <- assign (stringData s1) + len2 <- istr_len s2 + ptr2 <- assign (stringData s2) + call do_istr_eq ptr1 (fromIx len1) ptr2 (fromIx len2) + +-- | Primitive function to do a bounded string copy. +string_copy :: Def ('[ Ref s1 (CArray (Stored Uint8)) + , Sint32 + , ConstRef s2 (CArray (Stored Uint8)) + , Sint32] :-> Sint32) +string_copy = importProc "ivory_stdlib_string_copy" + "ivory_stdlib_string_prim.h" + +-- | Primitive function to do a bounded null-terminated string copy. +string_copy_z :: Def ('[ Ref s1 (CArray (Stored Uint8)) + , Sint32 + , ConstRef s2 (CArray (Stored Uint8)) + , Sint32] :-> Sint32) +string_copy_z = importProc "ivory_stdlib_string_copy_z" + "ivory_stdlib_string_prim.h" + +-- | Copy the contents of a fixed-size C string into an Ivory +-- string. If the source string is not null terminated (and +-- therefore corrupt), this will copy no more than 'len' +-- characters. +-- +-- FIXME: This should return false if the string was truncated. +-- (Can we actually detect this at compile-time? I think we +-- should be able to...) +istr_from_sz :: forall s1 s2 eff len str. + (SingI len, IvoryString str) + => Ref s1 str + -> ConstRef s2 (Array len (Stored Uint8)) + -> Ivory eff () +istr_from_sz dest src = do + len1 <- assign (stringCapacity (constRef dest)) + ptr1 <- assign (stringData dest) + let len2 = fromIntegral (fromSing (sing :: Sing len)) + ptr2 <- assign (toCArray src) + result <- call string_copy_z ptr1 len1 ptr2 len2 + store (stringLength dest) (toIx result) + +-- | Copy an Ivory string to a fixed-size, null-terminated C +-- string. The destination string is always properly terminated, +-- but may be truncated if the buffer is too small. +-- +-- FIXME: This should return false if the string was truncated. +-- (Can we actually detect this at compile-time? I think we +-- should be able to...) +sz_from_istr :: forall s1 s2 eff len str. + (SingI len, IvoryString str) + => Ref s1 (Array len (Stored Uint8)) + -> ConstRef s2 str + -> Ivory eff () +sz_from_istr dest src = do + let dest_capacity = fromSing (sing :: Sing len) + M.when (dest_capacity > 0) $ do + let dest_len = fromIntegral (dest_capacity - 1) + src_data <- assign (stringData src) + src_len <- istr_len src + _result <- call string_copy (toCArray dest) dest_len src_data (fromIx src_len) + -- XXX is this right? shouldn't it use "result"? + store (dest ! toIx (dest_len - 1)) 0 + +---------------------------------------------------------------------- +-- Old String Functions + +-- TODO: Delete these if they aren't used anymore. + +-- | Safely copy an IString (string literal) into a character array. +-- The resulting string will always be null terminated. +copy_istring :: Def ('[ Ref s (CArray (Stored IChar)) -- dest + , IString -- src + , Uint32] -- len + :-> ()) +copy_istring = importProc "ivory_stdlib_strlcpy" "ivory_stdlib_string_prim.h" + +-- | Type class to generate the correct call to a string function to +-- copy one C string to another. +class (IvoryType dest, IvoryType src) => Strcpy dest src where + strcpy :: dest -> src -> Ivory eff () + +-- | Strcpy instance for copying string constants to arrays of +-- characters. +instance (SingI len) => Strcpy (Ref s (Array len (Stored IChar))) IString where + strcpy dest src = call_ copy_istring (toCArray dest) src (arrayLen dest) + +-- | Binding to the C "strncmp" function. +strncmp :: Def ('[ ConstRef s1 (CArray (Stored IChar)) -- s1 + , ConstRef s2 (CArray (Stored IChar)) -- s2 + , Uint32] -- len + :-> Sint32) +strncmp = importProc "strncmp" "string.h" + + +strncpy :: Def ('[ Ref s1 (CArray (Stored IChar)) + , ConstRef s2 (CArray (Stored IChar)) + , Uint32 + ] :-> ()) +strncpy = importProc "strncpy" "string.h" + +strncpy_uint8 :: Def ('[ Ref s1 (CArray (Stored Uint8)) + , ConstRef s2 (CArray (Stored IChar)) + , Uint32 + ] :-> ()) +strncpy_uint8 = importProc "ivory_stdlib_strncpy_uint8" "ivory_stdlib_string_prim.h" + +-- | Ivory module definition. +stdlibStringModule :: Module +stdlibStringModule = package "ivory_stdlib_string" $ do + inclHeader "ivory_stdlib_string_prim.h" + inclHeader "string.h" + incl copy_istring + incl strncmp + incl memcmp + incl memcpy + incl do_istr_eq + incl string_copy + incl string_copy_z + sourceDep "ivory_stdlib_string_prim.h" + sourceDep "ivory_stdlib_string_prim.c" + diff --git a/src/Ivory/Stdlib/Trig.hs b/src/Ivory/Stdlib/Trig.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/Stdlib/Trig.hs @@ -0,0 +1,15 @@ + +module Ivory.Stdlib.Trig + ( iAtan2 + ) where + +import Ivory.Language + +-- spec: http://en.wikipedia.org/wiki/Atan2 +iAtan2 :: (IvoryOrd a, Floating a) => a -> a -> a +iAtan2 y x = ((x >? 0)?( atan(y/x) + ,((y >=? 0).&&(x ? 0).&&(x ==? 0))?( pi/2 + ,((y + +void ivory_stdlib_strncpy_uint8(uint8_t *dest, const char *src, uint32_t size) { + strncpy((char*)dest, src, size); +} + +/* + * Copy src to string dst of size siz. At most siz-1 characters + * will be copied. Always NUL terminates (unless siz == 0). + * Returns strlen(src); if retval >= siz, truncation occurred. + * + * Copyright (c) 1998 Todd C. Miller + * All rights reserved. + * + * 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. + * 3. The name of the author may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED ``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 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. + */ +uint32_t ivory_stdlib_strlcpy(char *dest, const char *src, uint32_t size) +{ + char *d = dest; + const char *s = src; + uint32_t n = size; + + /* Copy as many bytes as will fit */ + if (n != 0 && --n != 0) { + do { + if ((*d++ = *s++) == 0) + break; + } while (--n != 0); + } + + /* Not enough room in dest, add NUL and traverse rest of src */ + if (n == 0) { + if (size != 0) + *d = '\0'; /* NUL-terminate dest */ + while (*s++) + ; + } + + return (s - src - 1); /* count does not include NUL */ +} + +/* Copy at most 'min(dest_len, src_len)' bytes from 'src' to + * dest. Returns the number of bytes written to 'dest', which + * is not null terminated. */ +int32_t ivory_stdlib_string_copy( + uint8_t *dest, int32_t dest_len, + const uint8_t *src, int32_t src_len) +{ + int32_t result = 0; + int32_t n = dest_len < src_len ? dest_len : src_len; + + for (int32_t i = 0; i < n; ++i) { + dest[i] = src[i]; + ++result; + } + + return result; +} + +/* Copy at most 'min(dest_len, src_len)' bytes from 'src' to + * dest, stopping early if a null terminator is encountered. + * + * Returns the number of bytes written to 'dest' (which is + * never null-terminated. */ +int32_t ivory_stdlib_string_copy_z( + uint8_t *dest, int32_t dest_len, + const uint8_t *src, int32_t src_len) +{ + int32_t result = 0; + int32_t n = dest_len < src_len ? dest_len : src_len; + + for (int32_t i = 0; i < n; ++i) { + if (src[i] == 0) + break; + + dest[i] = src[i]; + ++result; + } + + return result; +} + diff --git a/support/ivory_stdlib_string_prim.h b/support/ivory_stdlib_string_prim.h new file mode 100644 --- /dev/null +++ b/support/ivory_stdlib_string_prim.h @@ -0,0 +1,43 @@ +/* -*- Mode: C; indent-tabs-mode: nil; c-basic-offset: 4 -*- */ +/* + * ivory_string_stdlib_prim.h --- C string primitives. + * + * Copyright (C) 2013, Galois, Inc. + * All Rights Reserved. + */ + +#ifndef __IVORY_STDLIB_STRING_PRIM_H__ +#define __IVORY_STDLIB_STRING_PRIM_H__ + +#include +#include + +#ifdef __cplusplus +extern "C" { +#endif + +uint32_t ivory_stdlib_strlcpy(char *dest, const char *src, uint32_t size); + +void ivory_stdlib_strncpy_uint8( uint8_t *dest, const char *src, uint32_t size); + +/* Copy at most 'min(dest_len, src_len)' bytes from 'src' to + * dest, stopping early if a null terminator is encountered. + * + * Returns the number of bytes written to 'dest' (which is + * never null-terminated. */ +int32_t ivory_stdlib_string_copy_z( + uint8_t *dest, int32_t dest_len, + const uint8_t *src, int32_t src_len); + +/* Copy at most 'min(dest_len, src_len)' bytes from 'src' to + * dest. Returns the number of bytes written to 'dest', which + * is not null terminated. */ +int32_t ivory_stdlib_string_copy( + uint8_t *dest, int32_t dest_len, + const uint8_t *src, int32_t src_len); + +#ifdef __cplusplus +} +#endif + +#endif /* !defined __IVORY_STDLIB_STRING_PRIM_H__ */