lenary

RISC-V Registers Cheatsheet

Numeric	ABI Name	Calling Convention	RVC?	RVE?
x0	zero	Immutable	No	Yes
x1	ra	Return Address	No	Yes
x2	sp	Callee-Saved	No*	Yes
x3	gp	Unallocatable	No	Yes
x4	tp	Unallocatable	No	Yes
x5-x7	t0-t2	Caller-Saved	No	Yes

lenary

          _Complex float	size:  8	align:  4	atomic-size:  8	atomic-align:  4
         _Complex double	size: 16	align:  8	atomic-size: 16	atomic-align:  8
 struct { char buf[0]; }	size:  0	align:  1	atomic-size:  1	atomic-align:  1
 struct { char buf[1]; }	size:  1	align:  1	atomic-size:  1	atomic-align:  1
 struct { char buf[2]; }	size:  2	align:  1	atomic-size:  2	atomic-align:  2
 struct { char buf[3]; }	size:  3	align:  1	atomic-size:  4	atomic-align:  4
 struct { char buf[4]; }	size:  4	align:  1	atomic-size:  4	atomic-align:  4
 struct { char buf[5]; }	size:  5	align:  1	atomic-size:  5	atomic-align:  1
 struct { char buf[6]; }	size:  6	align:  1	atomic-size:  6	atomic-align:  1
 struct { char buf[7]; }	size:  7	align:  1	atomic-size:  7	atomic-align:  1

lenary

You should read my dissertation here: http://lenary.co.uk/publications/dissertation/ it gives enough of an overview that you should see what is doable and what isn't. Of course the writing isn't super great, sorry about that.

Then, of course, realise that this is about 1/3 finished, but pretty much abandoned right now. Here are some jumping off points to taking it forwards:

Some ideas for jumping off points:

• look at the effects system in Idris, how this might work with the models of concurrency seen in erlang
• how do the different trade-offs that idris makes affect how good this will be at distribution. Concurrency is a slightly different problem, where I assumed a lack of failures (ie if one thing failed, it's fine for everything to fail).
• Better types for behaviours should be doable. I touched on this in my dissertation.
• There's a haskell library for generating core erlang. That could be a better backend than escripts.

lenary

#lang rosette

(require rosette/lib/synthax
         (only-in rosette/base/util/array reshape))

(provide generate-symbolic define-synthax-rule
         (all-from-out rosette/lib/synthax))

;; Fundamental. If you want bitvectors, use the bv explicit types
(current-bitwidth #f)

lenary

#include <dlfcn.h>
#include <stdio.h>
#include <stdbool.h>
#include <string.h>

#ifdef __APPLE__
#include <mach-o/dyld.h>
#else // Linux
#include <link.h>
#endif

lenary

-- In `f` we want to keep piping (part of) the result of one function into
-- another, and stop as soon as something fails
f :: [A] -> Either String (B, [A])
f xs =
  case f1 xs of
    Left s -> Left s
    Right (res1, xs') ->
      case f2 xs' of
        Left s -> Left s
        Right (res2, xs'') ->

lenary

%% Source Code Notes
\ProvidesPackage{listing-label}
% We use tikz for drawing the circles around the letters. Dumb, probably. 
\RequirePackage{tikz}

% Counter, numbered by section
\newcounter{lstlistinglabel}[section]
% Length for left out-dent
\newlength{\lstlabelleftoutdent}

lenary

#include <stdio.h>

// The file with the unchecked interface
#include <stdlib.h>

// The Redeclaration with the correct type
void *calloc(size_t nmemb, size_t size) : byte_count(nmemb * size);

#pragma BOUNDS_CHECKED ON

lenary

precmd_functions=("_exit_status" ${precmd_functions[@]})
function _exit_status() {
  local last_exit_status=$?

  export last_exit=""
  if [ -z "${last_exit_status}" ]; then
    last_exit=""
  elif (( last_exit_status != 0 )); then
    local description

lenary

{-# OPTIONS --copatterns #-}

open import Agda.Builtin.Nat
open import Agda.Builtin.Bool
open import Agda.Builtin.Equality


trans : {A : Set} {a b c : A} -> a ≡ b -> b ≡ c -> a ≡ c
trans refl refl = refl