Skip to content

Commit

Permalink
[ refactor, performance ] much faster C pointers (#35)
Browse files Browse the repository at this point in the history
* [ refactor, performance ] much faster C pointers

* [ lint ] use clang format
  • Loading branch information
stefan-hoeck authored Sep 20, 2024
1 parent 287d0b2 commit 155e90c
Show file tree
Hide file tree
Showing 10 changed files with 316 additions and 14 deletions.
2 changes: 1 addition & 1 deletion codegen/integer.c
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ void *stype(char *name, size_t sz) {

void *tsize(char *name, size_t sz) {
printf("\npublic export %%inline\n");
printf("%sSize : Nat\n", name);
printf("%sSize : Bits32\n", name);
printf("%sSize = %zd\n", name, sz);
}

Expand Down
1 change: 1 addition & 0 deletions cptr.ipkg
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ depends = base >= 0.6.0
, array

modules = Data.C.Array
, Data.C.Array8
, Data.C.Deref
, Data.C.Integer
, Data.C.Ptr
Expand Down
6 changes: 6 additions & 0 deletions pack.toml
Original file line number Diff line number Diff line change
Expand Up @@ -19,3 +19,9 @@ type = "git"
url = "https://github.com/stefan-hoeck/idris2-ref1"
commit = "latest:main"
ipkg = "ref1.ipkg"

[custom.all.profiler]
type = "git"
url = "https://github.com/stefan-hoeck/idris2-profiler"
commit = "latest:main"
ipkg = "profiler.ipkg"
9 changes: 9 additions & 0 deletions profile/src/Main.idr
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ module Main
import Data.Buffer.Indexed
import Data.Array
import Data.C.Ptr
import Data.C.Array8 as A8
import Profile

%default total
Expand All @@ -16,6 +17,9 @@ sumEmptyBuffer n = foldr (\x,y => cast x + y) 0 (Buffer.Indexed.fill n 1)
sumEmptyCptr : Nat -> Bits32
sumEmptyCptr n = withCArray {a = Bits32} n $ \r => withIArray r (foldr (+) 0)

sumEmptyArray8 : Nat -> Bits32
sumEmptyArray8 n = A8.withCArray n $ \r => A8.withIArray r (foldr (\x,y => cast x + y) 0)

bench : Benchmark Void
bench = Group "ref1"
[ Group "sum IArray"
Expand All @@ -33,6 +37,11 @@ bench = Group "ref1"
, Single "1000" (basic sumEmptyCptr 1000)
, Single "1000000" (basic sumEmptyCptr 1000000)
]
, Group "sum CArray8"
[ Single "1" (basic sumEmptyArray8 1)
, Single "1000" (basic sumEmptyArray8 1000)
, Single "1000000" (basic sumEmptyArray8 1000000)
]
]

main : IO ()
Expand Down
19 changes: 11 additions & 8 deletions src/Data/C/Array.idr
Original file line number Diff line number Diff line change
Expand Up @@ -18,16 +18,19 @@ import Syntax.T1
--------------------------------------------------------------------------------

export %foreign "C:cptr_malloc, cptr-idris"
"scheme,chez:(lambda (x) (if (= 0 x) 0 (foreign-alloc x)))"
prim__malloc : (size : Bits32) -> AnyPtr

export %foreign "C:cptr_calloc, cptr-idris"
prim__calloc : (n, size : Bits32) -> AnyPtr

export %foreign "C:cptr_free, cptr-idris"
"scheme,chez:(lambda (x) (if (= 0 x) '() (foreign-free x)))"
prim__free : AnyPtr -> PrimIO ()

export %foreign "C:cptr_inc_ptr, cptr-idris"
prim__inc_ptr : AnyPtr -> Bits32 -> AnyPtr
"scheme,chez:(lambda (p x y) (+ p (* x y)))"
prim__inc_ptr : AnyPtr -> Bits32 -> Bits32 -> AnyPtr

--------------------------------------------------------------------------------
-- Immutable API
Expand Down Expand Up @@ -59,7 +62,7 @@ parameters {0 a : Type}
export %inline
at : CIArray n a -> Fin n -> a
at r x =
let MkIORes v _ := toPrim (deref $ prim__inc_ptr r.ptr $ cast $ cast x * sizeof a) %MkWorld
let MkIORes v _ := toPrim (deref $ prim__inc_ptr r.ptr (sizeof a) (cast $ finToNat x)) %MkWorld
in v

export %inline
Expand Down Expand Up @@ -208,13 +211,13 @@ parameters {auto has : HasIO io}
||| Allocates a new C-pointer of `sizeof a * n` bytes.
export %inline
malloc : (0 a : Type) -> SizeOf a => (n : Nat) -> io (CArrayIO n a)
malloc a n = primIO $ MkIORes (CA $ prim__malloc (cast $ n * sizeof a))
malloc a n = primIO $ MkIORes (CA $ prim__malloc (cast n * sizeof a))

||| Like `malloc` but resets all allocated bytes to zero.
export %inline
calloc : (0 a : Type) -> SizeOf a => (n : Nat) -> io (CArrayIO n a)
calloc a n =
primIO $ MkIORes (CA $ prim__calloc (cast n) (cast $ sizeof a))
primIO $ MkIORes (CA $ prim__calloc (cast n) (sizeof a))

||| Frees the memory allocated for a C-array.
|||
Expand Down Expand Up @@ -243,7 +246,7 @@ malloc1 :
-> (1 t : T1 rs)
-> A1 rs (CArray n a)
malloc1 a n t =
let p := prim__malloc (cast $ n * sizeof a)
let p := prim__malloc (cast n * sizeof a)
in A (CA p) (unsafeBind t)

||| Like `malloc1` but resets all allocated bytes to zero.
Expand All @@ -255,7 +258,7 @@ calloc1 :
-> (1 t : T1 rs)
-> A1 rs (CArray n a)
calloc1 a n t =
let p := prim__calloc (cast n) (cast $ sizeof a)
let p := prim__calloc (cast n) (sizeof a)
in A (CA p) (unsafeBind t)

||| Frees the memory allocated for a C pointer and removes it from the
Expand All @@ -281,7 +284,7 @@ parameters {0 a : Type}
||| Reads a value from a C-pointer at the given position.
export %inline
get : Deref a => Fin n -> F1 rs a
get x = ffi $ toPrim (deref $ prim__inc_ptr r.ptr $ cast $ cast x * sizeof a)
get x = ffi $ toPrim (deref $ prim__inc_ptr r.ptr (cast $ finToNat x) (sizeof a))

||| Reads a value from a C-pointer at the given position.
export %inline
Expand All @@ -296,7 +299,7 @@ parameters {0 a : Type}
||| Writes a value to a C pointer at the given position.
export %inline
set : SetPtr a => Fin n -> a -> F1' rs
set x v = ffi $ toPrim (setPtr (prim__inc_ptr r.ptr $ cast $ cast x * sizeof a) v)
set x v = ffi $ toPrim (setPtr (prim__inc_ptr r.ptr (cast $ finToNat x) (sizeof a)) v)

||| Writes a value to a C pointer at the given position.
export %inline
Expand Down
Loading

0 comments on commit 155e90c

Please sign in to comment.