Skip to content

Commit

Permalink
[asl][semantics] Addressing feedback.
Browse files Browse the repository at this point in the history
  • Loading branch information
@Roman-Manevich
Roman-Manevich committed Mar 27, 2024
1 parent c4adf29 commit 59be792
Show file tree
Hide file tree
Showing 10 changed files with 1,528 additions and 1,011 deletions.
98 changes: 50 additions & 48 deletions asllib/Interpreter.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -392,17 +392,17 @@ module Make (B : Backend.S) (C : Config) = struct
(* End *)
(* Begin Binop *)
| E_Binop (op, e1, e2) ->
let*^ m1, env' = eval_expr env e1 in
let*^ m2, new_env = eval_expr env' e2 in
let*^ m1, env1 = eval_expr env e1 in
let*^ m2, new_env = eval_expr env1 e2 in
let* v1 = m1 and* v2 = m2 in
let* v = B.binop op v1 v2 in
return_normal (v, new_env) |: SemanticsRule.Binop
(* End *)
(* Begin Unop *)
| E_Unop (op, e') ->
let** v', env' = eval_expr env e' in
let* v = B.unop op v' in
return_normal (v, env') |: SemanticsRule.Unop
| E_Unop (op, e1) ->
let** v1, env1 = eval_expr env e1 in
let* v = B.unop op v1 in
return_normal (v, env1) |: SemanticsRule.Unop
(* End *)
(* Begin ECond *)
| E_Cond (e_cond, e1, e2) ->
Expand All @@ -420,27 +420,27 @@ module Make (B : Backend.S) (C : Config) = struct
(* Begin ESlice *)
| E_Slice (e_bv, slices) ->
let*^ m_bv, env1 = eval_expr env e_bv in
let*^ m_positions, env' = eval_slices env1 slices in
let*^ m_positions, new_env = eval_slices env1 slices in
let* v_bv = m_bv and* positions = m_positions in
let* v = B.read_from_bitvector positions v_bv in
return_normal (v, env') |: SemanticsRule.ESlice
return_normal (v, new_env) |: SemanticsRule.ESlice
(* End *)
(* Begin ECall *)
| E_Call (name, actual_args, params) ->
let**| ms, env = eval_call (to_pos e) name env actual_args params in
let**| ms, new_env = eval_call (to_pos e) name env actual_args params in
let* v =
match ms with
| [ m ] -> m
| _ ->
let* vs = sync_list ms in
B.create_vector vs
in
return_normal (v, env) |: SemanticsRule.ECall
return_normal (v, new_env) |: SemanticsRule.ECall
(* End *)
(* Begin EGetArray *)
| E_GetArray (e_array, e_index) -> (
let*^ m_array, env1 = eval_expr env e_array in
let*^ m_index, env' = eval_expr env1 e_index in
let*^ m_index, new_env = eval_expr env1 e_index in
let* v_array = m_array and* v_index = m_index in
match B.v_to_int v_index with
| None ->
Expand All @@ -449,36 +449,36 @@ module Make (B : Backend.S) (C : Config) = struct
fatal_from e (Error.UnsupportedExpr e_index)
| Some i ->
let* v = B.get_index i v_array in
return_normal (v, env') |: SemanticsRule.EGetArray)
return_normal (v, new_env) |: SemanticsRule.EGetArray)
(* End *)
(* Begin ERecord *)
| E_Record (_, e_fields) ->
let names, fields = List.split e_fields in
let** v_fields, env' = eval_expr_list env fields in
let** v_fields, new_env = eval_expr_list env fields in
let* v = B.create_record (List.combine names v_fields) in
return_normal (v, env') |: SemanticsRule.ERecord
return_normal (v, new_env) |: SemanticsRule.ERecord
(* End *)
(* Begin EGetField *)
| E_GetField (e_record, field_name) ->
let** v_record, env' = eval_expr env e_record in
let** v_record, new_env = eval_expr env e_record in
let* v = B.get_field field_name v_record in
return_normal (v, env') |: SemanticsRule.EGetBitField
return_normal (v, new_env) |: SemanticsRule.EGetBitField
(* End *)
(* Begin EGetFields *)
| E_GetFields _ ->
fatal_from e Error.TypeInferenceNeeded |: SemanticsRule.EGetBitFields
(* End *)
(* Begin EConcat *)
| E_Concat e_list ->
let** v_list, env' = eval_expr_list env e_list in
let** v_list, new_env = eval_expr_list env e_list in
let* v = B.concat_bitvectors v_list in
return_normal (v, env') |: SemanticsRule.EConcat
return_normal (v, new_env) |: SemanticsRule.EConcat
(* End *)
(* Begin ETuple *)
| E_Tuple e_list ->
let** v_list, env' = eval_expr_list env e_list in
let** v_list, new_env = eval_expr_list env e_list in
let* v = B.create_vector v_list in
return_normal (v, env') |: SemanticsRule.ETuple
return_normal (v, new_env) |: SemanticsRule.ETuple
(* End *)
(* Begin EUnknown *)
| E_Unknown t ->
Expand All @@ -487,9 +487,9 @@ module Make (B : Backend.S) (C : Config) = struct
(* End *)
(* Begin EPattern *)
| E_Pattern (e, p) ->
let** v1, env' = eval_expr env e in
let** v1, new_env = eval_expr env e in
let* v = eval_pattern env e v1 p in
return_normal (v, env') |: SemanticsRule.EPattern
return_normal (v, new_env) |: SemanticsRule.EPattern
(* End *)

(* Evaluation of Side-Effect-Free Expressions *)
Expand Down Expand Up @@ -646,22 +646,22 @@ module Make (B : Backend.S) (C : Config) = struct
| LE_SetArray (re_array, e_index) ->
let*^ rm_array, env1 = expr_of_lexpr re_array |> eval_expr env in
let*^ m_index, env2 = eval_expr env1 e_index in
let m' =
let m1 =
let* v = m and* v_index = m_index and* rv_array = rm_array in
match B.v_to_int v_index with
| None -> fatal_from le (Error.UnsupportedExpr e_index)
| Some i -> B.set_index i v rv_array
in
eval_lexpr ver re_array env2 m' |: SemanticsRule.LESetArray
eval_lexpr ver re_array env2 m1 |: SemanticsRule.LESetArray
(* End *)
(* Begin LESetField *)
| LE_SetField (re_record, field_name) ->
let*^ rm_record, env1 = expr_of_lexpr re_record |> eval_expr env in
let m' =
let m1 =
let* v = m and* rv_record = rm_record in
B.set_field field_name v rv_record
in
eval_lexpr ver re_record env1 m' |: SemanticsRule.LESetField
eval_lexpr ver re_record env1 m1 |: SemanticsRule.LESetField
(* End *)
(* Begin LEDestructuring *)
| LE_Destructuring le_list ->
Expand Down Expand Up @@ -712,8 +712,8 @@ module Make (B : Backend.S) (C : Config) = struct
let eval_one env = function
(* Begin SliceSingle *)
| Slice_Single e ->
let** start, new_env = eval_expr env e in
return_normal ((start, one), new_env) |: SemanticsRule.SliceSingle
let** v_start, new_env = eval_expr env e in
return_normal ((v_start, one), new_env) |: SemanticsRule.SliceSingle
(* End *)
(* Begin SliceLength *)
| Slice_Length (e_start, e_length) ->
Expand All @@ -727,19 +727,21 @@ module Make (B : Backend.S) (C : Config) = struct
let*^ m_top, env1 = eval_expr env e_top in
let*^ m_start, new_env = eval_expr env1 e_start in
let* v_top = m_top and* v_start = m_start in
let* length = B.binop MINUS v_top v_start >>= B.binop PLUS one in
return_normal ((v_start, length), new_env) |: SemanticsRule.SliceRange
let* v_length = B.binop MINUS v_top v_start >>= B.binop PLUS one in
return_normal ((v_start, v_length), new_env) |: SemanticsRule.SliceRange
(* End *)
(* Begin SliceStar *)
| Slice_Star (e_factor, e_length) ->
let*^ m_factor, env1 = eval_expr env e_factor in
let*^ m_length, new_env = eval_expr env1 e_length in
let* v_factor = m_factor and* v_length = m_length in
let* start = B.binop MUL v_factor v_length in
return_normal ((start, v_length), new_env) |: SemanticsRule.SliceStar
let* v_start = B.binop MUL v_factor v_length in
return_normal ((v_start, v_length), new_env) |: SemanticsRule.SliceStar
(* End *)
in
fold_par_list eval_one env
(* Begin Slices *)
fold_par_list eval_one env |: SemanticsRule.Slices
(* End *)

(* Evaluation of Patterns *)
(* ---------------------- *)
Expand All @@ -761,18 +763,18 @@ module Make (B : Backend.S) (C : Config) = struct
(* End *)
(* Begin PGeq *)
| Pattern_Geq e ->
let* v' = eval_expr_sef env e in
B.binop GEQ v v' |: SemanticsRule.PGeq
let* v1 = eval_expr_sef env e in
B.binop GEQ v v1 |: SemanticsRule.PGeq
(* End *)
(* Begin PLeq *)
| Pattern_Leq e ->
let* v' = eval_expr_sef env e in
B.binop LEQ v v' |: SemanticsRule.PLeq
let* v1 = eval_expr_sef env e in
B.binop LEQ v v1 |: SemanticsRule.PLeq
(* End *)
(* Begin PNot *)
| Pattern_Not p' ->
let* b' = eval_pattern env pos v p' in
B.unop BNOT b' |: SemanticsRule.PNot
| Pattern_Not p1 ->
let* b1 = eval_pattern env pos v p1 in
B.unop BNOT b1 |: SemanticsRule.PNot
(* End *)
(* Begin PRange *)
| Pattern_Range (e1, e2) ->
Expand All @@ -787,8 +789,8 @@ module Make (B : Backend.S) (C : Config) = struct
(* End *)
(* Begin PSingle *)
| Pattern_Single e ->
let* v' = eval_expr_sef env e in
B.binop EQ_OP v v' |: SemanticsRule.PSingle
let* v1 = eval_expr_sef env e in
B.binop EQ_OP v v1 |: SemanticsRule.PSingle
(* End *)
(* Begin PMask *)
| Pattern_Mask m ->
Expand Down Expand Up @@ -826,22 +828,22 @@ module Make (B : Backend.S) (C : Config) = struct
>>= return_normal |: SemanticsRule.LDVar
(* End *)
(* Begin LDTyped *)
| LDI_Typed (ldi', _t), Some m ->
eval_local_decl s ldi' env (Some m) |: SemanticsRule.LDTyped
| LDI_Typed (ldi1, _t), Some m ->
eval_local_decl s ldi1 env (Some m) |: SemanticsRule.LDTyped
(* End *)
(* Begin LDUninitialisedTyped *)
| LDI_Typed (ldi', t), None ->
| LDI_Typed (ldi1, t), None ->
let m = base_value env t in
eval_local_decl s ldi' env (Some m)
eval_local_decl s ldi1 env (Some m)
|: SemanticsRule.LDUninitialisedTyped
(* End *)
(* Begin LDTuple *)
| LDI_Tuple ldis, Some m ->
let n = List.length ldis in
let liv = List.init n (fun i -> m >>= B.get_index i) in
let folder envm ldi' vm =
let folder envm ldi1 vm =
let**| env = envm in
eval_local_decl s ldi' env (Some vm)
eval_local_decl s ldi1 env (Some vm)
in
List.fold_left2 folder (return_normal env) ldis liv
|: SemanticsRule.LDTuple
Expand Down
20 changes: 14 additions & 6 deletions asllib/doc/ASLNotations.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,11 +10,15 @@
The notation $\rightarrowfin$ stands for a function whose domain is finite.

\begin{definition}[Function Update\label{def:FunctionUpdate}]
The notation $f[x \mapsto v]$ is the function $f$ modified so that $x$ is bound
to $v$: $f[x \mapsto v] \triangleq \lambda\ z.\ \begin{cases}
The notation $f[x \mapsto v]$ is a function identical to $f$, except that $x$ is bound
to $v$. That is, if $g = f[x \mapsto v]$ then
\[
g(z) =
\begin{cases}
f(z) & \text{if } z \neq x\\
v & \text{if } z = x \enspace .
\end{cases}$
\end{cases}
\]

The notation $\{i=1..k: a_i\mapsto b_i\}$ stands for the function formed from the corresponding input-output pairs:
$\emptyfunc[a_1\mapsto b_1]\ldots[a_k\mapsto b_k]$.
Expand Down Expand Up @@ -42,9 +46,12 @@
\paragraph{Rules}
The following notation states that when the \emph{premises} $P_{1..k}$ hold then the \emph{verdict} $V$ holds as well:
\begin{mathpar}
\inferrule{P_1 \and \ldots \and P_k}{V}
\inferrule[Name]{P_1 \and \ldots \and P_k}{V}
\end{mathpar}
That is, the premises of a rule are interpreted as a conjunction.
%
Optionally, the name of the rule, which is useful for referencing it, appears above and to the left of it.
%
The variables appearing in the premises and verdict are interpreted universally.
%
A set of rules is interpreted disjunctively. That is, each rule is used to determine whether its verdict
Expand All @@ -65,8 +72,9 @@

\paragraph{Value Deconstruction}
We will often want to deconstruct compound values to refer to their internal values.
To achieve that, we will write $v \eqname \textit{deconstructed}(v)$ where the expression on the right
exposes the internal structure of $v$, allowing us to alias its internal components.
To achieve that, we will write $v \eqname \textit{f}(u_{1..k})$ where the expression on the right
hand side exposes the internal structure of $v$, allowing us to alias its internal components
via the new variables $u_{1..k}$.
For example, suppose we know that $v$ is a pair of values.
Then, $v \eqname (a, b)$ allows us to alias $a$ and $b$.
Similarly, if $v$ is a non-empty list, then $v \eqname [h] + t$ deconstructs the list into the
Expand Down
Loading

0 comments on commit 59be792

Please sign in to comment.