ivory-examples 0.1.0.3 → 0.1.0.3.1
raw patch · 2 files changed
+393/−1 lines, 2 files
Files
- examples/file.ivory +391/−0
- ivory-examples.cabal +2/−1
+ examples/file.ivory view
@@ -0,0 +1,391 @@+-- # -*- mode: haskell -*-++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++-- A top level definition.+bar = 3 + 2;++-- Define a top-level type alias.+type Boo = int8_t;++-- (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+ }++-- Safe string structs: strings of max length 16 bytes Generates two field+-- labels: stringLengthL (int32_t) and stringDataL (array uint8_t[4]). The type+-- of the struct is ivory_string_FooStr. See the String library in ivory-stdlib+-- for some string library functions.+string struct FooStr 4++-- Nested struct references+struct Foo2+ { struct Foo foo2f+ }++r* struct ivory_string_FooStr foostr(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);+ -- Store a new string into the dynamic string data structure.+ $string_lit_store("foos", s);+ return s;+}++-- Declaring abstract structs+-- abstract struct fooStruct "foobar/foo.h"++-- Struct declared with C-like types+struct Goo+ { int32_t aGoo;+ bool bGoo;+ int32_t[4] cGoo;+ }++-- Use the expression and alias+Boo foo(Boo x) {+ return (bar + x);+}++-- Calling builtin functions+void foo67(* float a)+{ store a as sin(*a);+}++-- if-the-else blocks. Braces are mandatory.+int32_t foo1() {+ if (true) {+ let a = 5;+ return a;+ }+ else {+ let b = 3;+ return b + 3;+ }+}++-- Empty statements in if-then-else+void foo30(Boo x) {+ if(true) {}+ else { return; }+ return;+}++-- Using an external symbol. Don't run this, unless the header is in-scope.+-- uint8_t foo31() {+-- return (3 + *myptr);+-- }++-- Allocation on the stack (dereference is an expression)+int32_t foo0() {+ alloc *x = 3;+ store x as 4;+ 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;+ return *b + *c + *d;+}++-- Allocated on either the stack or globally, with user-provided type-variable (xx).+xx* uint32_t foo14(xx* struct Foo f) {+ let a = f . aBar;+ let u = a @ 2;+ return u;+}++-- Allocate an array and index into it. A precondition is given for the function+-- argument.+uint32_t foo6(v *uint32_t[3] arr0) {+ alloc arr1[] = {1,2,3};+ map ix {+ store arr0 @ ix as *arr1 @ ix;+ }+ -- Same as *arr0 @ 1 ;+ return arr0[1] ;+}+{ pre(arr0[1] > 0);+}++-- Use a struct. Polymorphic region reference.+void foo00(* int32_t[5] arr, * struct Bar00 str) {+ -- The following two are equivalent+ store arr @ 2 as 3;+ store arr @ 2 as 4;+ -- As well as the next two+ store str.aBar00 as 1;+ store str.aBar00 as 2;++ store arr@2 as arr[3];+}++-- Boolean operators+uint32_t foo7(bool b, uint32_t a) {+ return (b && !b ? a+3 : signum(abs(a)) - 4);+}++void foo2() {return;}++-- Function calls, with a return value and without.+uint32_t foo8(bool b, uint32_t a) {+ foo2();+ let x = foo7(b, a);+ foo7 (b, a);+ return (b && !b ? a+3 : signum(abs(a)) - x);+}++-- Local assignment (constant).+uint32_t foo9(uint32_t a) {+ forever {+ let b = a + 3;+ return b;+ }+ return 0;+}++-- Memcopy.+void foo10(*uint32_t[3] r0, *uint32_t[3] r1) {+ memcpy r0 r1;+}++-- Const decorators.+uint32_t foo11(const *uint32_t i) {+ return *i;+}++-- Pre and post conditions.+uint32_t foo15(uint32_t a, * struct Foo f, * struct Foo g) {+ return a;+}+{ pre(a < 4);+ pre(a > 0);+ post(return > 5);+ pre(* f . aFoo && * g . aFoo);+}++-- Stack allocated variable.+uint32_t foo16(S*uint32_t i) {+ return *i;+}+{ pre(*i > 3); }++-- Global allocated variable.+uint32_t foo17(G*uint32_t i) {+ return *i;+}++-- allocate and initialize a struct.+void foo92() {+ alloc s{} = {aFoo = true};+ return;+}++-- Mapping over an array+void mapProc(*uint8_t[4] arr, uint8_t x) {+ map ix {+ let v = arr @ ix;+ store v as *v + x;+ }+}++-- Casting+void foo57(* uint8_t a, * uint16_t b, * int8_t c, * int32_t d)+{+ store b as safeCast(*a); -- can always safely cast+ store b as castWith(3, *d); -- cast with a default value if out of range+ store c as twosCompCast(*a); -- interpret under 2s compliment+}++-- Statements and expression macros+int32_t foo68(int32_t x, int32_t y) {+ -- macroStmts is a Haskell function+ $macroStmts(x, y);+ -- with a return value (Ivory eff a)+ a <- $macroStmtsRet(x, y);+ -- macroExp is a Haskell function, too+ if($macroExp(x, y)) { return x; }+ else { return a; }+}++int32_t foo100(int32_t x) {+ return x;+}++-- Calling functions (with return values) as expressions+int32_t bar82() {+ let y = foo100(4);+ return foo100(foo100(y));+}++-- Fizzbuzz four ways+void fizzbuzzUp() {+ upTo 100 ix {+ -- for typechecking+ let (ix_t 101) ix' = ix;+ let i = fromIx(ix);+ if (i % 15 == 0) {+ printf("Fizzbuzz");+ } else {+ if (i % 5 == 0) {+ printf("Fizz");+ } else {+ if (i % 3 == 0) {+ printf("Buzz");+ } else { printf2("%i\n",i); }+ }+ }+ }+}++void fizzbuzzUpFrom() {+ upFromTo 50 100 ix {+ -- for typechecking+ let (ix_t 101) ix' = ix;+ let i = fromIx(ix);+ if (i % 15 == 0) {+ printf("Fizzbuzz");+ } else {+ if (i % 5 == 0) {+ printf("Fizz");+ } else {+ if (i % 3 == 0) {+ printf("Buzz");+ } else { printf2("%i\n",i); }+ }+ }+ }+}++void fizzbuzzDown() {+ downFrom 100 ix {+ -- for typechecking+ let (ix_t 101) ix' = ix;+ let i = fromIx(ix);+ if (i % 15 == 0) {+ printf("Fizzbuzz");+ } else {+ if (i % 5 == 0) {+ printf("Fizz");+ } else {+ if (i % 3 == 0) {+ printf("Buzz");+ } else { printf2("%i\n",i); }+ }+ }+ }+}++void fizzbuzzDownFromTo() {+ downFromTo 100 50 ix {+ -- for typechecking+ let (ix_t 101) ix' = ix;+ let i = fromIx(ix);+ if (i % 15 == 0) {+ printf("Fizzbuzz");+ } else {+ if (i % 5 == 0) {+ printf("Fizz");+ } else {+ if (i % 3 == 0) {+ printf("Buzz");+ } else { printf2("%i\n",i); }+ }+ }+ }+}++------------------------------------------------------------+-- Larger example (hypothetical pack and unpack functions). In practice, use+-- ivory-serialize.+int32_t unpackSint32(uint8_t a, uint8_t b, uint8_t c, uint8_t d)+{+ alloc *x = 0;+ store x as safeCast(a) | safeCast(b) << 0x8 | safeCast(c) << 0x10 | safeCast(d) << 0x18;+ return twosCompCast(*x);+}++int32_t unpack(* uint8_t[10] msg, int32_t ixx)+{+ let ix = toIx(ixx);+ let res = unpackSint32( * msg @ ix+ , * msg @ (ix+1)+ , * msg @ (ix+2)+ , * msg @ (ix+3)+ );+ return res;+}++void pack(*uint8_t[10] msg, int32_t x, int32_t ixx)+{+ let ix = toIx(ixx);+ let ux = twosCompRep(x);+ store msg @ ix as bitCast(ux);+ store msg @ (ix+1) as bitCast(ux >> 0x08);+ store msg @ (ix+2) as bitCast(ux >> 0x10);+ store msg @ (ix+3) as bitCast(ux >> 0x18);+}++struct Foo7 { struct ivory_string_FooStr aFoo7; }++struct Bar2 { int32_t aBar7; }++struct Boo { struct Bar2 aBoo; }++void foobar (* struct Foo7 s) {+ store (s . aFoo7 . stringDataL@0) as 3;+ return;+}++int32_t bar72(int32_t x, * struct Boo a, * int32_t y, * int32_t[10] arr) {+ store (a . aBoo) . aBar7 as *y;+ store (a . aBoo) . aBar7 as *y;+ store arr@toIx(*y + *y) as *y + *y;+ return a.aBoo->aBar7;+}++float tanFuncD(float x) {+ return atan2(3.0, 1);+}++float tanFuncF(float x) {+ return atan2(3.0, 1);+}++string struct Astr 4++-- copy from an uint8_t array to a string+void arr_to_str( * struct ivory_string_Astr s+ , const * uint8_t[5] arr+ ) {+ $istr_from_sz(s, arr);+}++-- copy to an uint8_t array from a string+void str_to_arr(* uint8_t[5] arr+ , const * struct ivory_string_Astr s+ ) {+ $sz_from_istr(arr, s);+}
ivory-examples.cabal view
@@ -1,5 +1,5 @@ name: ivory-examples-version: 0.1.0.3+version: 0.1.0.3.1 author: Galois, Inc maintainer: trevor@galois.com, leepike@galois.com copyright: 2013 Galois, Inc.@@ -11,6 +11,7 @@ cabal-version: >= 1.10 license: BSD3 license-file: LICENSE+data-files: examples/file.ivory source-repository this type: git location: https://github.com/GaloisInc/ivory