Refactor: Using values of `Smtml` #128

julianayang777 · 2024-06-19T13:19:06Z

Changes

Operators exp, random, typeof and tuple related operators were removed from syntax and became external functions.
The values used by ECMA-SL (Val.ml) were changed to the values of Smtml. In the next code snippet, you can see how it was converted:

type t =
  | Null (* -> App "null" [] *)
  | Void (* -> App "void" [] *)
  | Int of int (* -> Int *)
  | Flt of (float[@unboxed]) (* -> Real *)
  | Str of string  (* -> Str *)
  | Bool of bool  (* -> True | False *)
  | Symbol of string (* -> App "symbol" [Str s] *)
  | Loc of Lo. c.t (* -> App "loc" [Int l] *)
  | Arr of t array (* int (pointer to array) *)
  | List of t list (* -> List l *)
  | Tuple of t list (* -> List l *)
  | Byte of int (* Int *)
  | Type of Type.t  
    (* -> App t [] *) 
    (* t := "NullType" | "IntType"    | "RealType" | "StrType" 
          | "BoolType" | "SymbolType" | "LocType"  | "ListType" 
          | "TupleType"| "CurryType" *)
  | Curry of string * t list  (* -> App fn fvs *)

When converting bitwise operators, I already take into consideration issue Bitwise operations should not be defined over floats #93. That means that the bitwise operators is already defined over integers.
I moved the custom pp function that was defined in Val.ml to EExpr.ml so that I could delete Val.ml. (But this might be the best approach😕).

Concrete Interpreter

In the concrete execution, all the tests passed using the command dune runtest. However, for the test262 suite, some tests are still failing. To fix it, we might change the ecmaref. (for instance, some of the tests failed due to change 3)

Symbolic Interpreter

In the symbolic execution, the tests are not passing, which might be due to the way we have defined the symbol undefined. And the way of handling error in symbolic_value.ml can be improved, because for now I have just put failwith.

julianayang777 · 2024-06-19T13:29:28Z

cc @andreffnascimento

filipeom

I haven't seen everything. But the more I see. The more I think we should use Smtml.Expr.Ptr for locations. I'm going to fix Ptr so that we can apply it here more easily.

I'll review more during the day

ECMA-SL/semantics/core/concrete/eval_op.ml

filipeom

More reviews, could you also change the smtml pin to commit ff3c34ad926f7b4329fe7412fe31d270c7b2220b?

ECMA-SL/semantics/core/functorial/symbolic_extern.ml

filipeom · 2024-06-23T09:52:58Z

ECMA-SL/semantics/core/functorial/symbolic_value.ml

+
+  let equal (e1 : value) (e2 : value) : bool = E.equal e1 e2 [@@inline]
+  let hash (e : value) = E.hash e [@@inline]
+  let compare (e1 : value) (e2 : value) = compare (hash e1) (hash e2)


compare should probably be defined in Smtml and we just use that

ECMA-SL/semantics/core/functorial/symbolic_value.ml

ECMA-SL/semantics/core/parser/parser.mly

filipeom · 2024-06-24T19:06:15Z

JS-Interpreters/ecmaref5/section 15/section_15.7.esl

@@ -327,11 +327,11 @@ function NumberPrototypeToFixedAlt(global, this, strict, items) {
        z := "";
        counter := 0;
        while (!(counter <= (f - k))) {
-          z := s_concat(z, "0");
+          z := s_concat[z, "0"];


s_concat receives a list as parameter?

Suggested change

z := s_concat[z, "0"];

z := s_concat [z, "0"];

I know for parsing it's all the same, but adding a space would make this look better

s_concat receives a list as parameter?

Yes, I think s_concat already received a list as parameter before the change.
Maybe, in this case it was receiving a tuple instead of a list? Because I didn't change the semantics of the s_concat, it is still an unary operator.

Indeed, it might have been receiving a tuple. I don't know how this worked. But it was on ecmaref5 which supposedly we're not going to maintain?

Indeed, it might have been receiving a tuple. I don't know how this worked. But it was on ecmaref5 which supposedly we're not going to maintain?

The idea is to stop maintaining the ECMARef5, yes

filipeom

Can you run dune fmt just to verify that everything is well formatted? Otherwise, I think I'm done.

JS-Interpreters/ecmaref6/section 8/section_8.1.esl

filipeom · 2024-06-24T19:19:11Z

@andreffnascimento This will probably break some tests for test262. But I'd rather not wait long to merge this as it is a monster PR 😅 and I want to catch the bugs earlier rather than later. If you can also just see if there is anything you'd like to change before we merge.

@julianayang777 Could you rebase on main and add the description of changes you provided here to CHANGES.md?

julianayang777 · 2024-06-24T21:05:08Z

Can you run dune fmt just to verify that everything is well formatted? Otherwise, I think I'm done.

Ok, maybe it's better to do it after André has done the review.

andreffnascimento

I'm done with my review. I'm going to approve this, so that you can merge this soon, but first take I look at my comments/proposals. I'm not going to merge #129 until this is done to avoid introducing extra merge conflicts. Also, I can run the entire Test262 to see how we are doing, but only after we are passing the CI. Btw, here is a link with the previous test results

ECMA-SL/semantics/core/concrete/eval_op.ml

ECMA-SL/syntax/extended/eExpr.ml

andreffnascimento · 2024-06-24T16:29:15Z

JS-Interpreters/ecmaref5/section 8/section_8.esl

+      if (el = "R") { return "Reference" }
+      elif (el = "C") { return "Completion" }
+      elif (el = "P") { return "PropertyIdentifier" }
+      else { return "List" }


@filipeom how sure are we that this is not going to break?? 😅
If we evaluate a list where the first element matches one of these cases, we will not get the correct type right? This used to be fine since tuples were only used internally, never in the JS AST, now I'm not sure

@filipeom how sure are we that this is not going to break?? 😅

I'm confident it will break at some point 😅

If we evaluate a list where the first element matches one of these cases, we will not get the correct type right? This used to be fine since tuples were only used internally, never in the JS AST, now I'm not sure

Exactly. That's why I believe the completions and objects we return in lists should be something else. Since they are never extended, we could use esl arrays, which are simply OCaml arrays. Besides allowing O(1) read/write operations, they would also be more memory efficient. We could use this efficiency to add metadata in the initial element of the array, such as a unique location to a global object used only when building these completion arrays.

For example, in this function, we would know exactly what we have instead of hoping the list is as expected. I asked Juliana to open an issue about this here: #132. I think we can implement this without compromising the similarity of ecmaref to the standard.

andreffnascimento · 2024-06-24T17:03:39Z

ECMA-SL/semantics/extended/parser/eParser.mly

+  | t = dtype_target;    { Value.App (`Op t, []) }

 let dtype_target :=
-  | DTYPE_NULL;         { Type.NullType }
-  | DTYPE_INT;          { Type.IntType }
-  | DTYPE_FLT;          { Type.FltType }
-  | DTYPE_STR;          { Type.StrType }
-  | DTYPE_BOOL;         { Type.BoolType }
-  | DTYPE_SYMBOL;       { Type.SymbolType }
-  | DTYPE_LOC;          { Type.LocType }
-  | DTYPE_LIST;         { Type.ListType }
-  | DTYPE_TUPLE;        { Type.TupleType }
-  | DTYPE_CURRY;        { Type.CurryType }
+  | DTYPE_NULL;          { "NullType" }
+  | DTYPE_INT;           { "IntType" }
+  | DTYPE_FLT;           { "FltType" }
+  | DTYPE_STR;           { "StrType" }
+  | DTYPE_BOOL;          { "BoolType" }
+  | DTYPE_SYMBOL;        { "SymbolType" }
+  | DTYPE_LOC;           { "LocType" }
+  | DTYPE_LIST;          { "ListType" }
+  | DTYPE_TUPLE;         { "TupleType" }
+  | DTYPE_CURRY;         { "CurryType" }


I don't have a very strong opinion on this, so we can leave it as it is (specially because this may break things / slow things down). But shouldn't these types be stored as: Value.App (`Op "type", ["null"]. I mean, it looks more consistent, but I'm not sure it is worth it. Opinions @filipeom @julianayang777

I agree that it looks more consistent, but yes, in both cases we will break things.

I agree that it looks more consistent. It also might help in pattern matching situations? For the solver it's all the same. Value applications are unitary so the strings in the list will be concatenated with the string in Op to make an uninterpreted symbol.

So we can probably do it and optimize later

Ok, I will not change now because I am not sure if it will influence my other branch merge. However, I will make the change in the next PR for branch merge.

andreffnascimento · 2024-06-25T10:17:08Z

JS-Interpreters/ecmaref5/section 15/section_15.7.esl

@@ -327,11 +327,11 @@ function NumberPrototypeToFixedAlt(global, this, strict, items) {
        z := "";
        counter := 0;
        while (!(counter <= (f - k))) {
-          z := s_concat(z, "0");
+          z := s_concat[z, "0"];


Indeed, it might have been receiving a tuple. I don't know how this worked. But it was on ecmaref5 which supposedly we're not going to maintain?

The idea is to stop maintaining the ECMARef5, yes

filipeom · 2024-06-25T11:44:13Z

I can run the entire Test262 to see how we are doing, but only after we are passing the CI.

@julianayang777 I'll just make dune runtest ignore symbolic tests for now. Its better to have the CI catch other failing tests and not be polluted by se related failures that are know to not be working

- At this stage, the symbolic interpreter does not work for now using Encoding values instaed of val - At this stage, the symbolic interpreter does not work for now restore value `Loc`

Fixes most of the type errors reported by the typechecker while also trying to use more ternary operators to reduce branching. And, forces ecmaref6 compilation test to use typechecker.

This will reduce the number of rules dune produces from 750k to 10k. Will not make compilation faster but it does make dune more responsive.

andreffnascimento · 2024-06-25T16:22:57Z

Can we merge this?

julianayang777 · 2024-06-25T16:37:15Z

Can we merge this?

For me, yes

julianayang777 requested review from filipeom and andreffnascimento and removed request for filipeom and andreffnascimento June 19, 2024 13:19

filipeom reviewed Jun 20, 2024

View reviewed changes

ECMA-SL/semantics/core/concrete/eval_op.ml Outdated Show resolved Hide resolved

julianayang777 added a commit that referenced this pull request Jun 22, 2024

address PR #128 review

881a461

filipeom reviewed Jun 23, 2024

View reviewed changes

julianayang777 added a commit that referenced this pull request Jun 24, 2024

address PR #128 review - 2

e10eb8a

filipeom reviewed Jun 24, 2024

View reviewed changes

filipeom approved these changes Jun 24, 2024

View reviewed changes

JS-Interpreters/ecmaref6/section 8/section_8.1.esl Show resolved Hide resolved

julianayang777 mentioned this pull request Jun 24, 2024

Use static arrays instead of lists in some cases #132

Closed

andreffnascimento approved these changes Jun 25, 2024

View reviewed changes

filipeom and others added 13 commits June 25, 2024 12:51

Pin latest smtml

b207745

using Encoding values instaed of val

8acf6a9

- At this stage, the symbolic interpreter does not work for now using Encoding values instaed of val - At this stage, the symbolic interpreter does not work for now restore value `Loc`

restore some functions

e2e8c3e

refactor array implementation

d5bfe3c

remove random from syntax

df9cf8a

remove exp from syntax

22be8c3

remove typeof from syntax (incomplete - Tuple)

ed275ee

remove tuple operators from syntax + fix ecamref

347eb23

refactor treating error + add pp for Smtml.Value.t

ed9db6d

fix ecmaref5

aa21f50

fix ecmaref5

b108018

promote tests

7b397df

fix small bug

c469cc6

julianayang777 and others added 13 commits June 25, 2024 12:51

operator type error treating

48982a5

small fixes on eval_op and use customized pp for Smtml.Value.t

ad46a43

catching indexOutOfBounds + fix logical binop + fmt

16fdb42

start to refactor symb values to smtml expr

ebf5ca8

add typeof and fix undefined

cacd07b

add exp as external and complete StringConcat ListConcat

af3b1b2

Fixes type errors in ecmaref6 (Closes #106)

f6cddfb

Fixes most of the type errors reported by the typechecker while also trying to use more ternary operators to reduce branching. And, forces ecmaref6 compilation test to use typechecker.

cleanup unused files and error handling in concrete interpreter

0f36ea4

fix some operators in symbolic interpreter

798d692

address PR #128 review

4dd84b5

address PR #128 review - 2

094ed3b

address PR #128 review - 3

ecf34ea

update Changes.md and fmt

2deacaf

julianayang777 force-pushed the refactor-symbval branch from e10eb8a to 2deacaf Compare June 25, 2024 12:38

filipeom added 3 commits June 25, 2024 15:44

Update smtml pin

d91506b

Update ocamlformat version and ignore symbolic tests

7d6543f

Do not scan unecessary directories with dune

fc7dbe6

This will reduce the number of rules dune produces from 750k to 10k. Will not make compilation faster but it does make dune more responsive.

filipeom force-pushed the refactor-symbval branch from 568387f to fc7dbe6 Compare June 25, 2024 13:58

filipeom merged commit 3492447 into main Jun 25, 2024
2 checks passed

filipeom pushed a commit that referenced this pull request Jun 25, 2024

address PR #128 review

ebcd35d

filipeom pushed a commit that referenced this pull request Jun 25, 2024

address PR #128 review - 2

655df01

filipeom pushed a commit that referenced this pull request Jun 25, 2024

address PR #128 review - 3

4d00229

filipeom deleted the refactor-symbval branch June 25, 2024 16:41

andreffnascimento mentioned this pull request Jun 26, 2024

General improvements to the ECMA-SL syntax #133

Merged

4 tasks

andreffnascimento mentioned this pull request Jul 24, 2024

Refactor ECMA-SL Operators to Use External Functions #146

Merged

filipeom pushed a commit that referenced this pull request Dec 27, 2024

address PR #128 review

a08ca62

filipeom pushed a commit that referenced this pull request Dec 27, 2024

address PR #128 review - 2

c00c951

filipeom pushed a commit that referenced this pull request Dec 27, 2024

address PR #128 review - 3

d4e2bab

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Refactor: Using values of `Smtml` #128

Refactor: Using values of `Smtml` #128

julianayang777 commented Jun 19, 2024

julianayang777 commented Jun 19, 2024

filipeom left a comment

filipeom left a comment

filipeom Jun 23, 2024

filipeom Jun 24, 2024

julianayang777 Jun 24, 2024 •

edited

Loading

filipeom Jun 25, 2024

andreffnascimento Jun 25, 2024

filipeom left a comment

filipeom commented Jun 24, 2024 •

edited

Loading

julianayang777 commented Jun 24, 2024

andreffnascimento left a comment

andreffnascimento Jun 24, 2024

filipeom Jun 25, 2024

andreffnascimento Jun 24, 2024

julianayang777 Jun 25, 2024

filipeom Jun 25, 2024 •

edited

Loading

julianayang777 Jun 25, 2024

andreffnascimento Jun 25, 2024

filipeom commented Jun 25, 2024

andreffnascimento commented Jun 25, 2024

julianayang777 commented Jun 25, 2024

Refactor: Using values of Smtml #128

Refactor: Using values of Smtml #128

Conversation

julianayang777 commented Jun 19, 2024

Changes

Concrete Interpreter

Symbolic Interpreter

julianayang777 commented Jun 19, 2024

filipeom left a comment

Choose a reason for hiding this comment

filipeom left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

julianayang777 Jun 24, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

filipeom left a comment

Choose a reason for hiding this comment

filipeom commented Jun 24, 2024 • edited Loading

julianayang777 commented Jun 24, 2024

andreffnascimento left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

filipeom Jun 25, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

filipeom commented Jun 25, 2024

andreffnascimento commented Jun 25, 2024

julianayang777 commented Jun 25, 2024

Refactor: Using values of `Smtml` #128

Refactor: Using values of `Smtml` #128

julianayang777 Jun 24, 2024 •

edited

Loading

filipeom commented Jun 24, 2024 •

edited

Loading

filipeom Jun 25, 2024 •

edited

Loading