Attachment 341980 Details for Bug 186310 – Patch for landing

[patch] Patch for landing

bug-186310-20180605203029.patch (text/plain), 13.01 KB, created by Robin Morisset on 2018-06-05 11:30:30 PDT

(hide)

Description:

Filename:

MIME Type:

Creator: Robin Morisset

Created: 2018-06-05 11:30:30 PDT

Size: 13.01 KB

patch

obsolete

>Subversion Revision: 232515
>diff --git a/Tools/ChangeLog b/Tools/ChangeLog
>index 2d0492fb0a5484ddfc4f79462544def858ffea7d..fecc9b07e0d3a3b066732ff9984f95c673d21f7e 100644
>--- a/Tools/ChangeLog
>+++ b/Tools/ChangeLog
>@@ -16,6 +16,21 @@
> 
> 2018-06-05  Robin Morisset  <rmorisset@apple.com>
> 
>+        [WSL] Start writing formal execution rules for the spec
>+        https://bugs.webkit.org/show_bug.cgi?id=186310
>+
>+        Rubberstamped by Filip Pizlo
>+
>+        So far it is only the raw rules for control-flow and little else.
>+        They can be compiled to latex with ott (http://www.cl.cam.ac.uk/~pes20/ott/).
>+        The latex can then be turned into a pdf with all the rules.
>+
>+        The longer term plan is to insert the rules one by one into the spec in the right place (ott makes one macro per rule).
>+
>+        * WebGPUShadingLanguageRI/SpecWork/WSL.ott: Added.
>+
>+2018-06-05  Robin Morisset  <rmorisset@apple.com>
>+
>         Add a grammar (in antlr4 format) to the WSL spec.
>         https://bugs.webkit.org/show_bug.cgi?id=186310
> 
>diff --git a/Tools/WebGPUShadingLanguageRI/SpecWork/WSL.ott b/Tools/WebGPUShadingLanguageRI/SpecWork/WSL.ott
>new file mode 100644
>index 0000000000000000000000000000000000000000..7e4e30036e4bf3a0cd0d6e8a2b0ae50d65ad0ebd
>--- /dev/null
>+++ b/Tools/WebGPUShadingLanguageRI/SpecWork/WSL.ott
>@@ -0,0 +1,311 @@
>+metavar x ::= {{ com variable name }}
>+indexvar index, i, j, k, n, m ::=
>+
>+grammar
>+s :: 'stmt_' ::= {{com statement}}
>+    | if ( e ) s :: :: if_then
>+    | if ( e ) s else s' :: :: if_then_expr
>+    | while ( e ) s :: :: while
>+    | do s while ( e ) ; :: :: do_while
>+    | for ( epre ; econd ; eincr ) s :: :: for_expr
>+    | for ( vdecls ; econd ; eincr ) s :: :: for_vdecls
>+    | switch ( e ) { se0 .. sen } :: :: switch
>+    | break ; :: :: break
>+    | continue ; :: :: continue
>+    | fallthrough ; :: :: fallthrough
>+    | return e ; :: :: return
>+    | { s0 .. sn } :: :: block
>+    | { G s0 .. sn } :: :: block_annotated {{com Special, annotated block}}
>+    | Loop ( s1 , s2 ) :: :: loop {{com Special, loop construct}}
>+    | Cases ( block0 , .. , blockn ) :: :: cases {{com Special, switch-cases construct}}
>+    | vdecls ; :: :: variables_declaration {{com variables declaration}}
>+    | e ; :: :: effectful_expr {{com effectful expr}}
>+    | ; :: :: nil {{tex \emptyset ; }} {{com empty statement}}
>+
>+se :: 'switch_elem_' ::= {{com switch element}}
>+    | case rval : block :: :: case
>+    | default : block :: :: default
>+
>+block :: 'block_' ::= {{com Special block with no effect on scoping, used for switches}}
>+    | s0 .. sn :: :: stmt_list
>+
>+e, epre {{tex e_{pre} }}, econd {{tex e_{cond} }}, eincr {{tex e_{incr} }} :: 'expr_' ::= {{com expression}}
>+    | True :: :: true
>+    | False :: :: false
>+    | e || e' :: :: or
>+    | e && e' :: :: and
>+    | e ? e1 : e2 :: :: ternary
>+    | Comma ( e0 , .. , en ) :: :: comma {{com Comma is just a way to disambiguate this in the rules}}
>+    | e = e' :: :: assignment
>+    | x :: :: identifier
>+    | Void :: :: void {{com Special, void value}}
>+    | sid :: :: sid {{com Special, store identifier}}
>+
>+v :: 'val_' ::= {{com value}}
>+    | True :: :: true
>+    | False :: :: false
>+    | Void :: :: void {{com Special, void value}}
>+    | sid :: :: sid {{com store identifier}}
>+
>+rval :: 'rval_' ::= {{com right-side value}}
>+    | True :: :: true
>+    | False :: :: false
>+    | Void :: :: void {{com Special, void value}}
>+
>+lval :: 'lval_' ::= {{com left-side value}}
>+    | sid :: :: sid {{com store identifier}}
>+
>+vdecls :: 'vdecls_' ::= {{com variables declaration}}
>+    | t vdecl1 , .. , vdecln :: :: vdecls
>+
>+t {{tex \tau}} :: 'type' ::= {{com type}}
>+    | bool :: :: bool
>+
>+vdecl :: vdecl' ::=
>+    | x : sid :: :: uninitialized
>+    | x : sid = e :: :: initialized
>+
>+sid :: 'sid' ::= {{com store identifier}}
>+
>+G {{tex \Gamma}}, Gout {{tex \Gamma_{out} }} :: 'gamma_' ::= {{com environment}}
>+    | Empty :: :: empty {{ tex \emptyset }} 
>+    | G [ x -> sid ] :: :: update {{tex [[G]][ [[x]] \mapsto [[sid]] ] }}
>+
>+S {{tex \Sigma}} :: 'sigma_' ::= {{com store}}
>+    | Empty :: :: empty {{ tex \emptyset }}
>+    | S [ sid -> rval ] :: :: update {{tex [[S]][ [[sid]] \mapsto [[rval]] ] }}
>+
>+formula :: formula_ ::=  
>+    | judgement :: :: judgement
>+    | rval = Default ( t ) :: :: default_value
>+    | rval = rval' :: :: rval_equality
>+    | isNotLVal ( e ) :: :: is_not_lval
>+    | sid -> rval in S :: :: mapping_in_store {{tex ([[sid]] \mapsto [[rval]]) \in [[S]] }}
>+    | x -> sid in G :: :: mapping_in_env {{tex ([[x]] \mapsto [[sid]]) \in [[G]] }}
>+    | n > 0 :: :: index_positive
>+    | rval not found in se0 .. sen :: :: not_found_in_switch
>+    | se0 = _ : block0 .. sen = _ : blockn :: :: destruct_switch_elems
>+
>+subrules
>+    rval <:: v
>+    lval <:: v
>+    v <:: e
>+
>+defns
>+reduction :: '' ::=
>+defn
>+s1 => s2 :: :: reduce_basic_stmt :: '' {{ tex [[s1]] \Rightarrow [[s2]]}} by
>+
>+    ------------------------------- :: if_then_desugar
>+    if ( e ) s => if ( e ) s else ;
>+
>+    -------------------------- :: if_true
>+    if ( True ) s else s' => s
>+
>+    ---------------------------- :: if_false
>+    if ( False ) s else s' => s'
>+
>+    ------------------------------ :: block_next_stmt
>+    {G ; s0 .. sn} => {G s0 .. sn}
>+
>+    ----------------------------------- :: block_break
>+    {G break; s0 .. sn} => break;
>+
>+    ----------------------------------------- :: block_fallthrough
>+    {G fallthrough; s0 .. sn} => fallthrough;
>+
>+    ----------------------------------- :: block_continue
>+    {G continue; s0 .. sn} => continue;
>+
>+    ----------------------------------- :: block_return
>+    {G return e; s0 .. sn} => return e;
>+
>+    --------- :: block_empty
>+    {G } => ;
>+
>+    ---------- :: effectful_expr_value
>+    rval; => ;
>+
>+    --------------------- :: loop_break
>+    Loop(break ;, s) => ;
>+
>+    ------------------------ :: loop_continue
>+    Loop(continue ;, s) => s
>+
>+    ------------------------------------- :: loop_fallthrough
>+    Loop(fallthrough;, s) => fallthrough;
>+
>+    ------------------------------- :: loop_return
>+    Loop(return e;, s) => return e;
>+
>+    --------------- :: loop_iteration_finished
>+    Loop(;, s) => s
>+
>+    ----------------------------------------------- :: cases_break
>+    Cases(break; s0 .. sn, block0, .., blockm) => ;
>+
>+    ------------------------------------------------------------ :: cases_continue
>+    Cases(continue; s0 .. sn, block0, .., blockm) => continue;
>+
>+    ----------------------------------------------------------------------------- :: cases_fallthrough
>+    Cases(fallthrough; s0 .. sn, block0, .., blockm) => Cases(block0, .., blockm)
>+
>+    ---------------------------------------------------------- :: cases_return
>+    Cases(return e; s0 .. sn, block0, .., blockm) => return e;
>+
>+    ----------------------------------------------------------------------------- :: cases_next_stmt
>+    Cases( ; s0 .. sn, block0, .., blockm) => Cases(s0 .. sn, block0, .., blockm)
>+
>+    ------------ :: cases_empty
>+    Cases() => ;
>+
>+    ------------------------------------------ :: while_loop
>+    while (e) s => if (e) Loop(s, while (e) s)
>+    % Note: this relies on the absence of variable declarations outside of blocks
>+    % if this is not guaranteed by the validation phase, replace the production by if(e) Loop({s}, while (e) s)
>+
>+    ------------------------------------- :: do_while_loop
>+    do s while(e); => Loop(s, while(e) s)
>+    % Note: this relies on the absence of variable declarations outside of blocks
>+    % if this is not guaranteed by the validation phase, replace the production by Loop({s}, while (e) s)
>+
>+    --------------------------------------------------------------- :: for_expr_loop
>+    for (epre; econd; eincr) s => { epre; while(econd) {s eincr;} }
>+    % Note: this relies on the absence of variable declarations outside of blocks
>+    % if this is not guaranteed by the validation phase, replace {s eincr} by {{s} eincr}
>+
>+    --------------------------------------------------------------- :: for_decls_loop
>+    for (vdecls; econd; eincr) s => { vdecls; while(econd) {s eincr;} }
>+    % Note: this relies on the absence of variable declarations outside of blocks
>+    % if this is not guaranteed by the validation phase, replace {s eincr} by {{s} eincr}
>+
>+    rval = rval'
>+    se'0 = _ : block'0 .. se'm = _ : block'm
>+    -------------------------------------------------------------------------------------------------- :: switch_case_found
>+    switch (rval) {se0 .. sen case rval' : block se'0 .. se'm} => {Cases(block, block'0, .., block'm)}
>+
>+    rval not found in se0 .. sen
>+    rval not found in se'0 .. se'm
>+    se'0 = _ : block'0 .. se'm = _ : block'm
>+    -------------------------------------------------------------------------------------------------- :: switch_case_not_found
>+    switch (rval) {se0 .. sen default : block se'0 .. se'm} => {Cases(block, block'0, .., block'm)}
>+
>+    n > 0
>+    ------------------------------------------------------------------------------------------ :: vdecls_multi
>+    {G t vdecl0, vdecl1, .., vdecln; s0 .. sm} => {G t vdecl0; t vdecl1, .., vdecln; s0 .. sm}
>+
>+    ------------------------------------------------------------- :: vdecl_initializer
>+    {G t x : sid = e; s0 .. sn} => {G t x : sid; x = e; s0 .. sn}
>+
>+defn
>+s1 , G1 , S1 => s2 , G2 , S2 :: :: reduce_stmt :: '' {{ tex [[s1]], [[G1]], [[S1]] \Rightarrow [[s2]], [[G2]], [[S2]] }} by
>+   
>+    s => s'
>+    -------------------- :: reduce_stmt_basic
>+    s, G, S => s', G, S
>+
>+    ---------------------------------------------- :: annotate_block
>+    {s0 .. sn}, G, S => {G s0 .. sn}, G, S
>+
>+    G |- e, S -> e', S'
>+    ---------------------- :: effectful_expr_reduce
>+    e;, G, S => e';, G, S'
>+
>+    G |- e, S -> e', S'
>+    -------------------------------------------------- :: if_reduce
>+    if (e) s else s', G, S => if (e') s else s', G, S'
>+
>+    G |- e, S -> e', S'
>+    ------------------------------------------------------------------------------------------------ :: switch_reduce
>+    switch (e) {se0 .. sen}, G, S => switch (e') {se0 .. sen}, G, S'
>+
>+    s, G, S => s', G', S'
>+    -------------------------------------------------------- :: block_reduce
>+    {G s s0 .. sn}, Gout, S => {G' s' s0 .. sn}, Gout, S'
>+
>+    s, G, S => s', G', S'
>+    ---------------------------------------- :: loop_reduce
>+    Loop(s, s2), G, S => Loop(s', s2), G', S'
>+    % Note: if G and G' are not equal, something very wrong is going on.
>+    % s should always be either a block (so no change to the environment), or a statement that is not a variable declaration (same)
>+
>+    s0, G, S => s0', G', S'
>+    ----------------------------------------------------------------------------------------------- :: cases_reduce_first_stmt
>+    Cases(s0 s1 .. sn, block0, .., blockm), G, S => Cases(s0' s1 .. sn, block0, .., blockm), G', S'
>+
>+    G |- e, S -> e', S'
>+    ---------------------------------- :: return_reduce
>+    return e;, G, S => return e';, G, S'
>+
>+    rval = Default(t)
>+    ----------------------------------------------- :: vdecl_uninitialized
>+    t x : sid;, G, S => ;, G[x -> sid], S[sid -> rval]
>+
>+defn
>+e1 -> e2 :: :: reduce_basic_expr :: '' {{ tex [[e1]] \rightarrow [[e2]] }} by
>+    
>+    -------------- :: boolean_and_true
>+    True && e -> e
>+
>+    ------------------- :: boolean_and_false
>+    False && e -> False
>+
>+    --------------- :: boolean_or_false
>+    False || e -> e
>+
>+    ----------------- :: boolean_or_true
>+    True || e -> True
>+
>+    -------------------- :: ternary_true
>+    True ? e1 : e2 -> e1
>+
>+    -------------------- :: ternary_false
>+    False ? e1 : e2 -> e2
>+
>+    ------------------ :: comma_last_expr
>+    Comma (e) -> e
>+
>+    -------------------------------------------------- :: comma_first_rval
>+    Comma(rval, e, e0, .., en) -> Comma(e, e0, .., en)
>+
>+defn
>+G |- e1 , S1 -> e2 , S2 :: :: reduce_expr :: '' {{ tex [[G]] \vdash [[e1]], [[S1]] \rightarrow [[e2]], [[S2]] }} by
>+    e1 -> e2
>+    ----------------------- :: reduce_expr_basic
>+    G |- e1, S -> e2, S
>+
>+    G |- e1, S -> e1', S'
>+    ------------------------------------- :: boolean_and_reduce
>+    G |- e1 && e2, S -> e1' && e2, S'
>+    
>+    G |- e1, S -> e1', S'
>+    ------------------------------------- :: boolean_or_reduce
>+    G |- e1 || e2, S -> e1' || e2, S'
>+
>+    G |- e, S -> e', S'
>+    --------------------------------------- :: ternary_reduce
>+    G |- e ? e1 : e2, S -> e' ? e1 : e2, S'
>+
>+    G |- e, S -> e', S'
>+    ----------------------------------------------------------------- :: comma_reduce
>+    G |- Comma(e, e0, e1, .., en), S -> Comma(e', e0, e1, .., en), S'
>+
>+    isNotLVal(e1)
>+    G |- e1, S -> e1', S' 
>+    ------------------------------------ :: assign_reduce_left
>+    G |- e1 = e2, S -> e1' = e2, S'
>+
>+    G |- e2, S -> e2', S'
>+    ---------------------------------- :: assign_reduce_right
>+    G |- lval = e2, S -> lval = e2', S
>+
>+    ------------------------------------------ :: assign_execute
>+    G |- sid = rval, S -> Void, S[sid -> rval]
>+
>+    x -> sid in G
>+    ------------------- :: environment_access
>+    G |- x, S -> sid, S
>+
>+    sid -> rval in S
>+    ---------------------- :: store_access
>+    G |- sid, S -> rval, S

Flags:

commit-queue: commit-queue-

Actions: View | Formatted Diff | Diff

Attachments on bug 186310: 341975 | 341980 | 341983