Skip to content

Commit

Permalink
Merge pull request #93 from austral/dereferencing
Browse files Browse the repository at this point in the history
Dereferencing
  • Loading branch information
eudoxia0 committed Nov 27, 2021
2 parents 88b5ba0 + 35a7224 commit 5217d9f
Show file tree
Hide file tree
Showing 20 changed files with 60 additions and 18 deletions.
8 changes: 4 additions & 4 deletions examples/box/Box.aum
Original file line number Diff line number Diff line change
Expand Up @@ -49,15 +49,15 @@ module body Example.Box is
generic [T: Free, R: Region]
function Read_Free(boxref: Reference[Box[T], R]): T is
let ptrref: Reference[Pointer[T], R] := boxref->pointer;
let ptr: Pointer[T] := Deref(ptrref);
let ptr: Pointer[T] := !ptrref;
let value: T := Load(ptr);
return value;
end;

generic [T: Free, R: Region]
function Store_Free(boxref: WriteReference[Box[T], R], value: T): Unit is
let ptrref: WriteReference[Pointer[T], R] := boxref->pointer;
let ptr: Pointer[T] := Deref_Write(ptrref);
let ptr: Pointer[T] := !(ptrref);
Store(ptr, value);
return nil;
end;
Expand All @@ -70,7 +70,7 @@ module body Example.Box is

generic [T: Free, R: Region]
function Swap_Mut(boxref: WriteReference[Box[T], R], value: T): T is
let ptr: Pointer[T] := Deref_Write(boxref->pointer);
let ptr: Pointer[T] := !(boxref->pointer);
let old_value: T := Load(ptr);
Store(ptr, value);
return old_value;
Expand Down Expand Up @@ -121,7 +121,7 @@ module body Example.Box is
when Some(value: Box[Integer_32]) do
borrow value as boxref in rho do
let valueref: Reference[Integer_32, rho] := Get_Value_Ref(boxref);
let contents: Integer_32 := Deref(valueref);
let contents: Integer_32 := !(valueref);
Put_Character(contents);
end;
Unbox(value);
Expand Down
4 changes: 2 additions & 2 deletions examples/buffer/Buffer.aum
Original file line number Diff line number Diff line change
Expand Up @@ -94,14 +94,14 @@ module body Example.Buffer is

generic [T: Free, R: Region]
function Buffer_Size(buffer: Reference[Buffer[T], R]): Natural_64 is
return Deref(buffer->size);
return !(buffer->size);
end;

-- Retrieval

generic [T: Free, R: Region]
function Nth_Free(buffer: Reference[Buffer[T], R], index: Natural_64): T is
let arr: Heap_Array[T] := Deref(buffer->array);
let arr: Heap_Array[T] := !(buffer->array);
return arr[index];
end;

Expand Down
2 changes: 1 addition & 1 deletion examples/ref-to-record/RTR.aum
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ module body Example.RTR is
function Main(root: Root_Capability): Root_Capability is
let r: R := R(X => 97);
borrow r as r2 in rho do
let char: Integer_32 := Deref(r2->X);
let char: Integer_32 := !(r2->X);
Put_Character(char);
end;
let { X: Integer_32 } := r;
Expand Down
2 changes: 2 additions & 0 deletions lib/AbstractionPass.ml
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,8 @@ and abs_expr im expr =
Path (abs_expr im e, List.map (abs_path_elem im) es)
| CEmbed (_, ty, expr, args) ->
Embed (qualify_typespec im ty, expr, List.map (abs_expr im) args)
| CDeref (_, e) ->
Deref (abs_expr im e)

and abs_when im (ConcreteWhen (name, params, body)) =
AbstractWhen (name,
Expand Down
1 change: 1 addition & 0 deletions lib/Ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ and aexpr =
| IfExpression of aexpr * aexpr * aexpr
| Path of aexpr * path_elem list
| Embed of qtypespec * string * aexpr list
| Deref of aexpr

and abstract_when =
| AbstractWhen of identifier * (identifier * qtypespec) list * astmt
Expand Down
1 change: 1 addition & 0 deletions lib/Ast.mli
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,7 @@ and aexpr =
| IfExpression of aexpr * aexpr * aexpr
| Path of aexpr * path_elem list
| Embed of qtypespec * string * aexpr list
| Deref of aexpr

and abstract_when =
| AbstractWhen of identifier * (identifier * qtypespec) list * astmt
Expand Down
2 changes: 2 additions & 0 deletions lib/CodeGen.ml
Original file line number Diff line number Diff line change
Expand Up @@ -257,6 +257,8 @@ let rec gen_exp (mn: module_name) (e: texpr): cpp_expr =
p)
| TEmbed (ty, expr, args) ->
CEmbed (gen_type ty, expr, List.map g args)
| TDeref e ->
CDeref (g e)

and gen_path (mn: module_name) (expr: cpp_expr) (elems: typed_path_elem list): cpp_expr =
match elems with
Expand Down
1 change: 1 addition & 0 deletions lib/Cpp.ml
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ type cpp_expr =
| CIndex of cpp_expr * cpp_expr
| CAddressOf of cpp_expr
| CEmbed of cpp_ty * string * cpp_expr list
| CDeref of cpp_expr

type cpp_stmt =
| CLet of string * cpp_ty * cpp_expr
Expand Down
1 change: 1 addition & 0 deletions lib/Cpp.mli
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,7 @@ type cpp_expr =
| CIndex of cpp_expr * cpp_expr
| CAddressOf of cpp_expr
| CEmbed of cpp_ty * string * cpp_expr list
| CDeref of cpp_expr

type cpp_stmt =
| CLet of string * cpp_ty * cpp_expr
Expand Down
2 changes: 2 additions & 0 deletions lib/CppRenderer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -244,6 +244,8 @@ and render_expr = function
in
let expr' = replace_all expr strs 1 in
"((" ^ (render_type ty) ^ ")(" ^ expr' ^ "))"
| CDeref expr ->
"*" ^ (e expr)

and e expr = render_expr expr

Expand Down
1 change: 1 addition & 0 deletions lib/Cst.ml
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,7 @@ and cexpr =
| CIfExpression of span * cexpr * cexpr * cexpr
| CPath of span * cexpr * concrete_path_elem list
| CEmbed of span * typespec * string * cexpr list
| CDeref of span * cexpr

and cstmt =
| CSkip of span
Expand Down
1 change: 1 addition & 0 deletions lib/Cst.mli
Original file line number Diff line number Diff line change
Expand Up @@ -80,6 +80,7 @@ and cexpr =
| CIfExpression of span * cexpr * cexpr * cexpr
| CPath of span * cexpr * concrete_path_elem list
| CEmbed of span * typespec * string * cexpr list
| CDeref of span * cexpr

and cstmt =
| CSkip of span
Expand Down
1 change: 1 addition & 0 deletions lib/Lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -120,6 +120,7 @@ rule token = parse
| "->" { HYPHEN_RIGHT }
| "=>" { RIGHT_ARROW }
| ":=" { ASSIGN }
| "!" { DEREF }
(* Strings and docstrings *)
| "\"\"\"" { read_triple_string lexbuf }
| '"' { read_string lexbuf }
Expand Down
2 changes: 2 additions & 0 deletions lib/Linearity.ml
Original file line number Diff line number Diff line change
Expand Up @@ -90,6 +90,8 @@ let rec count_appearances (name: identifier) (expr: texpr) =
e' + (sum (List.map ca_path elems))
| TEmbed (_, _, args) ->
sum (List.map ca args)
| TDeref e ->
(ca e)

(* Represents the state of a linear variable *)
type state =
Expand Down
2 changes: 2 additions & 0 deletions lib/Parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,7 @@ open Span
%token HYPHEN_RIGHT
%token RIGHT_ARROW
%token ASSIGN
%token DEREF
/* Strings and docstrings */
%token <string> STRING_CONSTANT
%token <string> TRIPLE_STRING_CONSTANT
Expand Down Expand Up @@ -437,6 +438,7 @@ compound_expression:
| atomic_expression AND atomic_expression { CConjunction (from_loc $loc, $1, $3) }
| atomic_expression OR atomic_expression { CDisjunction (from_loc $loc, $1, $3) }
| NOT atomic_expression { CNegation (from_loc $loc, $2) }
| DEREF atomic_expression { CDeref (from_loc $loc, $2) }
| arith_expr { $1 }
| IF expression THEN expression ELSE expression { CIfExpression (from_loc $loc, $2, $4, $6) }
;
Expand Down
10 changes: 10 additions & 0 deletions lib/Tast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ open Escape
open Type
open Span
open Semantic
open Error

type typed_module = TypedModule of module_name * typed_decl list

Expand Down Expand Up @@ -71,6 +72,7 @@ and texpr =
ty: ty
}
| TEmbed of ty * string * texpr list
| TDeref of texpr

and typed_when =
TypedWhen of identifier * value_parameter list * tstmt
Expand Down Expand Up @@ -152,6 +154,14 @@ let rec get_type = function
ty
| TEmbed (ty, _, _) ->
ty
| TDeref e ->
match get_type e with
| ReadRef (t, _) ->
t
| WriteRef (t, _) ->
t
| _ ->
err ("Internal error: a dereference expression was constructed whose argument is not a reference type.")

and path_elem_type = function
| TSlotAccessor (_, t) ->
Expand Down
1 change: 1 addition & 0 deletions lib/Tast.mli
Original file line number Diff line number Diff line change
Expand Up @@ -70,6 +70,7 @@ and texpr =
ty: ty
}
| TEmbed of ty * string * texpr list
| TDeref of texpr

and typed_when =
TypedWhen of identifier * value_parameter list * tstmt
Expand Down
14 changes: 14 additions & 0 deletions lib/TypingPass.ml
Original file line number Diff line number Diff line change
Expand Up @@ -143,6 +143,18 @@ let rec augment_expr (module_name: module_name) (menv: menv) (rm: region_map) (t
expr,
List.map aug args
)
| Deref expr ->
(* The type of the expression being dereferenced must be either a read-only
reference or a write reference. *)
let expr' = aug expr in
let ty = get_type expr' in
match ty with
| ReadRef _ ->
TDeref expr'
| WriteRef _ ->
TDeref expr'
| _ ->
err "The dereference operator must be applied to an expression of a reference type."

and get_path_ty_from_elems (elems: typed_path_elem list): ty =
assert ((List.length elems) > 0);
Expand Down Expand Up @@ -966,6 +978,8 @@ and is_constant = function
(is_constant head) && (List.for_all is_path_elem_constant elems)
| TEmbed _ ->
true
| TDeref _ ->
false

and is_path_elem_constant = function
| TSlotAccessor _ ->
Expand Down
6 changes: 3 additions & 3 deletions standard/src/Box.aum
Original file line number Diff line number Diff line change
Expand Up @@ -49,15 +49,15 @@ module body Standard.Box is
generic [T: Free, R: Region]
function Read_Free(boxref: Reference[Box[T], R]): T is
let ptrref: Reference[Pointer[T], R] := boxref->pointer;
let ptr: Pointer[T] := Deref(ptrref);
let ptr: Pointer[T] := !ptrref;
let value: T := Load(ptr);
return value;
end;

generic [T: Free, R: Region]
function Store_Free(boxref: WriteReference[Box[T], R], value: T): Unit is
let ptrref: WriteReference[Pointer[T], R] := boxref->pointer;
let ptr: Pointer[T] := Deref_Write(ptrref);
let ptr: Pointer[T] := !ptrref;
Store(ptr, value);
return nil;
end;
Expand All @@ -70,7 +70,7 @@ module body Standard.Box is

generic [T: Free, R: Region]
function Swap_Mut(boxref: WriteReference[Box[T], R], value: T): T is
let ptr: Pointer[T] := Deref_Write(boxref->pointer);
let ptr: Pointer[T] := !(boxref->pointer);
let old_value: T := Load(ptr);
Store(ptr, value);
return old_value;
Expand Down
16 changes: 8 additions & 8 deletions standard/src/Buffer.aum
Original file line number Diff line number Diff line change
Expand Up @@ -46,11 +46,11 @@ module body Standard.Buffer is
-- Grow a buffer by one element, reallocating if necessary.
generic [T: Type, R: Region]
function Increase_Size_By_One(buffer: WriteReference[Buffer[T], R]): Unit is
let old_size: Natural_64 := Deref_Write(buffer->size);
let old_capacity: Natural_64 := Deref_Write(buffer->capacity);
let old_size: Natural_64 := !(buffer->size);
let old_capacity: Natural_64 := !(buffer->capacity);
-- If size = capacity, then we need to resize first.
if old_size = Deref_Write(buffer->capacity) then
let old_array: Heap_Array[T] := Deref_Write(buffer->array);
if old_size = (!(buffer->capacity)) then
let old_array: Heap_Array[T] := !(buffer->array);
let new_capacity: Natural_64 := old_capacity * Growth_Factor;
let new_array: Heap_Array[T] := Resize_Or_Die(old_array, new_capacity);
buffer->capacity := new_capacity;
Expand Down Expand Up @@ -121,14 +121,14 @@ module body Standard.Buffer is

generic [T: Free, R: Region]
function Buffer_Size(buffer: Reference[Buffer[T], R]): Natural_64 is
return Deref(buffer->size);
return !(buffer->size);
end;

-- Retrieval

generic [T: Free, R: Region]
function Nth_Free(buffer: Reference[Buffer[T], R], index: Natural_64): T is
let arr: Heap_Array[T] := Deref(buffer->array);
let arr: Heap_Array[T] := !(buffer->array);
return arr[index];
end;

Expand All @@ -141,7 +141,7 @@ module body Standard.Buffer is

-- generic [T: Type, R: Region]
-- function Insert(buffer: WriteReference[Buffer[T], R], index: Natural_64, elem: T): Unit is
-- let old_size: Natural_64 := Deref_Write(buffer->size);
-- let old_size: Natural_64 := !(buffer->size);
-- -- The insertion index is the position the element will have when the
-- -- buffer is modified. It is a natural number in the closed interval [0, size].
-- --
Expand All @@ -163,7 +163,7 @@ module body Standard.Buffer is
-- else
-- let idx: Natural_64 := old_size + 1;
-- while idx /= index do
-- let arr: Heap_Array[T] := Deref_Write(buffer->array);
-- let arr: Heap_Array[T] := !(buffer->array);
-- let elem_to_move: T := arr[idx - 1];
-- buffer[idx] := elem_to_move;
-- end while;
Expand Down

0 comments on commit 5217d9f

Please sign in to comment.