Add more syscalls to Jasmin

[Rixxc]

This pull request documents the progress of adding the open, read, write and close syscalls to Jasmin. Currently the sycalls can be used using the #open, #close, #write ans #read functions.

Before the pull request can be merged there are several TODOs that need to be worked on:

• [ ] Implement the syscalls in the evaluator
• [ ] Fix proofs in syscall_sem.v
• [ ] What should be returned by syscall_cc in alias.ml?
• [ ] Fix partial match warnings in the ocaml code
• [ ] Insert static ASM snippet instead of call to some label
• [ ] Do some cleanup on the code

[vbgl]

Nice work! Thanks for your contribution. It would be nice if you could write a few example Jasmin programs to better illustrate the intended uses of these syscalls.

You should not bother with the proofs now: let’s have a compiler working first and then you’ll be able to get help from proficient Coq users.

Also, should the programmer explicitly provide the size argument to the write call?

[Rixxc]

I've added a test that should illustrate how the syscalls are supposed to be used.

Currently it is not intended for the programmer to explicitly provide a size argument to the syscalls. The sizes are implicitly inferred from the length of the provided array.

[vbgl]

Thanks for the example. IMHO, you should put the zero terminator in your global constants. There is no need to copy from global to stack.

Are you sure, when calling read/write, that the size to read or write is always statically known?

[Rixxc]

If the string is not explicitly null-terminated, this could lead to memory leaks if the programmer forgets to add the null-terminator. I think there should be a mecanism for to prevent those issues. Maybe in the safety checker or by introducing a new type?

I am not 100% sure wether the size is alway satically known. I was mainly thinking about my special use case and there the size is always known.