ssm-lang / Scoria

This is an embedding of the Sparse Synchronous Model, in Haskell!
BSD 3-Clause "New" or "Revised" License
4 stars 0 forks source link

Add uint64 type, use signed int for existing int64 #1

Closed j-hui closed 3 years ago

j-hui commented 3 years ago

The previous implementation of 64-bit integers didn't distinguish between signed and unsigned. I introduced an explicitly unsigned type, which we use wherever a time type is to be used.

j-hui commented 3 years ago

When I ran stack test, it encountered some issue and went through several rounds of shrinking, until it encountered some strange parse error:

*** Failed! Assertion failed (after 7 tests and 6 shrinks):
Program:
  entrypoint: fun2
  arguments: [Right ("ref1",Ref TBool), Right ("ref2",Ref TBool), Left (-1 < 4), Left (11 - 12), Right ("ref6",Ref TBool)]

fun1()
  If ((1 + 1) < (-2 * 1)) [] []
fun2(("ref1",Ref TBool), ("ref2",Ref TBool), ("var3",TBool), ("var4",TUInt64), ("ref6",Ref TBool))
  Fork [("fun2",[Right ("ref6",Ref TBool),Right ("ref6",Ref TBool),Left True,Left 6,Right ("ref6",Ref TBool)])]
  SetRef ("ref1",Ref TBool) (1 == 1)
  Wait [("ref1",Ref TBool),("ref2",Ref TBool)]
  SetLocal (Fresh "var3") TBool (1 < 1)

***********
parse-error
***********

fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
fork fun2
... (goes on for some while)
j-hui commented 3 years ago

This is parseerror.ssm:

Program:
  entrypoint: fun2
  arguments: [Right ("ref1",Ref TBool), Right ("ref2",Ref TBool), Left (-1 < 4), Left (11 - 12), Right ("ref6",Ref TBool)]

fun1()
  If ((1 + 1) < (-2 * 1)) [] []
fun2(("ref1",Ref TBool), ("ref2",Ref TBool), ("var3",TBool), ("var4",TUInt64), ("ref6",Ref TBool))
  Fork [("fun2",[Right ("ref6",Ref TBool),Right ("ref6",Ref TBool),Left True,Left 6,Right ("ref6",Ref TBool)])]
  SetRef ("ref1",Ref TBool) (1 == 1)
  Wait [("ref1",Ref TBool),("ref2",Ref TBool)]
  SetLocal (Fresh "var3") TBool (1 < 1)

And parseerror.c:

#include "peng-platform.h"
#include "peng.h"
#include <stdio.h>
#include <pthread.h>
#include <unistd.h>

#ifdef DEBUG
#define DEBUG_PRINT(x) printf(x);
#else
#define DEBUG_PRINT(x) while(0) {}
#endif

typedef struct {
    ACTIVATION_RECORD_FIELDS;
} act_fun1_t;

typedef struct {
    ACTIVATION_RECORD_FIELDS;
    sv_bool_t* ref1;
    sv_bool_t* ref2;
    sv_bool_t var3;
    sv_uint64_t var4;
    sv_bool_t* ref6;
    trigger_t trig1;
    trigger_t trig2;
} act_fun2_t;

act_fun1_t* enter_fun1(act_t* caller, uint32_t priority, uint8_t depth);
void step_fun1(act_t* gen_act);

act_fun2_t* enter_fun2(act_t* caller, uint32_t priority, uint8_t depth, sv_bool_t* ref1, sv_bool_t* ref2, bool var3, uint64 var4, sv_bool_t* ref6);
void step_fun2(act_t* gen_act);

act_fun1_t* enter_fun1(act_t* caller, uint32_t priority, uint8_t depth) {
    act_fun1_t* act = (act_fun1_t*) enter(sizeof(act_fun1_t), step_fun1, caller, priority, depth);
    return act;
}

act_fun2_t* enter_fun2(act_t* caller, uint32_t priority, uint8_t depth, sv_bool_t* ref1, sv_bool_t* ref2, bool var3, uint64 var4, sv_bool_t* ref6) {
    act_fun2_t* act = (act_fun2_t*) enter(sizeof(act_fun2_t), step_fun2, caller, priority, depth);
    act->ref1 = ref1;
    act->ref2 = ref2;
    initialize_bool(&act->var3);
    assign_bool(&act->var3, act->priority, var3);
    initialize_uint64(&act->var4);
    assign_uint64(&act->var4, act->priority, var4);
    act->ref6 = ref6;
    act->trig1.act = (act_t *) act;
    act->trig2.act = (act_t *) act;
    return act;
}

void step_fun1(act_t* gen_act) {
    act_fun1_t* act = (act_fun1_t*) gen_act;
    switch(act->pc) {
        case 0:
            if (!(((1 + 1) < ((-2) * 1)))) goto L0;
            goto L1;

            L0:

            L1:
        case 1:
        leave((act_t *) act, sizeof(act_fun1_t));
    }
}

void step_fun2(act_t* gen_act) {
    act_fun2_t* act = (act_fun2_t*) gen_act;
    switch(act->pc) {
        case 0:
            DEBUG_PRINT("fork fun2\n");
            act->pc = 1;
            call((act_t *) enter_fun2((act_t *) act, act->priority, act->depth, act->ref6, act->ref6, true, 6UL, act->ref6));
            return;
        case 1:
            assign_bool(act->ref1, act->priority, (1 == 1));
            sensitize((sv_t *)act->ref1, &act->trig1);
            sensitize((sv_t *)act->ref2, &act->trig2);
            act->pc = 2;
            return;
        case 2:
            desensitize(&act->trig1);
            desensitize(&act->trig2);
            assign_bool(&act->var3, act->priority, (1 < 1));
        case 3:
        leave((act_t *) act, sizeof(act_fun2_t));
    }
}

void* sleeper(void* arg) {
    sleep(0.5);
    exit(0);
}
void top_return(act_t* act) {
    return;
}

void main() {
    pthread_t sleep_thread;
    pthread_create(&sleep_thread, NULL, &sleeper, NULL);

    act_t top = { .step = top_return };
    sv_bool_t ref1;
    initialize_bool(&ref1);
    ref1.value = false;
    sv_bool_t ref2;
    initialize_bool(&ref2);
    ref2.value = false;
    sv_bool_t ref6;
    initialize_bool(&ref6);
    ref6.value = false;
    fork_routine((act_t *) enter_fun2(&top, PRIORITY_AT_ROOT, DEPTH_AT_ROOT, &ref1, &ref2, ((-1) < 4), (11UL - 12UL), &ref6));
    tick();
    printf("now %lu eventqueuesize %d\n", now, event_queue_len);

    while(1) {
        now = next_event_time();
        if(now == NO_EVENT_SCHEDULED)
            break;
        tick();
        printf("now %lu eventqueuesize %d\n", now, event_queue_len);

    }
    printf("result ref1 bool %d\n", ref1.value);
    printf("result ref2 bool %d\n", ref2.value);
    printf("result ref6 bool %d\n", ref6.value);
}
Rewbert commented 3 years ago

The parse error seems to be that the pthreads stuff is messing with fprint, and some of the trace-items become malformed and unrecognizable to the parser. Since we last spoke I have changed the testing code such that the tests that actually need to inspect the trace uses unix timeout, which seemed to not break anything with printf, while tests that don't care about the trace (like Valgrind) uses pthreads to limit execution time. I will look more tomorrow, but great job!

j-hui commented 3 years ago

Ah got it. Awesome, let me know when you push that code and I can test again!

Rewbert commented 3 years ago

I also had a thought about that very weird Num instance. Perhaps it is possible to add a data Lit a wrapper in the frontend similarly to Exp a & Ref a? That way the phantom type in the Lit type could specify which the polymorphic type in fromInteger is.

Brainstorming (not checked in ghc)

type Lit a = SSMLit

instance Num (Lit Int) where -- need type synonym instances, flexible instances
  ...
  fromInteger i = LInt (fromInteger i)
  ...

instance Num (Lit Word8) where
  ...
  fromInteger i = LUInt8 (fromInteger i)
  ...

instance Num a => Num (Exp a) where
  ...
  fromInteger i = Lit (typeOf (Proxy @a)) $ fromInteger i -- need scoped type variables and type applications extensions
  ...

-- etc

There will be a lot of instances that look very much the same, but a user of the language is not supposed to fiddle with this code anyway, just reap the benefits!

I suppose this goes very much hand in hand with designing a nice frontend though, which we definitely should do soon. I think we can get a very nice interface with wrappers (for type safety) and classes (for nice looking functions).

Rewbert commented 3 years ago

Everything looks great! I played myself by deciding to commit my own changes from a few days ago before merging this branch, but the merge conflict was quite straightforward.

I forgot to tell you about Trace.hs when we spoke but you seem to have understood the intention of it :) The generated code (if compiled with -DDEBUG) will yell at you what it's doing, producing a trace. The interpreter emits values of this datatype, but the c-code will print to stdout. In Trace.hs I wrote a parser that just parses this output to the same format as the one the interpreter is outputting.

j-hui commented 3 years ago

Lol I just grepped "64" and made changes wherever I saw Int64 being mentioned in some form or another. But yeah I figured that's what that was. Thanks for merging!