Fix JS (#229)

* Add float bitwise operators * Attempt to fix LstLen/LstNth/LstSub in JS * Ignore failing test262 tests for now * Fix some JS problems * Working towards Amazon JS * Attempt to fix ByteLogic and DataView * Fix var naming in ByteLogic.gil * Add printer for `Interpreter_error` * Tweak reductions for JS * More progress in JS fix * Attempt to add IsInt formula * Add list-of-LstNth-of-LstSub reduction * Fix IntToNum conversion * Fix most Amazon JS lemmas * new z3 just dropped Signed-off-by: Sacha Ayoun <[email protected]> * Encode certain llens as uninterpreted funcs * Revert lnth-lsub-list reduction * Add as_int, as_num and is-int to JS logic * Make JS-ified predicates nounfold * Log source location with CMDs/LCMDs where possible * Add facts to JSified preds * Make more progress with Amazon JS * code cleanup Signed-off-by: Sacha Ayoun <[email protected]> * Make produce GIL assertions * Add some Int/Num reductions * Amazon JS: Add asserts from facts back into preds * Revert Amazon JS files * Raise Z3 timeout * Re-enable JS tests --------- Signed-off-by: Sacha Ayoun <[email protected]> Co-authored-by: Sacha Ayoun <[email protected]>
GillianPlatform · Apr 6, 2023 · 04d4fbf · 04d4fbf
1 parent f9df486
commit 04d4fbf
Show file tree

Hide file tree

Showing 50 changed files with 1,438 additions and 1,139 deletions.
diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
@@ -109,69 +109,69 @@ jobs:
         run: "make"
         working-directory: "Gillian/Gillian-C/examples/amazon/"
 
-  # gillian_js_tests:
-  #   strategy:
-  #     matrix:
-  #       operating-system: [macos-latest, ubuntu-latest]
-  #   runs-on: ${{ matrix.operating-system }}
-  #   needs: build
-  #   steps:
-  #     - name: download release
-  #       uses: actions/download-artifact@v3
-  #       with:
-  #         name: ${{ runner.os }}-release
-  #         path: release
-  #     - name: setting up node
-  #       uses: actions/setup-node@v3
-  #       with:
-  #         node-version: ${{ env.NODE_VERSION }}
-  #     - name: install release
-  #       run: |
-  #         yarn global add file://$(pwd)/release
-  #         echo "$(yarn global bin)" >> $GITHUB_PATH
-  #     - name: checkout project
-  #       uses: actions/checkout@v3
-  #       with:
-  #         path: Gillian
-  #     - name: init env
-  #       run: "Gillian-JS/scripts/setup_environment.sh"
-  #       working-directory: "Gillian"
-  #     - name: Test JaVerT
-  #       run: "./testJaVerT.sh"
-  #       working-directory: "Gillian/Gillian-JS/environment/"
-  #     - name: Test Amazon
-  #       run: "make"
-  #       working-directory: "Gillian/Gillian-JS/Examples/Amazon/"
+  gillian_js_tests:
+    strategy:
+      matrix:
+        operating-system: [macos-latest, ubuntu-latest]
+    runs-on: ${{ matrix.operating-system }}
+    needs: build
+    steps:
+      - name: download release
+        uses: actions/download-artifact@v3
+        with:
+          name: ${{ runner.os }}-release
+          path: release
+      - name: setting up node
+        uses: actions/setup-node@v3
+        with:
+          node-version: ${{ env.NODE_VERSION }}
+      - name: install release
+        run: |
+          yarn global add file://$(pwd)/release
+          echo "$(yarn global bin)" >> $GITHUB_PATH
+      - name: checkout project
+        uses: actions/checkout@v3
+        with:
+          path: Gillian
+      - name: init env
+        run: "Gillian-JS/scripts/setup_environment.sh"
+        working-directory: "Gillian"
+      - name: Test JaVerT
+        run: "./testJaVerT.sh"
+        working-directory: "Gillian/Gillian-JS/environment/"
+      # - name: Test Amazon
+      #   run: "make"
+      #   working-directory: "Gillian/Gillian-JS/Examples/Amazon/"
 
-  # test262:
-  #   if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master')
-  #   strategy:
-  #     matrix:
-  #       operating-system: [macos-latest]
-  #   runs-on: ${{ matrix.operating-system }}
-  #   needs: build
-  #   steps:
-  #     - name: download release
-  #       uses: actions/download-artifact@v3
-  #       with:
-  #         name: ${{ runner.os }}-release
-  #         path: release
-  #     - name: setting up node
-  #       uses: actions/setup-node@v3
-  #       with:
-  #         node-version: ${{ env.NODE_VERSION }}
-  #     - name: install release
-  #       run: |
-  #         yarn global add file://$(pwd)/release
-  #         echo "$(yarn global bin)" >> $GITHUB_PATH
-  #     - name: checkout project
-  #       uses: actions/checkout@v3
-  #       with:
-  #         repository: GillianPlatform/javert-test262
-  #         path: test262
-  #         ref: 93e0d0b04093cabc3234a776eec5cc3e165f3b1a
-  #     - name: Test262
-  #       run: "gillian-js test262 test262/test --ci"
+  test262:
+    if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master')
+    strategy:
+      matrix:
+        operating-system: [macos-latest]
+    runs-on: ${{ matrix.operating-system }}
+    needs: build
+    steps:
+      - name: download release
+        uses: actions/download-artifact@v3
+        with:
+          name: ${{ runner.os }}-release
+          path: release
+      - name: setting up node
+        uses: actions/setup-node@v3
+        with:
+          node-version: ${{ env.NODE_VERSION }}
+      - name: install release
+        run: |
+          yarn global add file://$(pwd)/release
+          echo "$(yarn global bin)" >> $GITHUB_PATH
+      - name: checkout project
+        uses: actions/checkout@v3
+        with:
+          repository: GillianPlatform/javert-test262
+          path: test262
+          ref: 93e0d0b04093cabc3234a776eec5cc3e165f3b1a
+      - name: Test262
+        run: "gillian-js test262 test262/test --ci"
 
   collections-c:
     if: ( github.event_name == 'pull_request') && ( github.base_ref == 'master')

diff --git a/.gitignore b/.gitignore
@@ -56,6 +56,8 @@ racket/compiled
 *.aux
 *.out
 *.log
+*.log.zip
+/*.gil
 tutorial/main.pdf
 
 # esy + docker stuff

diff --git a/Gillian-C/examples/amazon/header.c b/Gillian-C/examples/amazon/header.c
@@ -594,6 +594,7 @@ int aws_cryptosdk_hdr_parse(struct aws_cryptosdk_hdr *hdr,
             valid_aws_byte_cursor_ptr(#cur, #restLength, #cbptr, #restEDKsAndRest) * \
             valid_edk_array_list_ptr(#edk_al, #alloc, #acc) * \
             (len #acc == #i) * (#eList == #acc @ #restEDKs) * \
+            (#i <=# #edk_count) * \
             Elements(#edkDef, #restEDKsAndRest, 0, #rest_count, 3, #restEDKs, #restEDKLength) * \
             (#restLength == len #restEDKsAndRest) * \
             (#rest_count == (#edk_count - #i)) * \

diff --git a/Gillian-JS/lib/Compiler/JS2JSIL_Compiler.ml b/Gillian-JS/lib/Compiler/JS2JSIL_Compiler.ml
@@ -607,9 +607,9 @@ let translate_binop_equality _ _ x1_v x2_v non_strict non_negated err =
 let translate_bitwise_bin_op x1 x2 x1_v x2_v bbop err =
   let bbop : BinOp.t =
     match bbop with
-    | JS_Parser.Syntax.Bitand -> BitwiseAnd
-    | JS_Parser.Syntax.Bitor -> BitwiseOr
-    | JS_Parser.Syntax.Bitxor -> BitwiseXor
+    | JS_Parser.Syntax.Bitand -> BitwiseAndF
+    | JS_Parser.Syntax.Bitor -> BitwiseOrF
+    | JS_Parser.Syntax.Bitxor -> BitwiseXorF
     | _ -> raise (Failure "Illegal bitwise operator")
   in
 
@@ -3064,7 +3064,7 @@ let rec translate_expr tr_ctx e :
 
       let new_cmds, new_errs, x_r =
         translate_bitwise_shift x1 x2 x1_v x2_v toInt32Name toUInt32Name
-          LeftShift tr_ctx.tr_err_lab
+          LeftShiftF tr_ctx.tr_err_lab
       in
       let cmds =
         annotate_first_cmd
@@ -3103,7 +3103,7 @@ let rec translate_expr tr_ctx e :
 
       let new_cmds, new_errs, x_r =
         translate_bitwise_shift x1 x2 x1_v x2_v toInt32Name toUInt32Name
-          SignedRightShift tr_ctx.tr_err_lab
+          SignedRightShiftF tr_ctx.tr_err_lab
       in
       let cmds =
         annotate_first_cmd
@@ -3142,7 +3142,7 @@ let rec translate_expr tr_ctx e :
 
       let new_cmds, new_errs, x_r =
         translate_bitwise_shift x1 x2 x1_v x2_v toUInt32Name toUInt32Name
-          UnsignedRightShift tr_ctx.tr_err_lab
+          UnsignedRightShiftF tr_ctx.tr_err_lab
       in
       let cmds =
         annotate_first_cmd
@@ -3863,13 +3863,13 @@ let rec translate_expr tr_ctx e :
             translate_multiplicative_binop x1 x2 x1_v x2_v op tr_ctx.tr_err_lab
         | JS_Parser.Syntax.Ursh ->
             translate_bitwise_shift x1 x2 x1_v x2_v toUInt32Name toUInt32Name
-              SignedRightShift tr_ctx.tr_err_lab
+              SignedRightShiftF tr_ctx.tr_err_lab
         | JS_Parser.Syntax.Lsh ->
             translate_bitwise_shift x1 x2 x1_v x2_v toInt32Name toUInt32Name
-              LeftShift tr_ctx.tr_err_lab
+              LeftShiftF tr_ctx.tr_err_lab
         | JS_Parser.Syntax.Rsh ->
             translate_bitwise_shift x1 x2 x1_v x2_v toInt32Name toUInt32Name
-              UnsignedRightShift tr_ctx.tr_err_lab
+              UnsignedRightShiftF tr_ctx.tr_err_lab
         | JS_Parser.Syntax.Bitand
         | JS_Parser.Syntax.Bitor
         | JS_Parser.Syntax.Bitxor ->
-Original file line number
+Diff line change
@@ Expand Up / @@ -56,6 +56,8 @@ racket/compiled @@
     *.aux
     *.out
     *.log
+    *.log.zip
+    /*.gil
     tutorial/main.pdf
     # esy + docker stuff
@@ Expand Down @@