notbad4u / osl Goto Github PK

• calling function
• binary operator
• conditional expression
• unary expression (most of them will be ignored)

⚠️ The support of cast expression will be tracked in another issue

We should be able to modify x through y.

decl x;
transfer newResource(mut) x;
decl y;
y mborrow x;
transfer newResource(mut) y;

but for now, that transforms y into a new resource.

    <env>
      x |-> 0
      y |-> 2
    </env>
    <store>
      0 |-> #rs ( mut , .Props )
      2 |-> #rs ( mut , .Props )
    </store>

but we should have

    <env>
      x |-> 0
      y |-> 2
    </env>
    <store>
      0 |-> #rs ( mut , .Props )
      2 |-> #br ( 3 , 3 , #mutRef ( 0 ) )
    </store>

Add the support the transpilation of C-lang function call.

exp ::= ..., call exp (exps) 

Maybe some std expression call can be ignored like:

printf("hello");

because they don't take any parameters.

• parse Id parameter
• parse call
• parse expression
• parse constant

When we call a function, in #bindparams, we should verify that the Props of the parameters match the Props of the Type declared in the function definition.

Example:

fn foo(x: own(mut) {....}

decl a;
transfer newResource(mut, copy) a;
call foo(a); //succeed

decl b;
transfer newResource(copy) b;
call foo(b); // fail

In this example, the X parameters is declared with the prop mut, so when we #bindparams in the two call, we have to verify that a and b have also mut.

The dereference operator is denoted by * in OSL.
This will be a special case of unary expression with an UnaryOperator::Indirection.

int x = 2;
int * p_x = &x;
*p_x = b;

Should be transpiled into

decl x;
decl p_x;
p_x borrow x;
*p_x;

⚠️ This is not a priority.

Currently, OSL uses version ~3.5 of K Framework and we should consider migrating to version 5.1.
A part of the semantic will need to be rewritten.

A goto statement in C programming provides an unconditional jump from the goto to a labeled statement in the same scope.
For now, OSL works only for programs with branching and looping control flow like C.
The support of goto will need to modify the semantic of OSL.

The usage of the goto statement is highly discouraged, so should we consider supporting it?

Variadic functions are functions that can take a variable number of arguments. The variadic function consists of at least one fixed variable and then an ellipsis(…) as the last parameter.

Syntax:

int function_name(data_type variable_name, ...);

Accessing the variadic arguments from the function body uses the following library facilities:

• va_start enables access to variadic function arguments
• va_arg accesses the next variadic function argument
• va_end ends traversal of the variadic function arguments
• va_list holds the information needed by va_start, va_arg, va_end, and va_copy

Usage:

#include<stdarg.h>

int maxof(int n_args, ...)
{
    va_list ap;
    va_start(ap, n_args);
    int max = va_arg(ap, int);
    for(int i = 2; i <= n_args; i++) {
        int a = va_arg(ap, int);
        if(a > max) max = a;
    }
    va_end(ap);
    return max;
}

The support of this feature is necessary to fully support stdlib functions like printf, scanf...

We need a CIL to run the frontend unit test and maybe evaluate the test folder in model.

The Rust borrow checker does understand structs to know that it's possible to borrow disjoint fields of a struct simultaneously.

struct Foo {
    a: i32,
    b: i32,
    c: i32,
}

let mut x = Foo {a: 0, b: 0, c: 0};
let a = &mut x.a;
let b = &mut x.b;
let c = &x.c;
*b += 1;
let c2 = &x.c;
*a += 10;
println!("{} {} {} {}", a, b, c, c2);

But OSL doesn't support product type and sum type (so struct and other), only variable are supported.
As a first step, we can simplify the declaration of a struct as a variable. So we can only borrow the entire struct as immutable or mutable. It is not possible to borrow parts of a struct as mutable and other parts as immutable.

struct Pair {
  int x, y;
}

Pair t = { .x = 1, .y = 2 };

become

decl pair;

After, we can change the semantic to support Product and Sum types for partial borrowing.

The syntax for a switch statement in C programming language is as follows:

switch(expression) {

   case constant-expression  :
      statement(s);
      break; /* optional */
	
   case constant-expression  :
      statement(s);
      break; /* optional */
  
   /* you can have any number of case statements */
   default : /* Optional */
   statement(s);
}

NOTE: break statement is tagged as not supported

The transpiler follows this rule:
Each parameter that is a reference gets its own lifetime parameter. In other words, a function with one parameter gets one lifetime parameter: fn foo<'a>(x: &'a i32); a function with two parameters gets two separate lifetime parameters: fn foo<'a, 'b>(x: &'a i32, y: &'b i32); and so on.

But when we have:

fn foo(x:#ref('a,#own(mut)),y:#ref('b,#own(mut))) -> #ref('rt,#own(mut)) {
    // return x
    x
}

We should put the same lifetime as x has in parameter. So we should have: -> #ref('a,#own(mut)) instead of #ref('rt,#own(mut)).

The Ownership model semantics does not compile anymore because there is some breaking change in Opam packages.

With a ubuntu:20.4 the script k-configure-opam crash with this error trace:

<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
[ERROR] The compilation of conf-gmp failed at "/root/.opam/opam-init/hooks/sandbox.sh build sh -exc cc -c $CFLAGS -I/usr/local/include test.c".
[ERROR] The compilation of conf-perl failed at "/root/.opam/opam-init/hooks/sandbox.sh build perl --version".
[ERROR] The compilation of conf-pkg-config failed at "/root/.opam/opam-init/hooks/sandbox.sh build pkg-config --help".
[ERROR] The compilation of ocaml-variants failed at "/root/.opam/opam-init/hooks/sandbox.sh build patch -p1 -i /root/.opam/repo/k/compilers/4.03.1/4.03.1+k/files/opam-compiler.patch".

#=== ERROR while compiling ocaml-variants.4.03.1+k ============================#
# context              2.0.5 | linux/x86_64 |  | file:///k/lib/opam
# path                 ~/.opam/4.03.1+k/.opam-switch/build/ocaml-variants.4.03.1+k
# command              ~/.opam/opam-init/hooks/sandbox.sh build patch -p1 -i /root/.opam/repo/k/compilers/4.03.1/4.03.1+k/files/opam-compiler.patch
# exit-code            1
# env-file             ~/.opam/log/ocaml-variants-175-6ef1df.env
# output-file          ~/.opam/log/ocaml-variants-175-6ef1df.out
### output ###
# bwrap: Creating new namespace failed: Operation not permitted


#=== ERROR while compiling conf-pkg-config.2 ==================================#
# context              2.0.5 | linux/x86_64 |  | https://opam.ocaml.org#2de26148
# path                 ~/.opam/4.03.1+k/.opam-switch/build/conf-pkg-config.2
# command              ~/.opam/opam-init/hooks/sandbox.sh build pkg-config --help
# exit-code            1
# env-file             ~/.opam/log/conf-pkg-config-175-2e72e2.env
# output-file          ~/.opam/log/conf-pkg-config-175-2e72e2.out
### output ###
# bwrap: Creating new namespace failed: Operation not permitted


#=== ERROR while compiling conf-perl.2 ========================================#
# context              2.0.5 | linux/x86_64 |  | https://opam.ocaml.org#2de26148
# path                 ~/.opam/4.03.1+k/.opam-switch/build/conf-perl.2
# command              ~/.opam/opam-init/hooks/sandbox.sh build perl --version
# exit-code            1
# env-file             ~/.opam/log/conf-perl-175-5dd0bd.env
# output-file          ~/.opam/log/conf-perl-175-5dd0bd.out
### output ###
# bwrap: Creating new namespace failed: Operation not permitted


#=== ERROR while compiling conf-gmp.4 =========================================#
# context              2.0.5 | linux/x86_64 |  | https://opam.ocaml.org#2de26148
# path                 ~/.opam/4.03.1+k/.opam-switch/build/conf-gmp.4
# command              ~/.opam/opam-init/hooks/sandbox.sh build sh -exc cc -c $CFLAGS -I/usr/local/include test.c
# exit-code            1
# env-file             ~/.opam/log/conf-gmp-175-4aef26.env
# output-file          ~/.opam/log/conf-gmp-175-4aef26.out
### output ###
# bwrap: Creating new namespace failed: Operation not permitted



<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
+- The following actions failed
| - build conf-gmp        4
| - build conf-perl       2
| - build conf-pkg-config 2
| - build ocaml-variants  4.03.1+k
+- 
- No changes have been performed

The packages you requested declare the following system dependencies. Please make sure they are installed before retrying:
    libgmp-dev perl pkg-config

Installing this package with apt does not solve the problem.

With a ubuntu:18.4 the script k-configure-opam crash succeed and also the compilation of the model, but when we try to run the model we get the error:

The module `CamlinternalFormatBasics' is already loaded (either by the main program or a previously-dynlinked library)Fatal error: exception Failure("could not load semantics")
[Error] Critical: Failed to execute the program in OCaml. See output for error
information.

As we do not have control over Opam packages, I do not see a solution for solving this problem. Moreover, we are based on an old version of K-Framework (see #6) and no support is provided anymore by maintainers.

Currently, OSL doesn't support sequential collection of elements of the same type like array.
Maybe we should treat an array like a variable and treat the access by an index like variable access?
This should work because the borrow checker doesn't understand partial borrow of arrays or slices.

So this doesn't work:

let mut x = [1, 2, 3];
let a = &mut x[0];
let b = &mut x[1];
println!("{} {}", a, b);

error[E0499]: cannot borrow `x[..]` as mutable more than once at a time
 --> src/lib.rs:4:18
  |
3 |     let a = &mut x[0];
  |                  ---- first mutable borrow occurs here
4 |     let b = &mut x[1];
  |                  ^^^^ second mutable borrow occurs here
5 |     println!("{} {}", a, b);
6 | }
  | - first borrow ends here

error: aborting due to previous error

• Support the declaration of variable
• Support the declaration of global variable
• Support declaration with initializer
• Support declaration with of multiple variables with same type: T a, b = <expression>, c;

The C library function void exit(int status) terminates the calling process immediately.

void exit(int status) // status − This is the status value returned to the parent process.

We should manage this function as free method. We may transpile this into the statement:

val(status)

but we have to check if OSL support val(<Exp>).

OSL only supports loop, so we have to first transform a while and for loop into a loop with a break (branch) statement.
We can find some inspiration from MIR Rust lang rewriting.

OSL grammar:

! <block> ; 

example:

!{
	transfer newResource() x; 
	decl y;
	@ {transfer newResource() y;}, {transfer x y;} ;
} ;

This enhancement will depend from #4

• Transpile do-while
• Transpile for-loop
• Transpile while

Many programs tested will use these two parameters from main.
We should add them in the signature of the main function and make a top
declaration (decl) of these two variables.

In the C Programming Language, the #include directive tells the preprocessor to insert the contents of another file into the source code at the point where the #include directive is found. Our C parser library runs the preprocessor and puts the result in one file.
For the prototype, we need to be able to parse C program that include stdio and stdlib, because a good things will be to be able to transpile basic code found on GitHub.

We should verify that any value are moved in a loop.
For this, we should verify that we have an injection between the two store.

For example:

struct Data();

fn foo(data: Data) {}

fn main() {
    let d = Data();
    loop {
        foo(d);
    }
}

We got the error:

error[E0382]: use of moved value: `d`
 --> src/main.rs:8:13
  |
6 |     let d = Data();
  |         - move occurs because `d` has type `Data`, which does not implement the `Copy` trait
7 |     loop {
8 |         foo(d);
  |             ^ value moved here, in previous iteration of loop

We should able to support this kind of expression (array of struct access):

  printf("Marks: %.1f", s[i].marks);
    |                               ---- structure tag which is not an Expression::Identifier

• return expression and return type
• arguments

The grammar:

function ::= fn name ( parameters ) → type block
paramters ::= <id: type ,>*
prop ::= copy | ...
props ::= <prop>*
type ::= own(props) | ref (lif etime, type)
lifetime ::= int | var

example:

fn sumV(v: ref(’a, own()), i:own(copy)) -> own(copy) {
...
}

decl x;
transfer newResource() x;
decl y;
y mborrow x;

we got this

      <env>
        x |-> 0
        y |-> 2
      </env>
      <store>
        0 |-> #rs ( .Props )
        2 |-> #br ( 3 , 3 , #mutRef ( 0 ) )
      </store>

but we should refuse this code.

We should be able to transpile C if statement in OSL branch.

example:

if (i >= v) {
    return 0;
} else {
    return i;
}

translated into:

@ {
    val(newResource()) //This returns the value 0
}, {
    val(newResource()) //return a resource
};