With inlining of calls, there is a bug caused by a clash in formal parameters of the inlined procedure. Fix: alpha rename the formal parameters of an inlined procedures to fresh variable names.

This example comes from the ivory-tutorial exercises. Attempting to model check potion usage.

[ivory|

struct Character
  { hp     :: Stored Uint16
  ; max_hp :: Stored Uint16
  ; mp     :: Stored Uint16
  ; max_mp :: Stored Uint16
  ; potions:: Stored Uint8
  }

void use_potion(*struct Character c) {
  let ps = *c.potions;

  if (ps > 0) {
    -- decrement the number of available potions
    store c.potions as (ps - 1);

    -- increase mp up to the maximum
    let mp_val = *c.mp;
    let mp_max = *c.max_mp;
    if ((mp_val + 25) < mp_max) {
      store c.mp as (mp_val + 25);
    } else {
      store c.mp as mp_max;
    }
  } else {}
}
|]

potions_available ref =
  checkStored (ref ~> potions) $ \ potions_val ->
    1 <=? potions_val

check_potion_use :: Def ('[Ref s ('Struct "Character")] ':-> ())
check_potion_use =
  proc "check_potion_use" $ \ ref ->
  requires (potions_available ref) $
  body $ do
    old_potions <- deref (ref ~> potions)
    call_ use_potion ref
    new_potions <- deref (ref ~> potions)
    assert (old_potions >? new_potions)

We're getting this error message with the 1.5 developer snapshot and the 1.4 release of cvc4:

Unsafe ["QUERY deref1 > mc_1deref2 ;\t % [ No location available ];"]

We also turned on Inlining for this example because use_potion needs to be inlined.

@elliottt, @leepike thinks this may be related to the fresh name generation with inlining.

We currently have SafeCast instances for Sint32 -> IFloat and Sint64 -> IDouble, but these casts don't preserve the value of the original expression for all inputs, because the input has more bits of precision than the mantissa of the output.

I think we should add a FloatCast class, which allows casts that lose precision while preserving approximate magnitude. That should have Sint32 -> IFloat, Sint64 -> IFloat, and Sint64 -> IDouble casts. Casts from smaller integer types can stay in the SafeCast class.

The generated AST for deref statements discards information about whether the reference on the right-hand side was const or not.

That isn't wrong, since deref is safe for both const and non-const refs.

But it means that CSE can't insert temporary variables for subexpressions that keep constness identical to the original types.

Which again, isn't wrong. As long as CSE assumes all subexpressions on the RHS of a dereference are const, any temporary assignments can only add const to a pointer, not remove it. So this respects C semantics and remains safe.

But if a non-const ref is used in both a dereference (treated as const) and a store (treated as non-const), then this strategy means CSE will emit two sets of temporary variables for the same subexpression used at two types which differ only in constness.

That's annoying, as it makes the generated code bigger, but otherwise harmless. Still, it would be nice to fix someday.

Lee suggests this is part of a larger refactoring to do someday, where more type information should be carried around in the AST, saying the current approach is "not such a good idea for issues like this, and even just that in AST traversals, the reference type must be reconstructed." But we agree that fixing that is a big change for the amount of benefit it would provide.

Ubuntu 14.04 LTS 32 bit. GHC 7.6.3. Cabal 1.20.0.3.

Looks like the solution is to be inside a Cabal sandbox, otherwise packages collide. The README.md says "we recommend using a cabal sandbox" but maybe it should be worded more strongly than that? :-)

installing 'ivory' with cabal works w/out a sandbox:
...Creating package registration file: /tmp/pkgConf-ivory-0.1.06558.0
Installing library in
/home/x/.cabal/lib/i386-linux-ghc-7.6.3/ivory-0.1.0.0
Registering ivory-0.1.0.0...
Installed ivory-0.1.0.0

but then 'ivory-backend-c' fails:
~/Dev/Ivory/test$ cabal install ivory-backend-c
Resolving dependencies...
In order, the following would be installed:
dlist-0.7.1 (new package)
exception-transformers-0.3.0.4 (new package)
exception-mtl-0.3.0.5 (new package)
fgl-5.5.0.1 (new package)
safe-0.3.8 (new package)
split-0.2.2 (new package)
srcloc-0.4.1 (new package)
syb-0.4.2 (new package)
cmdlib-0.3.5 (new package)
symbol-0.2.4 (new package)
text-1.1.1.3 (latest: 1.2.0.3) (new version)
mainland-pretty-0.2.7 (new package)
parsec-3.1.7 (reinstall) changes: text-1.2.0.3 -> 1.1.1.3
ivory-0.1.0.0 (reinstall)
ivory-opts-0.1.0.1 (new package)
polyparse-1.10 (new package)
cpphs-1.18.6 (new package)
haskell-src-exts-1.16.0.1 (new package)
th-expand-syns-0.3.0.4 (new package)
th-reify-many-0.1.2 (new package)
th-orphans-0.8.2 (new package)
haskell-src-meta-0.6.0.8 (new package)
language-c-quote-0.10.1.3 (new package)
ivory-backend-c-0.1.0.1 (new package)
cabal: The following packages are likely to be broken by the reinstalls:
network-uri-2.6.0.1
HTTP-4000.2.18
Use --force-reinstalls if you want to install anyway.

The cmdlib library is way too complicated for what we need, let's just write a simpler option parser.

It would be nice to be able to replace the ivory_assert define with some custom functionality. For example at the moment we print the assert message to a serial console and sit flashing a led.

As far as I can tell this change could be as simple as checking if ivory_assert is already defined in ivory_asserts.h.

According Function implementiation at http://smaccmpilot.org/languages/ivory-cheatsheet.html

func2 :: Def ('[Ref s (Stored Uint32), Uint32] :-> ())
func2 = proc "func0" $ \ref val -> body $ do
  store ref val
  retVoid

generates

uint32_t func2(uint32_t *ref, uint32_t val) {
  *ref = val;
}

There seem to be two copy&paste-errors here:

1. func2 instead of func0 in proc naming:

func2 :: Def ('[Ref s (Stored Uint32), Uint32] :-> ())
func2 = proc "func2" $ \ref val -> body $ do
  store ref val
  retVoid

1. Return type of C function should be void instead of uint32_t, and a return; is generated when compiling

void func2(uint32_t *ref, uint32_t val) {
  *ref = val;
  return;
}

Currently there's no warning that the user (accidentally) created modules or artifacts of the same name - whichever one gets written to disk last (which is arbitrary) "wins". This doesn't come up a lot in practice but when it does, it sure can be difficult to debug!

see build failure here. will work on a smaller test case when i have some spare time
https://travis-ci.org/GaloisInc/smaccmpilot-stm32f4/jobs/66928694

as seen in:
GaloisInc/ivory-tower-stm32@d184306
an innocent typo led to an incorrect register definition.

It seems like the bitdata quasiquoter should have been able to check that the register was declared at 32 bits wide but only defined 31 bits. It should throw some sort of error rather than pad it out implicitly - we have an explicit way to pad things out.

I have been using Ivory on Stack and, while the build has been working just fine, I find I am unable to get to a REPL with 'stack ghci'.

I brought this issue up with some Stack developers and was told I should bring it up here. My stack.yaml is:

flags: {}
packages:
- ivory-stdlib/
- ivory-model-check/
- ivory-opts/
- ivory-examples/
- ivory-backend-acl2/
- ivory-serialize/
- ivory/
- ivory-hw/
- ivory-eval/
- ivory-backend-c/
- ivory-quickcheck/
- ivory-artifact/
extra-deps:
- acl2-0.0.1
- ghc-srcspan-plugin-0.2.1.0
resolver: lts-2.21

and I have been running 'stack test' and 'stack ghci'. The latter eventually fails with:

There were multiple candidates for the Cabal entry "Test.hs(/home/hodapp/source/ivory/ivory-examples/examples/Test.hs), pi
cking /home/hodapp/source/ivory/ivory-model-check/test/Test.hs
Configuring GHCi with the following packages: ivory-artifact, ivory-backend-acl2, ivory-backend-c, ivory-eval, ivory-examp
les, ivory-hw, ivory-model-check, ivory-opts, ivory-quickcheck, ivory-serialize, ivory-stdlib, ivory
GHCi, version 7.8.4: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer-gmp ... linking ... done.
Loading package base ... linking ... done.
Loading package array-0.5.0.0 ... linking ... done.
Loading package deepseq-1.3.0.2 ... linking ... done.
Loading package containers-0.5.5.1 ... linking ... done.
Loading package bytestring-0.10.4.0 ... linking ... done.
Loading package filepath-1.3.0.2 ... linking ... done.
... (removed a bunch of lines) ...
Loading package acl2-0.0.1 ... linking ... done.
Loading package monadLib-3.7.3 ... linking ... done.
Loading package blaze-builder-0.4.0.1 ... linking ... done.
Loading package unordered-containers-0.2.5.1 ... linking ... done.
Loading package semigroups-0.16.2.2 ... linking ... done.
Loading package void-0.7 ... linking ... done.
Loading package HStringTemplate-0.8.3 ... linking ... done.
Loading package utf8-string-1 ... linking ... done.
Warning: ignoring unrecognised input `/home/hodapp/source/ivory/ivory/src/Ivory/Language/Syntax/Concrete/Lexer.x'
Warning: ignoring unrecognised input `/home/hodapp/source/ivory/ivory/src/Ivory/Language/Syntax/Concrete/Parser.y'

/home/hodapp/source/ivory/ivory/src/Ivory/Language/Syntax/Concrete/QQ.hs:45:8:
    Could not find module ‘Ivory.Language.Syntax.Concrete.Lexer’
    It is a member of the hidden package ‘ivory-0.1.0.2’.
    Use -v to see a list of the files searched for.

/home/hodapp/source/ivory/ivory/src/Ivory/Language/Syntax/Concrete/QQ.hs:46:18:
    Could not find module ‘Ivory.Language.Syntax.Concrete.Parser’
    It is a member of the hidden package ‘ivory-0.1.0.2’.
    Use -v to see a list of the files searched for.
Failed, modules loaded: none.
Prelude> 

And if I try to import Ivory.Language:

Prelude> import Ivory.Language

<no location info>:
    Could not find module ‘Ivory.Language’
    It is a member of the hidden package ‘ivory-0.1.0.2’.

This is a pretty minor issue (I can still just run a REPL in the cabal sandbox), and I may look into it myself, but I figured I would post it here in case anyone can shed some light on the problem.

Forgive my naivety, from the description at http://ivorylang.org/ivory-libs.html it seems that writing to registers in ivory only works for the STM32F4?

Memory bounds are defined statically in Ivory.HW.STM32F4 according to the STM32F4 microcontroller memory map

I'd like to use ivory for a project with the teensy++ (AT90USB1286). What work needs to be done before this is a possibility?

There's not currently a way to enforce that code paths terminate in a use of ret or retVoid in a proc. It's not clear if there's a way to do this, but a good example of the problem is this:

test = proc "test" $ body $ (ifte_ false (ret true) (return ()))

This will typecheck and generate code, though the generated C will include a path that would return no value, and generate a warning.

My apologies for cross posting to an issues register. I am looking for the correct forum in which to ask questions. In particular I what seems should be a simple misunderstanding. I'd appreciate someone in the know giving this a read: http://stackoverflow.com/questions/33459506/ivory-how-to-use-the-ivory-hw-package

There has been a feature request by an Ivory user to allow areas (structs in particular) to contain global references that can be dereferenced. Of course, already you can have, e.g.,

[ivory|
struct Foo42
  { i42 :: Stored (Ref Global (Stored Uint32))
  }
|]

but you can't dereference or store the Uint32 because of the IvoryStore constraint on deref and store.

What about adding an instance

instance IvoryVar a => IvoryStore (Ref 'Global ('Stored a))

Is this safe?

We can declare an opaque struct type, but for something like C's FILE *, we need to be able to pull in the type FILE without any qualifiers like struct.

Pat proposes, and this sounds good to me, that we add another Area kind or something for opaque typedefs. The declaration should indicate which header file the type comes from.

I write following code:

https://github.com/fpiot/arduino-ivory/blob/531329db24cc67f423c211d0fdfa1b52ee6eb000/demo/01_blink/MainIvory.hsb

And I believe it create following C code:

int main () {
    init();
    delay(500);
    return 0;
}

How ever it causes following error:

$ runhaskell MainIvory.hs

*** Procedure MainIvory
    ERROR: [ No location available ]:
             Unbound value: 'init'
    ERROR: [ No location available ]:
             Unbound value: 'delay'
MainIvory.hs: Sanity-check failed!

How to fix it?

The backend is changed (commit 02ef9f5) to declare structs with the form

typedef struct foo { ... } foo;

for compatibility issues with a particular target.

It might be nice to add a sanity check to ensure the same symbol isn't used for a struct typedef and a global variable, eventually resulting in a C compilation error.

HI! We faced 'unused variables' warnings with -Wall. The source of the problem is the following definitions in ivory_asserts.h:

#else /* IVORY_TEST */

#define REQUIRES(arg)
#define ENSURES(arg)
#define ASSUMES(arg)
#define ASSERTS(arg)
#define COMPILER_ASSERTS(arg)

#endif /* IVORY_TEST */

Next is an example of generated code which emits warnings:

    int32_t n_cse1 = (int32_t) -(int32_t) 1;
    COMPILER_ASSERTS((bool) ((bool) ((int32_t) 0 < (int32_t) 1024) && (bool) (n_cse1 <= (int32_t) 0)));

Here, the n_cse1 variable is only used in COMPILER_ASSERT, which maps its argument to nothing in the default case.

Add QC backend for C values and esp. structs.

I'd like to propose adding an opaque type to Ivory. The type represents an uninterpreted, unimplementable, type constant. The use-case is as follows: suppose I have some complex type defined in C. Suppose that foo.h delcares:

typedef struct { ... } complex_t;

complex_t com;

void bar(complex_t *com, ...);

and in an Ivory program, I want to define

com :: MemArea XXX
com  importArea "com" "foo.h"

bar :: Def ('[Ref Global XXX, ...] :-> ())
bar = importProc "bar" "foo.h"

and I am calling bar with a pointer to a com argument defined elsewhere in my Ivory program. What do I replace XXX with? I could teach Ivory about the complex_t type, but in this case, Ivory doesn't use the type, so it's unnecessary and onerous. I could define a "proxy" type, e.g., Uint32, and everything works out, since Ivory does not check that the type of Ivory's bar function corresponds to the C type of bar.

But the user should have more information that the type is never used and does not correspond to the prototype from the header file.

I propose adding an OpaqueType to Ivory that addresses this. No backend should implement OpaqueType, but it can be used as a proxy in these circumstances.

I've added this functionality to commit 54aaf68. If this looks reasonable, then I'll merge it, otherwise, is there a better way to solve the problem?

The symbolic simulator currently assumes there is no aliasing of formal parameters. But there can be aliasing, e.g.,

call foo x x

where x is a reference. Aliasing should not be assumed.

It appears that the assertions are insufficiently-restrictive. E.g., the assertion here uses <=? rather than <?. Double-check that the index + size < remaining pack length.

To some extent, you can write Haskell functions that operate over refs without caring whether they're const or not. You just need the ref type to be an instance of IvoryRef. But the (!) and (~>) operators are more picky than that, requiring that both the argument ref and the resulting ref be instances of IvoryExpr. And that means that a const-generic function's class constraints need to include IvoryExpr instances for every struct, field, array, and array element type used in the function.

In discussing this with Trevor, the best option we came up with was to switch to capturing constness in a phantom type variable, something like so:

data Constness = Const | Mutable
data Ref' (c :: Constness) (s :: RefScope) (a :: Area *) = Ref' { getRef :: I.Expr }
type Ref = Ref' Mutable
type ConstRef = Ref' Const

(The two type aliases are to limit the number of changes required in existing code.)

A single instance for IvoryVar and IvoryExpr then covers all two varieties of Ref'. (I'm not sure whether IvoryType needs one or two instances.)

Code that doesn't care about constness (because it only derefs, it doesn't store) can take a Ref' c s area and just not constrain c.

I found a bug in Ivory codegen where it can produce invalid C. It has to do with generating a cast of type array- the C comes out something like:

float[4U] a;
float[4U] b;
float* n_letX = (float[4U]) (p ? a : b)

the cast to float[4U] in the final line is not valid C. It should be a cast to float*. Both our arm-none-eabi-gcc cross compiler and clang agree this is an error.

One small test case I found was when using a ternary operator and assign:

arrayTernary :: Def('[IBool] :-> IFloat)
arrayTernary = proc "arrayTernary" $ \b -> body $ do
  a1 <- local (vs 1)
  a2 <- local (vs 2)
  ares <- assign (b ? (a1, a2))
  deref (ares ! 3) >>= ret
  where
  vs ::  IFloat -> Init (Array 4 (Stored IFloat))
  vs v = iarray (map ival [v, v, v, v])

I have not done a lot of investigation to get this test case smaller - there may be other places where a similar cast happens.

I hit this bug in the wild working on the copter motors code. Its the first time I've hit an Ivory bug in a really long time!

Pat

When one writes string literal in Haskell it may go into Ivory as IString. Then IString compiles into string literal and its type to char *. So one can pass string literal to a C function taking char * and mutating its argument, which leads to segmentation fault.

Code to reproduce

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators     #-}

import qualified Ivory.Compile.C.CmdlineFrontend as C
import           Ivory.Language

nullifyString2 :: Def ('[IString] ':-> ())
nullifyString2 = importProc "nullifyString2" "nullifyString2.h"

nullifyString :: Def ('[IString] ':-> ())
nullifyString = proc "nullifyString" $ \s -> body $ do
    call_ nullifyString2 s

cmain :: Def ('[] ':-> Sint32)
cmain = proc "main" $ body $ do
    call_ nullifyString "hello"
    ret 0

ivoryStringIssue :: Module
ivoryStringIssue = package "gen-ivory-string-issue" $ do
    incl nullifyString2
    incl nullifyString
    incl cmain

main :: IO ()
main = C.compile [ivoryStringIssue] []

// nullifyString2.h
void nullifyString2(char *s) {
    s[0] = 0;
}

I found this when tried to cast puts :: Def ('[IString] ':-> Sint32) to int puts(const char *s).

I don't know cabal, but it seems odd to me that while I'm trying to 'cabal install ivory-backend-c' it runs into missing things: I had to manually 'cabal install happy', then it got a little further, but now i apparently have to manually 'cabal install alex' as well... heaven only knows what next.

I would have guessed/assumed/hoped that the whole point of a packaging system would include support for dependencies to be automaticaly pulled in if need be.

Or barring that it would be nice if it said up front that I needed to manually install some other things, rather than me having to keep redoing the instal only to find the next block.

ivory-examples/examples/Extern.hs appears to be broken; 'runExtern' produces the following error:

*** Procedure Extern
    ERROR: [ No location available ]:
             Unbound value: 'putchar'
    ERROR: [ No location available ]:
             Unbound value: 'SOME_CONST'
    ERROR: [ No location available ]:
             Unbound value: 'putchar'
*** Exception: Sanity-check failed!

I noticed this when all of my external functions using externProc were causing that "Unbound value" error - but I could remedy this by instead using importProc with the appropriate header, and then using incl in the module.

However, this is the offending code for SOME_CONST:

x :: Uint8
x = extern "SOME_CONST"

and I don't know any equivalent fix for extern or any other way to reference an external constant.

It's still with older GHC.TypeLits, base < 4.7 etc, so it isn't useful with ghc-7.8.4.

I'm packaging interesting Hackage packages for ArchLinux, and not having Hackage packages is a real obstacle. The build procedure still uses cabal sandbox, so I don't see a reason why fresh Ivory cannot be on Hackage.

It looks like several links from ivorylang.org to github are broken on the tower page.

It would be easier for new users (such as myself) experimenting with Ivory to just be able to fetch it and other ivory related packages from Hackage rather than building everything as part of smaccmpilot-build, especially if using it independently from SMACCMPilot.

I understand this is is a new project under active development but I don't see too much harm in having alpha versions available on Hackage.

Thanks for this awesome library and keep up the good work!

Ivory should issue an error (warning?) if a constant is declared to have an index type that does not contain the constant. (Constants outside the range of integer types already produce an exception.)

low priority -

GHC 7.10 requires the AllowAmbiguousTypes extension to build Ivory.Language.Coroutine. Someone should diagnose why and see if the code can be fixed so we don't need this extra extension. I don't even have GHC 7.10 installed, or I would give a more informative bug report.

In addition to the known bug with the module system (renaming functions), we can get C compile errors depending on the order of 'defStruct's in a module definition, if one depends on the other when generating the header file. Ideally, the order in which we place them in the Module monad wouldn't matter.

Hi. Lets say I have several procedures sharing same signature. I'd like Ivory to build a procedure which would act as a call gate - select the right call branch by analyzing a selector variable. Here is the illustration:

syscalls_1 :: [ Def ('[Inp1] :-> Out1) ]
syscalls_1 = [
   proc "proc11" $ \a -> body ... ,
   proc "proc12" $ \a -> body ...
]

syscalls_2 :: [ Def ('[Inp2, Inp2] :-> Out2) ]
syscalls_2 = [
   proc "proc21" $ \a b -> body ... ,
   proc "proc22" $ \a b -> body ...
]

gate :: [(Int, Def (a :-> b))] -> Def ( (Uint32 ': a) :-> b)
gate pset = proc "gate" $ \ ??? (selector:args) ->
    ???  switch (selector) { 
              case 0 : call (pset !! 0) args ; break;
              case 1 : call (pset !! 1) args ; break ;
              ...
            }
    ???

Now I want to use gate to build a wrapper for all my syscalls. The resulting function should take additional argument describing an implementation to call :

syscall_1 :: Def ('[Uint32, Inp1] :-> Out1)
syscall_1= gate syscalls_1

syscall_2 :: Def ('[Uint32, Inp2, Inp2] :-> Out2)
syscall_2 = gate syscalls_2

Could you please help me to design the implementation of gate in Haskell ?
Thanks in advance.

n times loop claims to run a computation n times, but in the case of n = 0, because it runs from (n-1) down to 0, n will underflow. Here's an example:

loop :: Def ('[Ix 1000] :-> Uint32)
loop  = proc "loop" $ \ n -> body $ do
  a <- local (ival 0)
  n `times` \ _ix -> do
    a' <- deref a
    store a (a' + 1)
  result <- deref a
  ret result

loop_zero :: Def ('[] :-> Uint32)
loop_zero = proc "loop_zero" $ body $ (ret . safeCast) =<< call loop 0

One would expect loop_zero to return 0, but it in fact will return 1000.

Should be a simple zero check to fix. Am happy to implement if issue accepted.

The forever loop combinator clashes in name with the perfectly useful function of the same name from Control.Monad. It would be nice to rename our forever to something else, so that the clash doesn't exist.

It actually breaks all type safety.

It would be nice to be able to use C's continue statement in Ivory loops. We can use if statements spanning the end of the loop body to simulate this in common cases, but there are algorithms that are more clear if expressed using continue.

@elliottt and I discussed this and we don't think there are any difficulties. We would need to add a fourth type parameter to Effects, analogous to BreakEff, for ContinueEff.

$ pwd
/home/kiwamu/src/ivory
$ make
cabal sandbox init
Writing a default package environment file to
/home/kiwamu/src/ivory/cabal.sandbox.config
Creating a new sandbox at /home/kiwamu/src/ivory/.cabal-sandbox
echo "tests: True" >> cabal.sandbox.config
cabal sandbox add-source  ivory/  ivory-artifact/  ivory-backend-acl2/  ivory-backend-c/  ivory-eval/  ivory-examples/  ivory-hw/  ivory-model-check/  ivory-opts/  ivory-quickcheck/  ivory-serialize/  ivory-stdlib/
cabal: Error adding source reference.
Failed to read cabal file of add-source dependency:
/home/kiwamu/src/ivory/ivory-backend-acl2
Makefile:28: recipe for target 'build' failed
make: *** [build] Error 1

I can build them with following patch.

diff --git a/Makefile b/Makefile
index db883e9..9cdab14 100644
--- a/Makefile
+++ b/Makefile
@@ -6,7 +6,6 @@ BIN=.cabal-sandbox/bin
 PACKAGE= \
   ivory \
   ivory-artifact \
-  ivory-backend-acl2 \
   ivory-backend-c \
   ivory-eval \
   ivory-examples \

I am running the following: http://lpaste.net/1313446023258963968. The output with -ddump-splices is:

[1 of 1] Compiling BitDataTest      ( BitDataTest.hs, interpreted )
BitDataTest.hs:1:1: Splicing declarations
    "\n\
    \ bitdata TestBd :: Bits 8 = bdConstr\n\
    \   { lower :: Bit\n\
    \   , upper :: Bits 7\n\
    \   }\n"
  ======>
    [newtype TestBd
       = TestBd (Bits 8)
       deriving (IvoryType,
                 IvoryVar,
                 IvoryExpr,
                 IvoryEq,
                 IvoryInit,
                 IvoryStore,
                 IvoryZeroVal),
     instance BitData TestBd where
       type Ivory.Language.BitData.BitData.BitType TestBd = Bits 8
       toBits (TestBd x) = x
       fromBits = TestBd,
     bdConstr :: Bit -> Bits 7 -> TestBd,
     bdConstr arg0 arg1
       = Ivory.Language.BitData.BitData.unsafeFromRep
           ((0 .| ((safeCast (toRep arg0)) `iShiftL` 0))
            .| ((safeCast (toRep arg1)) `iShiftL` 7)),
     upper :: BitDataField TestBd (Bits 7),
     upper = Ivory.Language.BitData.BitData.BitDataField 0 7 "upper",
     lower :: BitDataField TestBd Bit,
     lower = Ivory.Language.BitData.BitData.BitDataField 7 1 "lower"]
Ok, modules loaded: BitDataTest.

bdConstr looks correct to me - it just looks like (lower << 0) | (upper << 7).

But, the BitDataField definition of upper then seems to be putting that field at the lower 7 bits, and the definition of lower seems to be putting it as the uppermost bit.

The output of main is:

// module bitdata_test Source:

#include "bitdata_test.h"
uint8_t bdTest(void)
{
    return (uint8_t) ((uint8_t) ((uint8_t) 0U |
                                 (uint8_t) ((uint8_t) (true ? (uint8_t) 1U : (uint8_t) ((uint8_t) 0U &
                                                                                        (uint8_t) 1U)) <<
                                            (uint8_t) 0U)) |
                      (uint8_t) ((uint8_t) ((uint8_t) 0U & (uint8_t) 127U) <<
                                 (uint8_t) 7U));
}
uint8_t bdTest2(void)
{
    return (uint8_t) ((uint8_t) ((uint8_t) 0U & (uint8_t) 255U) |
                      (uint8_t) ((uint8_t) 1U << (uint8_t) 7U));
}

// module bitdata_test Header:

#include "ivory.h"
uint8_t bdTest(void);
uint8_t bdTest2(void);

bdTest calls the constructor bdConstr with lower=1 and upper=0, and it looks correct there - I see 1 << 0.
bdTest2 uses withBits (0 :: Uint8) $ setBit lower to create the value, and I see 1 << 7. Somehow the fields lower and upper have reversed in order.

I have written various Ivory procedures that are parametrized over something (say, a board definition or some other configuration), so I will have something like this:

foo :: Bar -> Def ('[] :-> ())
foo bar = proc "foo_proc" $ body $ do ...

With call this can become a bit cumbersome because then every call to it must also be parametrized over Bar, and every call to that recursively, up to the point where some Bar is actually known. In my own code, this can be a lot of repeated boilerplate at every level when I have multiple bits of board/build configuration filtering down from the top level of the build.

In foo above, the definition (in the C sense) may depend on the function parameters, but the declaration (again in the C sense) does not - the function signature cannot, and the function name does not. It seems to me that while incl requires the full definition, call requires only the declaration, and it should be independent of the function's implementation.

I have used a stopgap measure that keeps the proc type and name; something like:

fooProto :: Def ('[] :-> ())
fooProto = importProc "fooProc" ""

This works, but it is a bit of a kludge (is it even kosher to give an empty header name?). It can also easily violate type-safety, should the procedure types between fooProc and fooProto drift apart.

I suppose what I'd like is the ability to do something like...

foo :: Def ('[] :-> ())
foo = procDecl "fooProc"

fooImpl :: Bar -> Def ('[] :-> ())
fooImpl bar = procImpl fooProto $ body $ do ...

where fooProc will fail to type-check if the procedure types are mismatched, I can easily call to foo without worrying about Bar, and I of course must produce a concrete definition via fooImpl in order to actually incl this function.

I may go try to implement this, but I'm interested in people's opinions first. Did I totally miss an existing obvious way in Ivory to do this? Does this still pose big concerns for safety or correctness?

As breakOut is considered unsafe in some contexts, e.g. in conjunction with a use of forever in the body of a tower task, it seems reasonable to consider this an effect to be tracked, rather than removing it from the language. If it's an effect, than it's still something that can be used by programmers, but restricted by API designers.

Defining an effect for break would yield a new signature for the breakOut function:

breakOut :: (CanBreak eff) => Ivory eff ()

Thus registering the requirement for a context that allows the breakOut function to be used. This has an added side-benefit of making it impossible to write functions where breakOut is used in a nonsensical position, as presumably only looping functions would introduce the CanBreak effect locally.

WIth this change to breakOut, the tower task loop example changes so that the argument that it will pass to forever has a very restricted context:

taskBody :: (outer `AllocsIn` s)
         => (forall inner. (inner `AllocsIn` s) => Ivory inner ())
         -> Ivory outer ()
taskBody body =
  do ...
     forever body

As you can see, the taskBody function takes an argument that only permits allocation effects, thus preventing uses of ret, and breakOut, as the new restrictive inner context will not permit them to be used.

uh, ok, so, like, i have cloned Ivory, and I got cabal installed (with sandboxes). now what? where do i go? what do i do? no, i haven't touched hasell in donkey's ages.

https://github.com/agacek noted that constants outside the range of an Ix n type are not a compile-time error and are simply moded. Perhaps a compile-time error should be thrown here?

I observed this on my ArchLinux box that I had just updated. I just reproduced it on a fresh Ubuntu VM using binary GHC 7.10.1 from https://www.haskell.org/ghc/dist/7.10.1/ghc-7.10.1-x86_64-unknown-linux-deb7.tar.bz2 and Cabal from https://www.haskell.org/cabal/release/cabal-install-1.22.2.0/cabal-install-1.22.2.0.tar.gz with 'cabal update' run right beforehand.

Running 'make' gives the following output:

cabal sandbox init
Writing a default package environment file to
/home/hodapp/ivory/cabal.sandbox.config
Creating a new sandbox at /home/hodapp/ivory/.cabal-sandbox
echo "tests: True" >> cabal.sandbox.config
cabal sandbox add-source  ivory/  ivory-artifact/  ivory-backend-acl2/  ivory-backend-c/  ivory-eval/  i
vory-examples/  ivory-hw/  ivory-model-check/  ivory-opts/  ivory-quickcheck/  ivory-serialize/  ivory-s
tdlib/
cabal install  ivory/  ivory-artifact/  ivory-backend-acl2/  ivory-backend-c/  ivory-eval/  ivory-exampl
es/  ivory-hw/  ivory-model-check/  ivory-opts/  ivory-quickcheck/  ivory-serialize/  ivory-stdlib/
Resolving dependencies...
cabal: Could not resolve dependencies:
trying: ivory-0.1.0.2 (user goal)
trying: hpc-0.6.0.2/installed-ac9... (dependency of ivory-0.1.0.2)
trying: ivory-artifact-0.1.0.0 (user goal)
next goal: HStringTemplate (dependency of ivory-artifact-0.1.0.0)
rejecting: HStringTemplate-0.8.3, 0.8.2, 0.8.1, 0.8 (conflict: ivory-artifact
=> HStringTemplate==0.7.3)
rejecting: HStringTemplate-0.7.3 (conflict: hpc =>
time==1.5.0.1/installed-e17..., HStringTemplate => time<1.5)
rejecting: HStringTemplate-0.7.1, 0.7.0, 0.6.12, 0.6.11, 0.6.10, 0.6.9, 0.6.8,
0.6.6, 0.6.5, 0.6.4, 0.6.3, 0.6.2, 0.6.1, 0.6, 0.5.1.3, 0.5.1.2, 0.5.1.1,
0.5.1, 0.5, 0.4.3, 0.4.2, 0.4.1, 0.4, 0.3.2, 0.3.1, 0.3, 0.2 (conflict:
ivory-artifact => HStringTemplate==0.7.3)
Dependency tree exhaustively searched.

Note: when using a sandbox, all packages are required to have consistent
dependencies. Try reinstalling/unregistering the offending packages or
recreating the sandbox.
make: *** [build] Error 1

Hi. I am exploring a way of using ivory for writing applications on top of pre-existing embedded framework written in C. As usual, the framework has its own set of C-headers containing various definitions of types, structs, etc. What is the best way of importing those definitions to Ivory? Is it really necessary to rewrite code usigin [ivory| ... |] facilities (and introduce risks of conflicts or mis-alignment)? Can we ask ivory to build accessors for C-structures defined elsewhere?

The toExpOp function in Gen.hs uses floatingBinary for the ExpRoundF, ExpCeilF, and ExpFloorF functions. Since these functions are unary, this causes an index out of bounds error during runtime.
The lines should be changes to use floatingUnary.