-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #19 from ethanuppal/immutable-context
Improve Context Implementation and Testing
- Loading branch information
Showing
10 changed files
with
147 additions
and
45 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,34 +1,25 @@ | ||
(* TODO: can we have immutability here? kind of seems like a good place | ||
actually. *) | ||
open Util | ||
module Scope = Hashtbl.Make (String) | ||
|
||
type 'a t = 'a Scope.t BatDynArray.t | ||
|
||
let make () = BatDynArray.make 16 | ||
let stack_size = BatDynArray.length | ||
let is_empty = BatDynArray.empty | ||
let push ctx = BatDynArray.add ctx (Scope.create 16) | ||
let pop = BatDynArray.delete_last | ||
|
||
(** [top ctx] is the scope at the top of the stack. | ||
Requires: [not (is_empty ctx)]. *) | ||
let top = BatDynArray.last | ||
type 'a t = 'a Scope.t list ref | ||
|
||
let make () = ref [] | ||
let stack_size ctx = List.length !ctx | ||
let is_empty ctx = List.is_empty !ctx | ||
let push ctx = ctx := Scope.create 16 :: !ctx | ||
let pop ctx = ctx := List.tl !ctx | ||
let top ctx = List.hd !ctx | ||
let insert ctx = Scope.replace (top ctx) | ||
|
||
let get ctx key = | ||
let rec get_aux i = | ||
if i = -1 then None | ||
else | ||
let scope = BatDynArray.get ctx i in | ||
match Scope.find_opt scope key with | ||
| None -> get_aux (i - 1) | ||
| Some value -> Some value | ||
let rec get_aux lst = | ||
match lst with | ||
| [] -> None | ||
| scope :: rest -> ( | ||
match Scope.find_opt scope key with | ||
| None -> get_aux rest | ||
| Some value -> Some value) | ||
in | ||
get_aux (stack_size ctx - 1) | ||
get_aux !ctx | ||
|
||
(* sadly [Util.(>>)] doesn't work with the type system here *) | ||
let to_seq ctx = | ||
ctx |> BatDynArray.to_list |> List.map Scope.to_seq |> List.to_seq | ||
|> Seq.concat | ||
let to_list ctx = !ctx |> List.map (Scope.to_seq >> List.of_seq) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,118 @@ | ||
open X86ISTMB | ||
|
||
let uniq_ctx_list lst = | ||
let cmp_fst a b = String.compare (fst a) (fst b) in | ||
List.map (BatList.unique_cmp ~cmp:cmp_fst) lst | ||
|
||
let sort_ctx_list lst = lst |> List.map (BatList.sort compare) | ||
|
||
(** [ctx_of_ctx_lst lst] creates a [Context.t] from a list of scopes and | ||
variable bindings. Scopes that appear earlier in [lst] are guaranteed to be | ||
pushed before scopes that appear later in [lst]. Key-value pairs that come | ||
later in each scope will overwrite those that come earlier. *) | ||
let ctx_of_ctx_lst lst = | ||
let ctx = Context.make () in | ||
List.iter | ||
(fun scope -> | ||
Context.push ctx; | ||
List.iter (fun (name, value) -> Context.insert ctx name value) scope) | ||
lst; | ||
ctx | ||
|
||
let gen_ctx_lst = | ||
QCheck2.Gen.(small_list (small_list (pair string int)) >|= uniq_ctx_list) | ||
|
||
let gen_ctx = QCheck2.Gen.(gen_ctx_lst >|= ctx_of_ctx_lst) | ||
let print_ctx_lst = QCheck2.Print.(list (list (pair string int))) | ||
|
||
let make_is_empty = | ||
let test () = | ||
let open Alcotest in | ||
let ctx = Context.make () in | ||
(check bool) "new context is empty" true (Context.is_empty ctx); | ||
(check int) "new context has zero stack size" 0 (Context.stack_size ctx); | ||
(check (list (list (pair string int)))) | ||
"new context has no pairs" [] (Context.to_list ctx) | ||
in | ||
Alcotest.test_case "empty context properties" `Quick test | ||
|
||
let empty_get_none = | ||
let open QCheck2 in | ||
let test = | ||
Test.make ~name:"get on empty always none" ~count:10 Gen.string (fun s -> | ||
let empty = Context.make () in | ||
Context.get empty s = None) | ||
in | ||
QCheck_alcotest.to_alcotest test | ||
|
||
let to_list_correct = | ||
let open QCheck2 in | ||
let test = | ||
Test.make ~name:"to_list correct vars" ~count:100 ~print:print_ctx_lst | ||
gen_ctx_lst (fun lst -> | ||
let ctx = ctx_of_ctx_lst lst in | ||
let result = Context.to_list ctx in | ||
let expected = lst |> List.rev in | ||
sort_ctx_list result = sort_ctx_list expected) | ||
in | ||
QCheck_alcotest.to_alcotest test | ||
|
||
let push_pop_id = | ||
let open QCheck2 in | ||
let test = | ||
Test.make ~name:"push then pop" ~count:100 gen_ctx (fun ctx -> | ||
let initial = Context.to_list ctx in | ||
Context.push ctx; | ||
Context.insert ctx "a" 1; | ||
Context.pop ctx; | ||
let final = Context.to_list ctx in | ||
sort_ctx_list initial = sort_ctx_list final) | ||
in | ||
QCheck_alcotest.to_alcotest ~long:true test | ||
|
||
let push_stack_size = | ||
let open QCheck2 in | ||
let test = | ||
Test.make ~name:"push stack size" ~count:100 gen_ctx (fun ctx -> | ||
let initial = Context.stack_size ctx in | ||
Context.push ctx; | ||
let final = Context.stack_size ctx in | ||
final = initial + 1) | ||
in | ||
QCheck_alcotest.to_alcotest ~long:true test | ||
|
||
let pop_stack_size = | ||
let open QCheck2 in | ||
let test = | ||
Test.make ~name:"pop stack size" ~count:100 gen_ctx (fun ctx -> | ||
assume (not (Context.is_empty ctx)); | ||
let initial = Context.stack_size ctx in | ||
Context.pop ctx; | ||
let final = Context.stack_size ctx in | ||
final = initial - 1) | ||
in | ||
QCheck_alcotest.to_alcotest ~long:true test | ||
|
||
let insert_get = | ||
let open QCheck2 in | ||
let test = | ||
Test.make ~name:"insert then get" ~count:100 | ||
QCheck2.Gen.(triple gen_ctx string int) | ||
(fun (ctx, str, i) -> | ||
assume (not (Context.is_empty ctx)); | ||
Context.insert ctx str i; | ||
Context.get ctx str = Some i) | ||
in | ||
QCheck_alcotest.to_alcotest ~long:true test | ||
|
||
let suite = | ||
( "lib/frontend/context.ml", | ||
[ | ||
make_is_empty; | ||
empty_get_none; | ||
to_list_correct; | ||
push_pop_id; | ||
push_stack_size; | ||
pop_stack_size; | ||
insert_get; | ||
] ) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters