diff --git a/README.md b/README.md index 10f51988..6879cde7 100644 --- a/README.md +++ b/README.md @@ -258,7 +258,7 @@ Before running the simulator, we need to convert the test program `test.S` to an To simulate execution of the test program using ASLi, load `demo.asl` into ASLi, load the ELF file `test.elf` and use `:step` to step through the program and the `PrintState` function (defined in `demo.asl`) to observe the processor state at each step. - $ ASL_PATH=.:.. ../_build/default/bin/asli.exe demo.asl + $ ASL_PATH=.:.. ../_build/install/default/bin/asli demo.asl ASLi> :elf test.elf Loading ELF file test.elf. Entry point = 0x401000 @@ -281,7 +281,7 @@ This is just about the most exciting program we can run using such a limited ins ASLi can also accept commands from a "project file". For example, we could put all of the `:step` and `PrintState();` commands in a file `test.prj` and run the same test like this. - ASL_PATH=.:.. ../_build/default/bin/asli.exe demo.asl --project=test.prj + ASL_PATH=.:.. ../_build/install/default/bin/asli demo.asl --project=test.prj We often use this with the LLVM project [FileCheck](https://llvm.org/docs/CommandGuide/FileCheck.html) tool in our integration tests. @@ -289,17 +289,17 @@ We often use this with the LLVM project [FileCheck](https://llvm.org/docs/Comman For larger architecture specifications, it can be more effective to compile the specification instead. To compile the specification, we first build a project file containing a sequence of ASLi commands to compile the specification to C code. There are multiple options for doing this, the "fallback" backend is the most portable. - ../_build/default/bin/asl2c.py --basename=sim --backend=fallback > sim.prj + ../_build/install/default/bin/asl2c --basename=sim --backend=fallback > sim.prj We then load the demo specification into ASLi and run the project file to generate C code. The configuration file `exports.json` is used to specify which ASL functions are called by hand-written C code. - ASL_PATH=.:.. ../_build/default/bin/asli.exe --project=sim.prj --configuration=exports.json demo.asl + ASL_PATH=.:.. ../_build/install/default/bin/asli --project=sim.prj --configuration=exports.json demo.asl The generated code is in C files that start with the basename `sim` such as `sim_funs.c`. To compile and link the C code, we need to use some compiler and linker flags. We can use the `asl2c.py` script to get the right flags for each backend. - ASL2C=../_build/default/bin/asl2c.py + ASL2C=../_build/install/default/bin/asl2c CFLAGS=`$ASL2C --backend=fallback --print-c-flags` LDFLAGS=`$ASL2C --backend=fallback --print-ld-flags` diff --git a/bin/asl2c.py b/bin/asl2c.py index c66d3af5..fc444963 100755 --- a/bin/asl2c.py +++ b/bin/asl2c.py @@ -252,11 +252,11 @@ def get_c_flags(asli, backend): c_flags = subprocess.check_output([asli, "--print-c-flags"]).decode('utf-8').strip().split() else: # ASLi has not been installed so let's assume that it is being run - # directly out of the build tree and the path looks like this ../_build/default/bin/asli.exe - # and the include path that we need is ../_build/default/runtime/include + # directly out of the build tree and the path looks like this ../_build/install/default/bin/asli + # and the include path that we need is ../_build/install/default/runtime/include bindir = os.path.dirname(asli) rootdir = os.path.dirname(bindir) - path = os.path.join(rootdir, "runtime/include") + path = os.path.join(rootdir, "lib/asli/runtime_include") c_flags = [f"-I{path}"] c_flags.extend(backend_c_flags[backend]) return c_flags @@ -279,7 +279,7 @@ def get_ld_flags(asli, backend): # and the include path that we need is ../_build/install/default/runtime bindir = os.path.dirname(asli) rootdir = os.path.dirname(bindir) - path = os.path.join(rootdir, "runtime/libASL.a") + path = os.path.join(rootdir, "lib/asli/runtime/libASL.a") ld_flags = [path] if backend == "sc": sc_types_dir = os.environ.get('SC_TYPES_DIR') diff --git a/bin/asli.ml b/bin/asli.ml index 1fd95f37..a1158d08 100644 --- a/bin/asli.ml +++ b/bin/asli.ml @@ -411,6 +411,30 @@ let banner = let usage_msg = version ^ "\nusage: asli ... \n" +(* Use PATH to search for the executable based on the name in argv[0] *) +let get_executable_path _ : string = + let exe_name = Sys.argv.(0) in + let search_path = if Filename.is_relative exe_name + then Sys.getenv "PATH" |> String.split_on_char ':' + else [] + in + let opt_path = List.find_map (fun dir -> + (* Note: we do not use Unix.realpath because that removes symlinks *) + let filename = Filename.concat dir exe_name in + if Sys.file_exists filename + then Some filename + else None + ) + (""::search_path) + in + ( match opt_path with + | Some path -> path + | None -> + Printf.printf "Error: unable to locate executable on PATH\n"; + exit 1 + ) + + let _ = Arg.parse options (fun s -> opt_filenames := !opt_filenames @ [ s ]) usage_msg @@ -419,7 +443,11 @@ let main () = Ocolor_format.prettify_formatter Format.std_formatter; Ocolor_config.set_color_capability Ocolor_config.Color4 end; - let paths = Option.value (Sys.getenv_opt "ASL_PATH") ~default:"." + + let exe_dir = Filename.dirname (get_executable_path ()) in + let share_dir = Filename.concat exe_dir "../share/asli/stdlib" in + let default_path = share_dir ^ ":." in + let paths = Option.value (Sys.getenv_opt "ASL_PATH") ~default:default_path |> String.split_on_char ':' in if !opt_print_version then Printf.printf "%s\n" version else if !opt_print_cflags then begin diff --git a/demo/Makefile b/demo/Makefile index 457d5c54..84b7957d 100644 --- a/demo/Makefile +++ b/demo/Makefile @@ -8,8 +8,8 @@ .default: test ASL_PATH = ..:. -ASLI = ../_build/default/bin/asli.exe -ASL2C = ../_build/default/bin/asl2c.py +ASLI = ../_build/install/default/bin/asli +ASL2C = ../_build/install/default/bin/asl2c ################################################################ # Test whether we have GNU as or clang emulating as diff --git a/libASL/asl_parser.messages b/libASL/asl_parser.messages index ea29d8f0..ac4c055f 100644 --- a/libASL/asl_parser.messages +++ b/libASL/asl_parser.messages @@ -4849,7 +4849,7 @@ stmt_command_start: CASE ID OF WHEN ID EQ_GT OTHERWISE EQ_GT BEGIN END CATCH ## In state 482, spurious reduction of production opt_otherwise -> OTHERWISE EQ_GT block ## -Malformed case statement. +Missing "end" in case statement. The syntax of case statements is "case $1 of when => @@ -4903,7 +4903,7 @@ stmt_command_start: FOR ID EQ ID DOWNTO ID DO BEGIN END CATCH ## In state 472, spurious reduction of production block -> list(stmt) ## -Malformed for statement. +Missing "end" in for statement. The syntax of for statements is "for = to/downto do end" @@ -5056,7 +5056,7 @@ stmt_command_start: IF ID THEN ELSE BEGIN END CATCH ## In state 498, spurious reduction of production optional_else -> ELSE block ## -Malformed if statement. +Missing "end" in if statement. The syntax of if statements is "if then else end" or @@ -5301,7 +5301,7 @@ stmt_command_start: TRY CATCH OTHERWISE EQ_GT BEGIN END CATCH ## In state 482, spurious reduction of production opt_otherwise -> OTHERWISE EQ_GT block ## -Malformed try-catch statement. +Missing "end" in try-catch statement. The syntax of try-catch statements is "try @@ -5952,7 +5952,7 @@ declarations_start: GETTER ID LBRACK RBRACK EQ_GT INTEGER BEGIN BEGIN END CATCH ## In state 472, spurious reduction of production block -> list(stmt) ## -Malformed getter declaration. +Missing "end" in getter declaration. The syntax of getter declarations is "getter $8$7[ $5 ] => $2 begin $0 @@ -6035,7 +6035,7 @@ declarations_start: GETTER ID EQ_GT INTEGER BEGIN BEGIN END CATCH ## In state 472, spurious reduction of production block -> list(stmt) ## -Malformed getter declaration. +Missing "end" in getter declaration. The syntax of getter declarations is "getter $5$4 => $2 begin $0 @@ -6104,9 +6104,9 @@ declarations_start: FUNC ID LBRACE ID RBRACE WHILE Malformed function declaration. The syntax of function declarations is - "func $1$0() => ..." + "func $2$1$0() => ..." or - "func $1$0() ..." + "func $2$1$0() ..." declarations_start: FUNC ID LPAREN WHILE ## @@ -6123,9 +6123,9 @@ declarations_start: FUNC ID LPAREN WHILE Malformed function declaration. The syntax of function declarations is - "func $2$1() => ..." + "func $3$2$1() => ..." or - "func $2$1() ..." + "func $3$2$1() ..." @@ -6202,7 +6202,7 @@ declarations_start: FUNC ID LPAREN RPAREN EQ_GT INTEGER BEGIN WHERE Malformed function body. The syntax of function declarations is - "func $7$6($4) => $1 begin + "func $8$7$6($4) => $1 begin end" @@ -6224,9 +6224,9 @@ declarations_start: FUNC ID LPAREN RPAREN EQ_GT INTEGER BEGIN BEGIN END CATCH ## In state 472, spurious reduction of production block -> list(stmt) ## -Malformed function declaration. +Missing "end" in function declaration. The syntax of function declarations is - "func $8$7($5) => $2 begin + "func $9$8$7($5) => $2 begin $0 end" @@ -6243,7 +6243,7 @@ declarations_start: FUNC ID LPAREN RPAREN BEGIN WHERE Malformed procedure body. The syntax of procedure declarations is - "func $5$4($2) begin + "func $6$5$4($2) begin end" @@ -6265,13 +6265,13 @@ declarations_start: FUNC ID LPAREN RPAREN BEGIN BEGIN END CATCH ## In state 472, spurious reduction of production block -> list(stmt) ## -Malformed procedure body. +Missing "end" in procedure body. The syntax of procedure declarations is - "func $6$5($3) begin - $0 + "func $7$6$5($3) begin end" + declarations_start: ENUMERATION WHILE ## ## Ends in an error in state: 594. diff --git a/libASL/asl_utils.ml b/libASL/asl_utils.ml index 8eea762d..5c2c0be3 100644 --- a/libASL/asl_utils.ml +++ b/libASL/asl_utils.ml @@ -766,6 +766,24 @@ let identify_impure_funs (isConstant : Ident.t -> bool) | _ -> ()) ds; + (* A function is also treated as impure if we have a function type + * but no definition + *) + let name_of_fundefn (d : AST.declaration) : Ident.t option = + ( match d with + | Decl_FunDefn (f, _, _, _) -> Some f + | _ -> None + ) + in + let defined = IdentSet.of_list (List.filter_map name_of_fundefn ds) in + List.iter (fun d -> + ( match d with + | Decl_FunType (f, _, _) when not (IdentSet.mem f defined) -> + impure := IdentSet.add f !impure + | _ -> () + )) + ds; + (* globally impure if it calls a locally impure function *) callers (IdentSet.elements !impure) ds diff --git a/libASL/backend_c.ml b/libASL/backend_c.ml index 592b6a33..5b92d798 100644 --- a/libASL/backend_c.ml +++ b/libASL/backend_c.ml @@ -1651,6 +1651,7 @@ let mk_ffi_export_wrapper let pp_wrapper fmt = PP.fprintf fmt "// Export wrapper for %a@.@." ident c_name; wrap_extern true fmt (fun fmt -> + pp_proto fmt; PP.fprintf fmt "%a {" pp_c_function_header (); indented fmt (fun _ -> pp_export_body fmt); PP.fprintf fmt "@,}@." diff --git a/libASL/lexer.mll b/libASL/lexer.mll index 0b576a5b..ce609a89 100644 --- a/libASL/lexer.mll +++ b/libASL/lexer.mll @@ -72,6 +72,8 @@ let keywords : (string * Asl_parser.token) list = [ ("with", WITH); ] +let prev_else_token_pos = ref (-1) + let update_location lexbuf opt_file line = let pos = lexbuf.Lexing.lex_curr_p in let new_file = match opt_file with @@ -121,10 +123,30 @@ rule token = parse | ['0'-'9']+ '.' ['0'-'9']+ as lxm { REALLIT(lxm) } | ['0'-'9'] ['0'-'9' '_']* as digits { INTLIT(None, Z.of_string digits) } | ['a'-'z' 'A'-'Z' '_'] ['a'-'z' 'A'-'Z' '0'-'9' '_']* as lxm { + let tok = ( match List.assoc_opt lxm keywords with | Some x -> x | None -> ID(lxm) ) + in + (* If the code accidentally uses "else if" instead of "elsif", + * then parsing will eventually fail with a report about a missing + * "end". But that error report can come much later (e.g., at the end + * of the function and it is hard to find the actual cause of the error. + * + * So, the following code performs a heuristic check for "else" followed + * by "if" in the same line - in the hope of catching most places that + * this can go wrong. + *) + let follows_within x y dist = x < y && (y-x) < dist + in + if tok = IF && follows_within (!prev_else_token_pos) (Lexing.lexeme_start lexbuf) 2 then begin + let pos = Lexing.lexeme_start_p lexbuf in + Printf.printf "Warning: 'else if' should possibly be written as 'elsif' at %s:%d\n%!" + pos.pos_fname pos.pos_lnum + end; + if tok = ELSE then prev_else_token_pos := Lexing.lexeme_end lexbuf; + tok } (* delimiters *) diff --git a/libASL/tcheck.ml b/libASL/tcheck.ml index 21a93620..ffc7e6ea 100644 --- a/libASL/tcheck.ml +++ b/libASL/tcheck.ml @@ -1573,19 +1573,28 @@ let get_var (env : Env.t) (loc : Loc.t) (v : Ident.t) : var_info = (** check that we have exactly the fields required *) let check_field_assignments (loc : Loc.t) (fs : (Ident.t * ty) list) (fas : (Ident.t * expr) list) : unit = - let expected = IdentSet.of_list (List.map fst fs) in - let assigned = IdentSet.of_list (List.map fst fas) in + let fields1 = List.map fst fs in + let fields2 = List.map fst fas in + let expected = IdentSet.of_list fields1 in + let assigned = IdentSet.of_list fields2 in if not (IdentSet.equal assigned expected) then begin let missing = IdentSet.elements (IdentSet.diff expected assigned) in let extra = IdentSet.elements (IdentSet.diff assigned expected) in - let msg = "record initializer is missing fields " + let msg = "record initializer is missing field[s] " ^ String.concat ", " (List.map Ident.to_string missing) - ^ " and/or has extra fields " + ^ " and/or has extra field[s] " ^ String.concat ", " (List.map Ident.to_string extra) in raise (TypeError (loc, msg)) + end else if not (List.for_all2 Ident.equal fields1 fields2) then begin + let msg = "record initializer must set fields in the same order as the type declaration." + ^ "\nOrder of fields in type declaration: " ^ String.concat ", " (List.map Ident.to_string fields1) + ^ "\nOrder of fields in record initializer: " ^ String.concat ", " (List.map Ident.to_string fields2) + in + raise (TypeError (loc, msg)) end + (** Typecheck list of expressions *) let rec tc_exprs (env : Env.t) (loc : Loc.t) (xs : AST.expr list) : (AST.expr * AST.ty) list = diff --git a/libASL/xform_bitslices.ml b/libASL/xform_bitslices.ml index a5d7d83d..c4f320aa 100644 --- a/libASL/xform_bitslices.ml +++ b/libASL/xform_bitslices.ml @@ -23,6 +23,12 @@ open Asl_utils open Builtin_idents open Utils +let is_constant (x : AST.expr) : bool = + ( match x with + | Expr_Lit _ -> true + | _ -> false + ) + let transform_slices : bool ref = ref true let transform_non_slices (n : AST.expr) (w : AST.expr) (i : AST.expr) @@ -55,7 +61,7 @@ let transform (loc : Loc.t) (n : AST.expr) (w : AST.expr) (i : AST.expr) | Expr_Slices (_, _, [Slice_Single _]) -> raise (InternalError (loc, "Slice_Single not expected", (fun fmt -> Asl_fmt.expr fmt x), __LOC__)) - | Expr_Slices (Type_Bits (we, _), e, [Slice_LoWd (lo, wd)]) -> + | Expr_Slices (Type_Bits (we, _), e, [Slice_LoWd (lo, wd)]) when not (is_constant wd) -> (* generate "zero_extend_bits((e >> lo) AND mk_mask(wd, we), n) << i" *) let e1 = mk_lsr_bits we e lo in let e2 = mk_and_bits we e1 (Asl_utils.mk_mask wd we) in diff --git a/libASL/xform_constprop.ml b/libASL/xform_constprop.ml index a6ad7076..0ec408ed 100644 --- a/libASL/xform_constprop.ml +++ b/libASL/xform_constprop.ml @@ -638,17 +638,11 @@ and xform_stmt (env : Env.t) (x : AST.stmt) : AST.stmt list = ) (** Create local environment and add parameters and arguments *) -let mk_fun_env (env : Eval.GlobalEnv.t) (loc : Loc.t) (f : Ident.t) : Env.t = +let mk_fun_env (env : Eval.GlobalEnv.t) (fty : AST.function_type) : Env.t = let fun_env = Env.newEnv env in - ( match Eval.GlobalEnv.get_function env f with - | Some (tvs, args, _, _) -> - List.iter (fun tv -> Env.addLocalConst fun_env tv Values.bottom) tvs; - List.iter (fun v -> Env.addLocalConst fun_env v Values.bottom) args - | _ -> - let msg = "undeclared function" in - raise - (InternalError (loc, msg, (fun fmt -> Asl_fmt.funname fmt f), __LOC__)) - ); + List.iter (fun (tv, _) -> Env.addLocalConst fun_env tv Values.bottom) fty.parameters; + List.iter (fun (v, _, _) -> Env.addLocalConst fun_env v Values.bottom) fty.args; + Option.iter (fun (v, _) -> Env.addLocalConst fun_env v Values.bottom) fty.setter_arg; fun_env let xform_decl (genv : Eval.GlobalEnv.t) (d : AST.declaration) : AST.declaration @@ -681,11 +675,11 @@ let xform_decl (genv : Eval.GlobalEnv.t) (d : AST.declaration) : AST.declaration let e' = xform_expr env e in Decl_Config (v, ty', e', loc) | Decl_FunType (f, fty, loc) -> - let env = mk_fun_env genv loc f in + let env = mk_fun_env genv fty in let fty' = xform_funtype env fty in Decl_FunType (f, fty', loc) | Decl_FunDefn (f, fty, body, loc) -> - let env = mk_fun_env genv loc f in + let env = mk_fun_env genv fty in let fty' = xform_funtype env fty in let body' = xform_stmts env body in Decl_FunDefn (f, fty', body', loc) diff --git a/mk_install.py b/mk_install.py new file mode 100755 index 00000000..cfbc4b8d --- /dev/null +++ b/mk_install.py @@ -0,0 +1,95 @@ +#! /usr/bin/env python3 + +""" +Build asli and install it into directory without including +a full copy of ~/.opam. + +Typical usage: + + cd asl-interpreter + ./mk_install.py --release-dir=$HOME/release --version=`date -I` + # will be released into ${release_dir}/${version} + +""" + +import argparse +import os +import os.path +import pathlib +import shutil +import subprocess +import sys +import textwrap + +# Run command (printing command first if verbose) and abort if command fails +# (The assumption is that the command printed a useful/meaningful error message already) +def run(cmd): + print(" ".join(cmd)) + try: + subprocess.run(cmd, check=True) + except subprocess.CalledProcessError as e: + print(f"Command '{' '.join(e.cmd)}' returned non-zero exit status {e.returncode}.") + sys.exit(e.returncode) + +def write_to_file(filename, contents): + with open(filename, 'w') as f: + f.write(contents) + +def main() -> int: + parser = argparse.ArgumentParser( + prog = 'mk_install', + description = __doc__, + formatter_class=argparse.RawDescriptionHelpFormatter, + ) + parser.add_argument("--release-dir", help="release directory", metavar="release_dir", required=True) + parser.add_argument("--version", help="version (used as subdirectory name)", metavar="version", required=True) + args = parser.parse_args() + + opam_switch = os.environ.get('OPAM_SWITCH_PREFIX') + release_dir = f"{args.release_dir}/{args.version}" + release_dir = os.path.abspath(release_dir) + bin_dir = f"{release_dir}/bin" + lib_dir = f"{release_dir}/lib" + sh_file = f"{release_dir}/env.sh" + csh_file = f"{release_dir}/env.csh" + + if os.path.exists(release_dir): + print(f"Error: release_dir '{release_dir}' already exists") + sys.exit(1) + + print(f"Building release") + + run(["make", "build"]) + + print(f"Copying release to {release_dir}") + + shutil.copytree(f"_build/install/default", release_dir, dirs_exist_ok=True) + shutil.rmtree(f"{release_dir}/lib/asli/libASL") # just a copy of the source code + + # copy Z3 file over into release (user will need to set LD_LIBRARY_PATH to lib_dir) + shutil.copy(f"{opam_switch}/lib/stublibs/libz3.so", lib_dir) + + print(f"Copied release in {release_dir}") + + write_to_file(sh_file, textwrap.dedent(f""" +export ASLI_INSTALL_DIR={release_dir} +export ASLI_BIN_DIR={bin_dir} +export LD_LIBRARY_PATH={lib_dir} +export PATH={bin_dir}:$PATH + """)) + + write_to_file(csh_file, textwrap.dedent(f""" +setenv ASLI_INSTALL_DIR {release_dir} +setenv ASLI_BIN_DIR {bin_dir} +setenv LD_LIBRARY_PATH {lib_dir} +setenv PATH {bin_dir}:$PATH + """)) + + print(f"Generated environment setting files in {sh_file} and {csh_file}") + + sys.exit(0) + + +if __name__ == "__main__": + main() + diff --git a/tests/lit.cfg b/tests/lit.cfg index 42f1d9b9..8f9d8d26 100644 --- a/tests/lit.cfg +++ b/tests/lit.cfg @@ -4,8 +4,8 @@ import subprocess lit_cfg_path = os.path.dirname(os.path.abspath(__file__)) asl_path = os.path.dirname(lit_cfg_path) -asli_bin_path = os.path.join(asl_path, "_build/default/bin/asli.exe") -asl2c_path = os.path.join(asl_path, "_build/default/bin/asl2c.py") +asli_bin_path = os.path.join(asl_path, "_build/install/default/bin/asli") +asl2c_path = os.path.join(asl_path, "_build/install/default/bin/asl2c") backend = os.environ.get("ASL_BACKEND") ac_types_dir = os.environ.get("AC_TYPES_DIR") sc_types_dir = os.environ.get("SC_TYPES_DIR") diff --git a/tests/lit/tcheck/record_init_00.asl b/tests/lit/tcheck/record_init_00.asl index 2f93ea0d..bedd7ebd 100644 --- a/tests/lit/tcheck/record_init_00.asl +++ b/tests/lit/tcheck/record_init_00.asl @@ -9,5 +9,5 @@ record R{ func T() => R begin return R{x=1, z=3}; -// CHECK: Type error: record initializer is missing fields y and/or has extra fields z +// CHECK: Type error: record initializer is missing field[s] y and/or has extra field[s] z end diff --git a/tests/lit/tcheck/record_init_02.asl b/tests/lit/tcheck/record_init_02.asl new file mode 100644 index 00000000..63eadc1d --- /dev/null +++ b/tests/lit/tcheck/record_init_02.asl @@ -0,0 +1,16 @@ +// RUN: not %asli --batchmode %s | filecheck %s +// Copyright (C) 2023-2025 Intel Corporation + +record R{ + x : integer; + y : integer; +}; + +func T() => R +begin + return R{y=3, x=1}; +// CHECK: Type error: record initializer must set fields in the same order as the type declaration. +// CHECK-NEXT: Order of fields in type declaration: x, y +// CHECK-NEXT: Order of fields in record initializer: y, x +end + diff --git a/tests/lit/tcheck/records_02.asl b/tests/lit/tcheck/records_02.asl index 5adde55c..63126da1 100644 --- a/tests/lit/tcheck/records_02.asl +++ b/tests/lit/tcheck/records_02.asl @@ -9,5 +9,5 @@ record R { func F() => R begin return R{x = 1}; -// CHECK: Type error: record initializer is missing fields y and/or has extra fields +// CHECK: Type error: record initializer is missing field[s] y and/or has extra field[s] end