Skip to content

Commit 06ad225

Browse files
ivgivg
authored
Merge pull request #2 from ccasin/smallstep
Modify small-step reduction to eliminate "stuck" expressions
2 parents 90f7a07 + ca48e1a commit 06ad225

File tree

2 files changed

+120
-92
lines changed

2 files changed

+120
-92
lines changed

‎bil.ott

Lines changed: 97 additions & 87 deletions
Original file line numberDiff line numberDiff line change
@@ -57,6 +57,8 @@ grammar
5757
{{ com -- extract or extend bitvector $e$}}
5858
| e1 @ e2 :: :: concat
5959
{{ com -- concatenate two bitvector $e_1$ to $e_2$ }}
60+
| [ e1 / var ] e2 :: M :: subst
61+
{{ com -- the (capture avoiding) substitution of $e_1$ for $var$ in $e_2$ }}
6062

6163
var :: var_ ::=
6264
| id : type :: S :: var
@@ -201,6 +203,11 @@ formula :: formula_ ::=
201203
| nat1 > nat2 :: M :: nat_gt {{ coq ([[nat1]] > [[nat2]])}}
202204
| nat1 = nat2 :: M :: nat_eq {{ coq ([[nat1]] = [[nat2]])}}
203205
| nat1 >= nat2 :: M :: nat_ge {{ coq ([[nat1]] >= [[nat2]])}}
206+
| e1 :=def e2 :: M :: defines
207+
{{ tex [[e1]] \stackrel{\text{def} }{:=} [[e2]] }}
208+
| ( var , val ) in delta :: M :: in_env
209+
| var notin dom ( delta ) :: M :: notin_env
210+
{{ tex [[var]] [[notin]] \mathsf{dom}([[delta]]) }}
204211

205212
terminals :: terminals_ ::=
206213
| -> :: :: rarrow {{ tex \rightarrow }}
@@ -210,10 +217,13 @@ terminals :: terminals_ ::=
210217
| |-> :: :: mapsto {{ tex \mapsto }}
211218
| lambda :: :: lambda {{ tex \lambda }}
212219
| ~> :: :: leadsto {{ tex \leadsto }}
220+
| ~>* :: :: mleadsto {{ tex \leadsto^{*} }}
213221
| <> :: :: neq {{ tex \neq }}
214222
| >> :: :: lsr {{ tex \gg}}
215223
| ~>> :: :: asr {{ tex \ggg}}
216224
| << :: :: lsl {{ tex \ll}}
225+
| in :: :: in {{ tex \in }}
226+
| notin :: :: notin {{ tex \notin }}
217227

218228

219229
subrules
@@ -386,44 +396,35 @@ defns reduce_exp :: '' ::=
386396

387397
defn delta |- exp ~> exp' :: :: exp :: '' by
388398

389-
390-
-------------------------------------------- :: var_reduce
391-
delta[var <- v] |- var ~> v
392-
393-
399+
(var,v) in delta
400+
------------------ :: var_in
394401
delta |- var ~> v
395-
var <> var'
396-
-------------------------------------------- :: var_extend
397-
delta[var' <- v'] |- var ~> v
398-
399402

400403

404+
id:type notin dom(delta)
401405
-------------------------------------------- :: var_unknown
402-
[] |- id:type ~> unknown [str] : type
406+
delta |- id:type ~> unknown[str]:type
403407

404408
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
405409
% LOAD %
406410
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
407411

412+
delta |- e2 ~> e2'
413+
------------------------------------- :: load_step_addr
414+
delta |- e1[e2,ed]:sz ~> e1[e2',ed]:sz
408415

409-
delta |- e2 ~> v2
410-
------------------------------------- :: load_addr
411-
delta |- e1[e2,ed]:sz ~> e1[v2,ed]:sz
412416

417+
delta |- e1 ~> e1'
418+
------------------------------------- :: load_step_mem
419+
delta |- e1[v2,ed]:sz ~> e1'[v2,ed]:sz
413420

414-
delta |- e1 ~> v1
415-
------------------------------------- :: load_mem
416-
delta |- e1[v2,ed]:sz ~> v1[v2,ed]:sz
417421

418-
419-
----------------------------------------------------------- :: load_byte
422+
------------------------------------------------------ :: load_byte
420423
delta |- (v1 with [w,ed]:8 <- num:8)[w,ed']:8 ~> num:8
421424

422425
------------------------------------------------------------------------------ :: load_un_addr
423426
delta |- (v1 with [unknown[str]:t,ed]:8 <- v2)[v3,ed]:8 ~> unknown[str]:imm<8>
424427

425-
426-
427428
w1 <> w2
428429
---------------------------------------------------------- :: load_rec
429430
delta |- (v1 with [w1,ed]:8 <- v3)[w2,ed]:8 ~> v1[w2,ed]:8
@@ -446,94 +447,90 @@ defns reduce_exp :: '' ::=
446447
%% STORE %
447448
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
448449

450+
449451

450-
451-
delta |- e ~> v
452-
------------------------------------------------------------------------- :: store_val
453-
delta |- e1 with [e2,ed]:sz <- e ~> e1 with [e2,ed] : sz <- v
452+
delta |- e3 ~> e3'
453+
------------------------------------------------------------------------- :: store_step_val
454+
delta |- e1 with [e2,ed]:sz <- e3 ~> e1 with [e2,ed] : sz <- e3'
454455

455456

456-
delta |- e ~> v
457-
------------------------------------------------------------------------- :: store_addr
458-
delta |- e1 with [e,ed]:sz <- val ~> e1 with [v,ed] : sz <- val
457+
delta |- e2 ~> e2'
458+
------------------------------------------------------------------------- :: store_step_addr
459+
delta |- e1 with [e2,ed]:sz <- v3 ~> e1 with [e2',ed] : sz <- v3
459460

460461

461-
delta |- e ~> v
462-
------------------------------------------------------------------------- :: store_mem
463-
delta |- e with [v1,ed]:sz <- val ~> v with [v1,ed] : sz <- val
462+
delta |- e1 ~> e1'
463+
------------------------------------------------------------------------- :: store_step_mem
464+
delta |- e1 with [v2,ed]:sz <- v3 ~> e1' with [v2,ed] : sz <- v3
464465

465466
succ w = w'
466-
delta |- high:8[w] ~> w1
467-
delta |- low:(sz-8)[w] ~> w2
468-
delta |- v with [w,be]:8 <- w1 ~> v'
467+
e1 :=def (v with [w,be]:8 <- high:8[val])
469468
-------------------------------------------------------------------- :: store_word_be
470-
delta |- v with [w,be]:sz <- val ~> v' with [w', be]:(sz-8) <- w2
469+
delta |- v with [w,be]:sz <- val ~> e1 with [w',be]:(sz-8) <- low:(sz-8)[val]
471470

472471
succ w = w'
473-
delta |- low:8[w] ~> w1
474-
delta |- high:(sz-8)[w] ~> w2
475-
delta |- v with [w,be]:8 <- w1 ~> v'
472+
e1 :=def (v with [w,el]:8 <- low:8[val])
476473
-------------------------------------------------------------------- :: store_word_el
477-
delta |- v with [w,el]:sz <- val ~> v' with [w', el]:(sz-8) <- w2
474+
delta |- v with [w,el]:sz <- val ~> e1 with [w',el]:(sz-8) <- high:(sz-8)[val]
478475

479476

477+
delta |- e1 ~> e1'
478+
------------------------------------------------ :: let_step
479+
delta |- let var = e1 in e2 ~> let var = e1' in e2
480480

481481

482-
delta |- e1 ~> v
483-
------------------------------------------------ :: let_head
484-
delta |- let var = e1 in e2 ~> let var = v in e2
482+
------------------------------------------------- :: let
483+
delta |- let var = v in e ~> [v/var]e
485484

486485

487-
delta[var <- v] |- e ~> val
488-
-------------------------------- :: let_body
489-
delta |- let var = v in e ~> val
486+
delta |- e1 ~> e1'
487+
------------------------------------------------------------------ :: ite_step
488+
delta |- if e1 then e2 else e3 ~> if e1' then e2 else e3
490489

490+
----------------------------------------------- :: ite_true
491+
delta |- if true then e2 else e3 ~> e2
491492

492-
delta |- e1 ~> true
493-
------------------------------------ :: ite_true
494-
delta |- if e1 then e2 else e3 ~> e2
493+
494+
------------------------------------------------ :: ite_false
495+
delta |- if false then e2 else e3 ~> e3
495496

496-
delta |- e1 ~> false
497-
------------------------------------ :: ite_false
498-
delta |- if e1 then e2 else e3 ~> e3
499497

498+
delta |- e2 ~> e2'
499+
------------------------------------------ :: bop_rhs
500+
delta |- e1 bop e2 ~> e1 bop e2'
500501

501-
delta |- e2 ~> v
502-
------------------------------------- :: bop_rhs
503-
delta |- e1 bop e2 ~> e1 bop v
502+
delta |- e1 ~> e1'
503+
----------------------------------------- :: bop_lhs
504+
delta |- e1 bop v2 ~> e1' bop v2
504505

505-
delta |- e1 ~> v
506-
------------------------------------- :: bop_lhs
507-
delta |- e1 bop v' ~> v bop v'
508506

509-
510-
----------------------------------------------- :: bop_unk_rhs
507+
-------------------------------------------------------- :: bop_unk_rhs
511508
delta |- e bop unknown[str]:t ~> unknown[str]:t
512509

513-
----------------------------------------------- :: bop_unk_lhs
510+
-------------------------------------------------------- :: bop_unk_lhs
514511
delta |- unknown[str]:t bop e ~> unknown[str]:t
515512

516513

517-
---------------------------------------- :: plus
514+
-------------------------------------- :: plus
518515
delta |- w1 + w2 ~> w1 .+ w2
519516

520-
---------------------------------------- :: minus
517+
-------------------------------------- :: minus
521518
delta |- w1 - w2 ~> w1 .- w2
522519

523520

524-
---------------------------------------- :: times
521+
------------------------------------- :: times
525522
delta |- w1 * w2 ~> w1 .* w2
526523

527524

528-
---------------------------------------- :: div
525+
------------------------------------- :: div
529526
delta |- w1 / w2 ~> w1 ./ w2
530527

531528

532-
----------------------------------------------- :: sdiv
529+
--------------------------------------- :: sdiv
533530
delta |- w1 /$ w2 ~> w1 ./$ w2
534531

535532

536-
---------------------------------------- :: mod
533+
------------------------------------- :: mod
537534
delta |- w1 % w2 ~> w1 .% w2
538535

539536

@@ -573,22 +570,22 @@ defns reduce_exp :: '' ::=
573570
delta |- w1 < w2 ~> w1 .< w2
574571

575572

576-
delta |- w1 <> w2 ~> w
573+
577574
----------------------------------------------- :: less_eq
578-
delta |- w1 <= w2 ~> w & (w1 < w2)
575+
delta |- w1 <= w2 ~> (w1 < w2) | (w1 = w2)
579576

580577

581578

582579
----------------------------------------------- :: signed_less
583580
delta |- w1 <$ w2 ~> w1 .<$ w2
584581

585-
delta |- w1 <> w2 ~> w
586-
----------------------------------------------- :: signed_less_eq
587-
delta |- w1 <=$ w2 ~> w & (w1 <$ w2)
588582

589-
delta |- e ~> v
583+
----------------------------------------------------- :: signed_less_eq
584+
delta |- w1 <=$ w2 ~> (w1 = w2) & (w1 <$ w2)
585+
586+
delta |- e ~> e'
590587
---------------------------------------- :: uop
591-
delta |- uop e ~> uop v
588+
delta |- uop e ~> uop e'
592589

593590
---------------------------------------- :: not_true
594591
delta |- ~true ~> false
@@ -598,14 +595,14 @@ defns reduce_exp :: '' ::=
598595
delta |- ~false ~> true
599596

600597

601-
delta |- e2 ~> v2
598+
delta |- e2 ~> e2'
602599
---------------------------------------- :: concat_rhs
603-
delta |- e1 @ e2 ~> e1 @ v2
600+
delta |- e1 @ e2 ~> e1 @ e2'
604601

605602

606-
delta |- e1 ~> v1
603+
delta |- e1 ~> e1'
607604
---------------------------------------- :: concat_lhs
608-
delta |- e1 @ v2 ~> v1 @ v2
605+
delta |- e1 @ v2 ~> e1' @ v2
609606

610607
---------------------------------------------- :: concat_lhs_un
611608
delta |- unknown[str]:t @ v2 ~> unknown[str]:t
@@ -616,9 +613,9 @@ defns reduce_exp :: '' ::=
616613
---------------------------------------- :: concat
617614
delta |- w1 @ w2 ~> w1 .@ w2
618615

619-
delta |- e ~> v
616+
delta |- e ~> e'
620617
------------------------------------------------- :: extract_reduce
621-
delta |- extract:sz1:sz2[e] ~> extract:sz1:sz2[v]
618+
delta |- extract:sz1:sz2[e] ~> extract:sz1:sz2[e']
622619

623620

624621
---------------------------------------------------------- :: extract_un
@@ -627,9 +624,9 @@ defns reduce_exp :: '' ::=
627624
------------------------------------------------------ :: extract
628625
delta |- extract:sz1:sz2[w] ~> ext w ~hi:sz1 ~lo:sz2
629626

630-
delta |- e ~> v
627+
delta |- e ~> e'
631628
--------------------------------- :: cast_reduce
632-
delta |- cast:sz[e] ~> cast:sz[v]
629+
delta |- cast:sz[e] ~> cast:sz[e']
633630

634631

635632
-------------------------------------------- :: cast_low
@@ -652,11 +649,12 @@ defns reduce_stmt :: '' ::=
652649
defn delta , word |- stmt ~> delta' , word' :: :: stmt :: '' by
653650

654651

655-
delta |- e ~> v
652+
delta |- e ~>* v
656653
----------------------------------------- :: move
657654
delta,w |- var := e ~> delta[var <- v], w
658655

659-
delta |- e ~> w'
656+
657+
delta |- e ~>* w'
660658
---------------------------------- :: jmp
661659
delta,w |- jmp e ~> delta, w'
662660

@@ -669,29 +667,29 @@ defns reduce_stmt :: '' ::=
669667
delta,w |- special(str) ~> delta,w
670668

671669

672-
delta |- e ~> true
670+
delta |- e ~>* true
673671
delta,word |- seq ~> delta',word',{}
674672
------------------------------------- :: ifthen_true
675673
delta,word |- if (e) seq ~> delta', word'
676674

677-
delta |- e ~> true
675+
delta |- e ~>* true
678676
delta,word |- seq ~> delta',word',{}
679677
------------------------------------- :: if_true
680678
delta,word |- if (e) seq else seq1 ~> delta', word'
681679

682-
delta |- e ~> false
680+
delta |- e ~>* false
683681
delta,word |- seq ~> delta',word',{}
684682
------------------------------------- :: if_false
685683
delta,word |- if (e) seq1 else seq ~> delta', word'
686684

687685

688-
delta1 |- e ~> true
686+
delta1 |- e ~>* true
689687
delta1,word1 |- seq ~> delta2,word2,{}
690688
delta2,word2 |- while (e) seq ~> delta3,word3
691689
--------------------------------------------- :: while
692690
delta1,word1 |- while (e) seq ~> delta3,word3
693691

694-
delta |- e ~> false
692+
delta |- e ~>* false
695693
----------------------------------------- :: while_false
696694
delta,word |- while (e) seq ~> delta,word
697695

@@ -714,3 +712,15 @@ defns reduce_stmt :: '' ::=
714712

715713
------------------------------------------------------------- :: seq_nil
716714
delta,word |- {} ~> delta, word, {}
715+
716+
defns multistep_exp :: '' ::=
717+
718+
defn delta |- exp ~>* exp' :: :: mexp :: '' by
719+
720+
---------------- :: refl
721+
delta |- e ~>* e
722+
723+
delta |- e1 ~> e2
724+
delta |- e2 ~>* e3
725+
------------------ :: reduce
726+
delta |- e1 ~>* e3

0 commit comments

Comments
 (0)