galoisinc / ivory Goto Github PK
View Code? Open in Web Editor NEWThe Ivory EDSL
Home Page: http://ivorylang.org
License: BSD 3-Clause "New" or "Revised" License
The Ivory EDSL
Home Page: http://ivorylang.org
License: BSD 3-Clause "New" or "Revised" License
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.
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.
https://github.com/agacek noted that constants outside the range of an Ix n
type are not a compile-time error and are simply mod
ed. Perhaps a compile-time error should be thrown here?
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.
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.
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
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.
I write following code:
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?
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
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 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 \
It looks like several links from ivorylang.org to github are broken on the tower page.
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.
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.
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:
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
void
instead of uint32_t
, and a return;
is generated when compilingvoid 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!
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
Add QC backend for C values and esp. structs.
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.
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.
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.
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
It actually breaks all type safety.
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.
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.
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.
The cmdlib library is way too complicated for what we need, let's just write a simpler option parser.
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!
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.
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)
.
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.
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.
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.
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?
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.)
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
.
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?
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.
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?
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.
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.
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.
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?
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.
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?
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.
ts2@linux-0fiz:~/tmp/xx9/2015_12_22_Ivory_Programming_Language/uhuu/ivory$ cabal --version
cabal-install version 1.16.0.2
using version 1.16.0 of the Cabal library
ts2@linux-0fiz:~/tmp/xx9/2015_12_22_Ivory_Programming_Language/uhuu/ivory$ nice -n20 make
cabal sandbox init
cabal: unrecognised command: sandbox (try --help)
Makefile:23: recipe for target 'cabal.sandbox.config' failed
make: *** [cabal.sandbox.config] Error 1
ts2@linux-0fiz:~/tmp/xx9/2015_12_22_Ivory_Programming_Language/uhuu/ivory$ uname -a
Linux linux-0fiz 3.16.7-29-desktop #1 SMP PREEMPT Fri Oct 23 00:46:04 UTC 2015 (6be6a97) x86_64 x86_64 x86_64 GNU/Linux
ts2@linux-0fiz:~/tmp/xx9/2015_12_22_Ivory_Programming_Language/uhuu/ivory$ date
Tue Dec 22 23:40:21 EET 2015
ts2@linux-0fiz:~/tmp/xx9/2015_12_22_Ivory_Programming_Language/uhuu/ivory$ ls
CODE_OF_CONDUCT.md ivory-backend-c ivory-hw ivory-quickcheck Makefile
ivory ivory-eval ivory-model-check ivory-serialize Makefile.sandbox
ivory-artifact ivory-examples ivory-opts ivory-stdlib README.md
ivory-backend-acl2 ivory-formal-model ivory-paper LICENSE
ts2@linux-0fiz:~/tmp/xx9/2015_12_22_Ivory_Programming_Language/uhuu/ivory$ ghc -v
Glasgow Haskell Compiler, Version 7.6.3, stage 2 booted by GHC version 7.6.3
Using binary package database: /usr/lib64/ghc-7.6.3/package.conf.d/package.cache
wired-in package ghc-prim mapped to ghc-prim-0.3.0.0-d5221a8c8a269b66ab9a07bdc23317dd
wired-in package integer-gmp mapped to integer-gmp-0.5.0.0-2f15426f5b53fe4c6490832f9b20d8d7
wired-in package base mapped to base-4.6.0.1-8aa5d403c45ea59dcd2c39f123e27d57
wired-in package rts mapped to builtin_rts
wired-in package template-haskell mapped to template-haskell-2.8.0.0-a3012803fde1dc362e555b35a1a78e6d
wired-in package dph-seq not found.
wired-in package dph-par not found.
Hsc static flags: -static
*** Deleting temp files:
Deleting:
*** Deleting temp dirs:
Deleting:
ghc: no input files
Usage: For basic information, try the `--help' option.
ts2@linux-0fiz:~/tmp/xx9/2015_12_22_Ivory_Programming_Language/uhuu/ivory$
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.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.