Makefile cleanup, fix display in browser, implement more endian-ness …

…functions

kremlib/js/browser.js

@@ -4,9 +4,9 @@
 var my_print;
 
 function kremlin_start () {
-  my_print = msg =>
+  my_print = (...msg) =>
     document.getElementById("terminal").appendChild(
-      document.createTextNode(msg+"\n"));
+      document.createTextNode(msg.join(" ")+"\n"));
 
   if (!("WebAssembly" in this))
     my_print("Error: WebAssembly not enabled. Use Chrome Canary?");

runtime/WasmSupport.fst

@@ -2,6 +2,8 @@ module WasmSupport
 
 open FStar.HyperStack.ST
 
+module C = FStar.Int.Cast
+module I64 = FStar.Int64
 module U32 = FStar.UInt32
 module U64 = FStar.UInt64
 
@@ -26,6 +28,8 @@ let check_buffer_size (s: U32.t): Stack unit (fun _-> True) (fun _ _ _ -> True)
   if U32.( s =^ 0ul ) then
     trap ()
 
+(* TODO: all of these functions are copy-pastes from whatever is written in
+ * kremlib.h. They OUGHT TO BE implement in F*! *)
 let eq_mask64 (x y: U64.t) =
   let open FStar.UInt64 in
   let x = lognot (logand x y) in
@@ -37,9 +41,6 @@ let eq_mask64 (x y: U64.t) =
   let x = shift_left x 1ul in
   FStar.Int64.( shift_right (FStar.Int.Cast.uint64_to_int64 x) 63ul )
 
-module C = FStar.Int.Cast
-module I64 = FStar.Int64
-
 let gte_mask64 (x y: U64.t) =
   let low63 = U64.lognot (C.int64_to_uint64 (I64.shift_right
     (I64.sub
@@ -54,3 +55,15 @@ let gte_mask64 (x y: U64.t) =
     63ul))
   in
   U64.logand low63 high_bit
+
+let betole32 (x: U32.t) =
+  let open U32 in
+  logor (logor (logor (logand (shift_right x 24ul) 0x000000FFul)
+    (logand (shift_right x 8ul) 0x0000FF00ul))
+    (logand (shift_left x 8ul) 0x00FF0000ul))
+    (logand (shift_left x 24ul) 0xFF000000ul)
+
+let betole64 (x: U64.t) =
+  let low = C.uint32_to_uint64 (betole32 (C.uint64_to_uint32 x)) in
+  let high = C.uint32_to_uint64 (betole32 (C.uint64_to_uint32 (U64.shift_right x 32ul))) in
+  U64.logor (U64.shift_left low 32ul) high

src/CFlatToWasm.ml

@@ -47,7 +47,7 @@ let find_global env name =
  * removed... *)
 let builtins = [
   "FStar_UInt64_eq_mask", "WasmSupport_eq_mask64";
-  "FStar_UInt64_gte_mask", "WasmSupport_gte_mask64"
+  "FStar_UInt64_gte_mask", "WasmSupport_gte_mask64";
 ]
 
 let name_of_string = W.Utf8.decode
@@ -64,10 +64,14 @@ let rec find_func env name =
 
 let primitives = [
   "load32_le";
+  "load32_be";
   "load64_le";
+  "load64_be";
   "load128_le";
   "store32_le";
+  "store32_be";
   "store64_le";
+  "store64_be";
   "store128_le"
 ]
 
@@ -620,10 +624,16 @@ and mk_expr env (e: expr): W.Ast.instr list =
       mk_expr env e @
       [ dummy_phrase W.Ast.(Load { ty = mk_type I32; align = 0; offset = 0l; sz = None })]
 
+  | CallFunc ("load32_be", [ e ]) ->
+      mk_expr env (CallFunc ("WasmSupport_betole32", [ CallFunc ("load32_le", [ e ])]))
+
   | CallFunc ("load64_le", [ e ]) ->
       mk_expr env e @
       [ dummy_phrase W.Ast.(Load { ty = mk_type I64; align = 0; offset = 0l; sz = None })]
 
+  | CallFunc ("load64_be", [ e ]) ->
+      mk_expr env (CallFunc ("WasmSupport_betole64", [ CallFunc ("load64_le", [ e ])]))
+
   | CallFunc ("store128_le", [ dst; src ])
   | CallFunc ("load128_le", [ src; dst ]) ->
       let fst64 = env.n_args + 2 in
@@ -656,12 +666,18 @@ and mk_expr env (e: expr): W.Ast.instr list =
       [ dummy_phrase W.Ast.(Store { ty = mk_type I32; align = 0; offset = 0l; sz = None })] @
       mk_unit
 
+  | CallFunc ("store32_be", [ e1; e2 ]) ->
+      mk_expr env (CallFunc ("store32_le", [ e1; CallFunc ("WasmSupport_betole32", [ e2 ])]))
+
   | CallFunc ("store64_le", [ e1; e2 ]) ->
       mk_expr env e1 @
       mk_expr env e2 @
       [ dummy_phrase W.Ast.(Store { ty = mk_type I64; align = 0; offset = 0l; sz = None })] @
       mk_unit
 
+  | CallFunc ("store64_be", [ e1; e2 ]) ->
+      mk_expr env (CallFunc ("store64_le", [ e1; CallFunc ("WasmSupport_betole64", [ e2 ])]))
+
   | CallFunc (name, es) ->
       KList.map_flatten (mk_expr env) es @
       [ dummy_phrase (W.Ast.Call (mk_var (find_func env name))) ]

test/Makefile

@@ -75,11 +75,8 @@ hello-system/HelloSystem.exe: EXTRA = -add-include '"system.h"' \
 %.wasm: %.krml $(KRML_BIN)
 	$(KRML) $(EXTRA) -tmpdir $(subst .wasm,.out,$@) $(JSFILES) -no-prefix $(notdir $*) $<
 	cd $*.out && \
-	  if ! $(NEGATIVE); then \
-	    $(shell which d8) --allow-natives-syntax main.js; \
-	  else \
-	    ! $(shell which d8) --allow-natives-syntax main.js; \
-	  fi && \
+	  if ! $(NEGATIVE); then $(shell which d8) main.js; \
+	  else ! $(shell which d8) main.js; fi && \
 	  cd .. && cp $*.out/$(subst .,_,$(notdir $(basename $@))).wasm $@
 	# cd $*.out && ch -Wasm main.js
 
@@ -90,33 +87,34 @@ WasmTrap.wasm: NEGATIVE = true
 
 # External WASM targets: recycle the HACL* Makefile!
 HACL_DROP=Prims,Hacl.UInt8,Hacl.UInt16,Hacl.UInt32,Hacl.UInt64,Hacl.UInt128,Hacl.Endianness,Hacl.Cast,Hacl.Spec.*,Spec.*,Seq.*
-$(SALSA)/Hacl.Test.Chacha20.wasm: EXTRA+=-drop $(HACL_DROP) \
-  -bundle 'Chacha20=Hacl.Impl.*,Chacha20,Hacl.Lib.*'
 
 .PHONY: $(SALSA)/Hacl.Test.Chacha20.krml
 $(SALSA)/Hacl.Test.Chacha20.krml:
 	KREMLIN_ARGS=-wasm $(MAKE) -C $(SALSA) chacha-c/out.krml
 	[ -e $(subst .krml,.out,$@) ] || ln -sf $(SALSA)/chacha-c $(subst .krml,.out,$@)
 	cp $(subst .krml,.out,$@)/out.krml $@
 
-$(CURVE)/Hacl.Test.X25519.wasm: EXTRA+=-drop $(HACL_DROP) \
-  -bundle 'Curve25519=Hacl.Bignum,Hacl.Bignum.*,Hacl.EC,Hacl.EC.*'
+$(SALSA)/Hacl.Test.Chacha20.wasm: EXTRA+=-drop $(HACL_DROP) \
+  -bundle 'Chacha20=Hacl.Impl.*,Chacha20,Hacl.Lib.*'
 
 .PHONY: $(CURVE)/Hacl.Test.X25519.krml
 $(CURVE)/Hacl.Test.X25519.krml:
 	KREMLIN_ARGS=-wasm $(MAKE) -C $(CURVE) extract-c
 	[ -e $(subst .krml,.out,$@) ] || ln -sf $(CURVE)/x25519-c $(subst .krml,.out,$@)
 	cp $(subst .krml,.out,$@)/out.krml $@
 
-$(POLY)/Hacl.Test.Poly1305_64.wasm: EXTRA+=-drop $(HACL_DROP) \
-  -bundle 'Poly1305_64=Hacl.Bignum.*,Hacl.Impl.*,Hacl.Standalone.*,Poly1305_64' \
-  -drop AEAD_Poly1305_64
+$(CURVE)/Hacl.Test.X25519.wasm: EXTRA+=-drop $(HACL_DROP) \
+  -bundle 'Curve25519=Hacl.Bignum,Hacl.Bignum.*,Hacl.EC,Hacl.EC.*'
 
 .PHONY: $(POLY)/Hacl.Test.Poly1305_64.krml
 $(POLY)/Hacl.Test.Poly1305_64.krml:
 	KREMLIN_ARGS=-wasm $(MAKE) -C $(POLY) poly-c/out.krml
 	[ -e $(subst .krml,.out,$@) ] || ln -sf $(POLY)/poly-c $(subst .krml,.out,$@)
 	cp $(subst .krml,.out,$@)/out.krml $@
 
+$(POLY)/Hacl.Test.Poly1305_64.wasm: EXTRA+=-drop $(HACL_DROP) \
+  -bundle 'Poly1305_64=Hacl.Bignum.*,Hacl.Impl.*,Hacl.Standalone.*,Poly1305_64' \
+  -drop AEAD_Poly1305_64
+
 clean:
 	rm -rf *.exe *.dSYM *.out *.wasm *.krml