Skip to content

Commit

Permalink
[asl] Introduce asl-carpenter
Browse files Browse the repository at this point in the history
This is a test-generator for ASL, working in two modes:
 - Enumerating all possible ASTs by increasing size
 - Randomly generating ASTs that respect some type-checking constraints

It can also work as a fuzzing tool, and as an execution tool for ASLRef.

Building and installing it is completely optional.
  • Loading branch information
HadrienRenaud committed Mar 13, 2024
1 parent 2f2663d commit 48b5548
Show file tree
Hide file tree
Showing 17 changed files with 2,908 additions and 15 deletions.
4 changes: 3 additions & 1 deletion asllib/Interpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1269,8 +1269,10 @@ module Make (B : Backend.S) (C : Config) = struct
| Some i -> i
in
L_BitVector (Bitvector.zeros length) |> lit
| T_Enum li ->
| T_Enum li -> (
try
IMap.find (List.hd li) env.global.static.constants_values |> lit
with Not_found -> fatal_from t Error.TypeInferenceNeeded)
| T_Int UnConstrained -> L_Int Z.zero |> lit
| T_Int (UnderConstrained _) ->
failwith "Cannot request the base value of a under-constrained integer."
Expand Down
3 changes: 1 addition & 2 deletions asllib/Typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1782,8 +1782,7 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
let env', ldi' = annotate_local_decl_item_uninit s env ldi in
(S_Decl (LDK_Var, ldi', None) |> here, env') |: TypingRule.SDeclNone
| (LDK_Constant | LDK_Let), None ->
(* by construction in Parser. *)
assert false)
fatal_from s UnrespectedParserInvariant)
(* End *)
(* Begin SThrowSome *)
| S_Throw (Some (e, _)) ->
Expand Down
Loading

0 comments on commit 48b5548

Please sign in to comment.