@@ -189,7 +189,9 @@ let check_vec_binop binop at =
189189 error at " invalid lane index"
190190 | _ -> ()
191191
192- let check_memop (c : context ) (memop : ('t, 's) memop ) ty_size get_sz at =
192+ type mem_mode = NonAtomic | Atomic
193+
194+ let check_memop (mode : mem_mode ) (c : context ) (memop : ('t, 's) memop ) ty_size get_sz at =
193195 let _mt = memory c (0l @@ at) in
194196 let size =
195197 match get_sz memop.pack with
@@ -198,8 +200,13 @@ let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
198200 check_pack sz (ty_size memop.ty) at;
199201 packed_size sz
200202 in
201- require (1 lsl memop.align < = size) at
202- " alignment must not be larger than natural"
203+ match mode with
204+ | NonAtomic ->
205+ require (1 lsl memop.align < = size) at
206+ " alignment must not be larger than natural" ;
207+ | Atomic ->
208+ require (1 lsl memop.align = size) at
209+ " atomic alignment must be natural"
203210
204211
205212(*
@@ -354,29 +361,29 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
354361 [] --> []
355362
356363 | Load memop ->
357- check_memop c memop num_size (Lib.Option. map fst) e.at;
364+ check_memop NonAtomic c memop num_size (Lib.Option. map fst) e.at;
358365 [NumType I32Type ] --> [NumType memop.ty]
359366
360367 | Store memop ->
361- check_memop c memop num_size (fun sz -> sz) e.at;
368+ check_memop NonAtomic c memop num_size (fun sz -> sz) e.at;
362369 [NumType I32Type ; NumType memop.ty] --> []
363370
364371 | VecLoad memop ->
365- check_memop c memop vec_size (Lib.Option. map fst) e.at;
372+ check_memop NonAtomic c memop vec_size (Lib.Option. map fst) e.at;
366373 [NumType I32Type ] --> [VecType memop.ty]
367374
368375 | VecStore memop ->
369- check_memop c memop vec_size (fun _ -> None ) e.at;
376+ check_memop NonAtomic c memop vec_size (fun _ -> None ) e.at;
370377 [NumType I32Type ; VecType memop.ty] --> []
371378
372379 | VecLoadLane (memop , i ) ->
373- check_memop c memop vec_size (fun sz -> Some sz) e.at;
380+ check_memop NonAtomic c memop vec_size (fun sz -> Some sz) e.at;
374381 require (i < vec_size memop.ty / packed_size memop.pack) e.at
375382 " invalid lane index" ;
376383 [NumType I32Type ; VecType memop.ty] --> [VecType memop.ty]
377384
378385 | VecStoreLane (memop , i ) ->
379- check_memop c memop vec_size (fun sz -> Some sz) e.at;
386+ check_memop NonAtomic c memop vec_size (fun sz -> Some sz) e.at;
380387 require (i < vec_size memop.ty / packed_size memop.pack) e.at
381388 " invalid lane index" ;
382389 [NumType I32Type ; VecType memop.ty] --> []
@@ -514,23 +521,23 @@ let rec check_instr (c : context) (e : instr) (s : infer_result_type) : op_type
514521 " invalid lane index" ;
515522 [t; NumType t2] --> [t]
516523 | MemoryAtomicWait atomicop ->
517- check_memop c atomicop num_size (fun sz -> sz) e.at;
524+ check_memop Atomic c atomicop num_size (fun sz -> sz) e.at;
518525 [NumType I32Type ; NumType atomicop.ty; NumType I64Type ] --> [NumType I32Type ]
519526 | MemoryAtomicNotify atomicop ->
520- check_memop c atomicop num_size (fun sz -> sz) e.at;
527+ check_memop Atomic c atomicop num_size (fun sz -> sz) e.at;
521528 [NumType I32Type ; NumType I32Type ] --> [NumType I32Type ]
522529 | AtomicFence -> [] --> []
523530 | AtomicLoad atomicop ->
524- check_memop c atomicop num_size (fun sz -> sz) e.at;
531+ check_memop Atomic c atomicop num_size (fun sz -> sz) e.at;
525532 [NumType I32Type ] --> [NumType atomicop.ty]
526533 | AtomicStore atomicop ->
527- check_memop c atomicop num_size (fun sz -> sz) e.at;
534+ check_memop Atomic c atomicop num_size (fun sz -> sz) e.at;
528535 [NumType I32Type ; NumType atomicop.ty] --> []
529536 | AtomicRmw (rmwop , atomicop ) ->
530- check_memop c atomicop num_size (fun sz -> sz) e.at;
537+ check_memop Atomic c atomicop num_size (fun sz -> sz) e.at;
531538 [NumType I32Type ; NumType atomicop.ty] --> [NumType atomicop.ty]
532539 | AtomicRmwCmpXchg atomicop ->
533- check_memop c atomicop num_size (fun sz -> sz) e.at;
540+ check_memop Atomic c atomicop num_size (fun sz -> sz) e.at;
534541 [NumType I32Type ; NumType atomicop.ty; NumType atomicop.ty] --> [NumType atomicop.ty]
535542
536543and check_seq (c : context ) (s : infer_result_type ) (es : instr list )
0 commit comments