diff --git a/examples/Alloc.hs b/examples/Alloc.hs --- a/examples/Alloc.hs +++ b/examples/Alloc.hs @@ -1,15 +1,15 @@ {-# OPTIONS_GHC -fno-warn-orphans #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TypeOperators #-} module Alloc where -import Ivory.Language -import Ivory.Compile.C.CmdlineFrontend -import Ivory.Compile.C.Modules +import Ivory.Compile.C.CmdlineFrontend +import Ivory.Compile.C.Modules +import Ivory.Language [ivory| @@ -53,16 +53,16 @@ arrayMap (\ix -> store (a ! (ix :: Ix 10)) 1) retVoid +{- -- Can't do this! (Which is good.) --- memcpy4 :: Def ('[ Ref Global (Array 1 (Stored (Ref (Stack s) (Stored Uint32))))] :-> ()) --- memcpy4 = proc "memcpy3" $ \a -> body $ do --- val <- local (ival 2) --- larr <- local (iarray [ival val]) --- refCopy a larr --- arrayMap (\ix -> store (a ! (ix :: Ix 1)) 1) --- retVoid +memcpy4 :: Def ('[ Ref Global (Array 1 (Stored (Ref (Stack s) (Stored Uint32))))] :-> ()) +memcpy4 = proc "memcpy3" $ \a -> body $ do + val <- local (ival 2) + larr <- local (iarray [ival val]) + refCopy a larr + arrayMap (\ix -> store (a ! (ix :: Ix 1)) 1) + retVoid -{- -- The type system prevents this. bad_alloc :: Def ('[] :-> Ref s (Stored Uint32)) bad_alloc = proc "bad_alloc" $ body $ do @@ -114,9 +114,9 @@ loopTest :: Def ('[Ref s ('Array 15 ('Stored Sint32))] ':-> ()) loopTest = proc "loopTest" $ \ arr -> body $ do - arrayMap (\ix -> store (arr ! (ix :: Ix 15)) 1) - times 3 (\ix -> store (arr ! (ix :: Ix 15)) 1) - for 0 (\ix -> store (arr ! (ix :: Ix 15)) 1) + arrayMap (\ix -> store (arr ! (ix :: Ix 15)) 1) + 2 `downTo` 0 $ (\ix -> store (arr ! (ix :: Ix 15)) 1) + 0 `upTo` 2 $ (\ix -> store (arr ! (ix :: Ix 15)) 1) retVoid testToIx :: Def ('[Sint32, Ref s ('Array 10 ('Stored Uint32))] ':-> Ref s ('Stored Uint32)) @@ -129,31 +129,11 @@ [ istruct [ i .= ival 10 ] ] --- DefProc (Proc {procSym = "foo", procRetTy = TyWord Word32, procArgs = [Typed --- {tType = TyRef (TyStruct "Foo"), tValue = VarName "var0"}], procBody = [ - --- Deref (TyWord Word32) (VarName "deref0") (ExpLabel (TyStruct "Foo") (ExpVar --- (VarName "var0")) "i") --- , Return (Typed {tType = TyWord Word32, tValue = ExpVar --- (VarName "deref0")}) --- ], procRequires = [], procEnsures = Nothing}) - -- uint32_t n_deref0 = *&n_var0->i; foo :: Def ('[Ref s ('Struct "Foo")] ':-> Uint32) foo = proc "foo" $ \str -> body $ do ret =<< deref (str ~> i) --- DefProc (Proc {procSym = "foo2", procRetTy = TyWord Word32, procArgs = [Typed --- {tType = TyRef (TyStruct "Foo"), tValue = VarName "var0"}], procBody = [ - --- Deref (TyWord Word32) (VarName "deref0") (ExpIndex (TyArr 10 (TyWord Word32)) --- (ExpLabel (TyStruct "Foo") (ExpVar (VarName "var0")) "p") (TyInt Int32) --- (ExpOp ExpMod [ExpLit (LitInteger 0),ExpLit (LitInteger 10)])) - --- ,Return (Typed --- {tType = TyWord Word32, tValue = ExpVar (VarName "deref0")})], procRequires = --- [], procEnsures = Nothing}) - -- uint32_t n_deref0 = *&n_var0->p[0 % 10]; foo2 :: Def ('[Ref s ('Struct "Foo")] ':-> Uint32) foo2 = proc "foo2" $ \str -> body $ do @@ -161,13 +141,24 @@ let x = arr ! (0 :: Ix 10) ret =<< deref x --deref (arr ! 0) --- foo3 :: Def ('[Ref s (Struct "Bar")] :-> Uint32) --- foo3 = proc "foo3" $ \str -> body $ do --- v <- deref (str ~> aa) --- ret =<< deref v - --------------------------------------------- +-- Testing matrices +mat1 :: Def ('[ConstRef s ('Array 1 ('Array 2 ('Stored Uint32)))] ':-> Uint32) +mat1 = proc "mat1" $ \arr -> body $ do + v <- deref (arr ! 1 ! 0) + ret v + +mat2 :: Def ('[] ':-> Uint32) +mat2 = proc "mat2" $ body $ do + arr <- local ((iarray [iarray [ival 0, ival 1]]) :: Init ('Array 1 ('Array 2 ('Stored Uint32)))) + arr2 <- local ((iarray [iarray [ival 3, ival 3]]) :: Init ('Array 1 ('Array 2 ('Stored Uint32)))) + v' <- assign arr + refCopy arr2 v' + refZero arr2 + v <- call mat1 (constRef arr) + ret v + cmodule :: Module cmodule = package "Alloc" $ do defStruct (Proxy :: Proxy "Foo") @@ -187,9 +178,11 @@ incl testToIx incl memcpy3 defMemArea arrayTest + incl mat1 + incl mat2 runAlloc :: IO () runAlloc = runCompiler [cmodule] [] initialOpts { outDir = Nothing } test2 :: String -test2 = showModule (compileModule cmodule) +test2 = showModule (compileModule Nothing cmodule) diff --git a/examples/ConcreteFile.hs b/examples/ConcreteFile.hs --- a/examples/ConcreteFile.hs +++ b/examples/ConcreteFile.hs @@ -1,10 +1,10 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE QuasiQuotes #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# OPTIONS_GHC -fno-warn-orphans -fno-warn-unused-binds -fno-warn-unused-matches #-} {-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-missing-signatures #-} @@ -18,13 +18,14 @@ module ConcreteFile where -import Ivory.Language -import Ivory.Stdlib -import Ivory.Compile.C.CmdlineFrontend +import Ivory.Compile.C.CmdlineFrontend +import Ivory.Language +import Ivory.Stdlib e :: IBool e = (4::Sint32) >? 3 +-- Currently, type synonyms can *only* be for base (non=stored) typed. type SomeInt = Uint32 macroStmts :: @@ -40,11 +41,10 @@ macroStmtsRet x y = do a <- local (ival 0) store a (x + y) - return =<< deref a + deref a macroExp :: IvoryOrd a => a -> a -> IBool -macroExp x y = do - x Uint32 -> Ix n toIx' ix = toIx (twosComplementCast ix) @@ -59,5 +59,3 @@ main :: IO () main = runCompiler [concreteIvory, examplesfile, stdlibStringModule] stdlibStringArtifacts initialOpts {outDir = Just "concrete-ivory", constFold = True} - - diff --git a/examples/file.ivory b/examples/file.ivory --- a/examples/file.ivory +++ b/examples/file.ivory @@ -1,13 +1,34 @@ -- # -*- mode: haskell -*- +-- For any imported header files, you can also provide paths, e.g., "foo/stdio.h". import (stdio.h, printf) int32_t printf(string x) import (stdio.h, printf) int32_t printf2(string x, int32_t y) include concreteIvory --for printf definitions in ConcreteFile.hs include stdlibStringModule --- extern foo.h G* uint8_t myptr +-- Define a struct. A base type is turned into a memory area by adding a +-- '&'. Note this is a type-level operator. Arrays and structs are always memory +-- areas. +struct Bar00 { + &int32_t aBar00; +} +-- Import global memory areas from `foo.h`. +import foo.h &int32_t *anArea1 +import foo.h &int32_t const *anArea2 +import foo.h int32_t[4] const anArea3[] + +-- Declare some global memory areas. They may be initizlied (otherwise, are initialized to zero). +&int32_t alloc *myArea1; +&int32_t const alloc *myArea2 = 3; +struct Bar00 alloc myArea3{} = { aBar00 = 3 }; +int32_t[3] alloc myArea4[] = {1,2,3}; +struct Bar00 alloc myArea5{}; +struct Bar00 const alloc myArea6{}; + +extern foo.h G* uint8_t myptr + -- A top level definition. bar = 3 + 2; @@ -16,20 +37,12 @@ -- (Both of the above can be done on Haskell and you can use antiquotation.) --- Define a struct. A base type is turned into a memory area by adding a --- '&'. Note this is a type-level operator. Arrays and structs are always memory --- areas. -struct Bar00 { - &int32_t aBar00; -} - struct Foo { -- When context makes apparent and we can syntactically check the type, a -- base type is promoted to a memory area (i.e., bool is rewritten to &bool). bool aFoo - -- '&' at the type level binds most tightly and is right-associative. When - -- we use a type alias, the '&' must be added explicitly. - ; &SomeInt[4] aBar + -- To use synonyms (`SomeInt`), you have to use Haskell syntax. + ; aBar :: Array 4 (Stored SomeInt) } -- Safe string structs: strings of max length 16 bytes Generates two field @@ -43,10 +56,10 @@ { struct Foo foo2f } -r* struct ivory_string_FooStr foostr(r* struct ivory_string_FooStr s) { +r* struct ivory_string_FooStr foostr(uint8_t i, r* struct ivory_string_FooStr s) { -- Allocate a new string dynamic string. Fails if the string is too large. alloc s0{} = $stringInit("foo"); - foostr(s0); + if (0>i) { foostr(i-1, s0); } else {} -- Store a new string into the dynamic string data structure. $string_lit_store("foos", s); return s; @@ -103,7 +116,6 @@ return *x + 4; } - -- Global allocation (G), stack allocation (S), and undetermined scope (var c) uint8_t foo12(* uint8_t a, G*uint8_t b, * uint8_t c, S* uint8_t d) { store b as *a; @@ -261,7 +273,7 @@ } void fizzbuzzUpFrom() { - upFromTo 50 100 ix { + upFromTo (50, 100) ix { -- for typechecking let (ix_t 101) ix' = ix; let i = fromIx(ix); @@ -299,7 +311,7 @@ } void fizzbuzzDownFromTo() { - downFromTo 100 50 ix { + downFromTo (100, 50) ix { -- for typechecking let (ix_t 101) ix' = ix; let i = fromIx(ix); @@ -388,4 +400,30 @@ , const * struct ivory_string_Astr s ) { $sz_from_istr(arr, s); +} + +int16_t return_negative() { return -32767; } +int16_t return_negative2() { return -32768; } + +struct x { + int32_t a; + int32_t b; +} + +void test() { + alloc myref{}; + $refZero (myref); + store myref.a as 1; +} + +-- A 3 dimensional matrix declaration +struct X +{ + float[3][4][5] matrix; +} + +void myfunc(* struct X myx) +{ + let m = myx.matrix; + store m@2@3@4 as 0.0; } diff --git a/ivory-examples.cabal b/ivory-examples.cabal --- a/ivory-examples.cabal +++ b/ivory-examples.cabal @@ -1,12 +1,12 @@ name: ivory-examples -version: 0.1.0.3.1 +version: 0.1.0.4 author: Galois, Inc maintainer: trevor@galois.com, leepike@galois.com copyright: 2013 Galois, Inc. category: Language synopsis: Ivory examples. description: Various examples demonstrating the use of Ivory. -homepage: http://smaccmpilot.org/languages/ivory-introduction.html +homepage: http://ivorylang.org/ build-type: Simple cabal-version: >= 1.10 license: BSD3 @@ -15,7 +15,7 @@ source-repository this type: git location: https://github.com/GaloisInc/ivory - tag: hackage-examples-0103 + tag: hackage-examples-0.1.0.4 executable ivory-c-clang-test main-is: TestExamples.hs