Skip to content

Commit

Permalink
Merge branch 'master' into taramana_rust_val_test
Browse files Browse the repository at this point in the history
  • Loading branch information
@msprotz
msprotz authored Feb 20, 2025
2 parents 1ad3668 + bbaa528 commit 2a00494
Show file tree
Hide file tree
Showing 10 changed files with 240 additions and 167 deletions.
31 changes: 10 additions & 21 deletions book/tutorial/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,11 +46,10 @@ FSTAR_EXTRACT = --extract 'OCaml:-* +Spec'
# But also:
# - --cmi, for cross-module inlining, a must-have for anyone who relies on
# inline_for_extraction in the presence of interfaces
# - --cache_checked_modules to rely on a pre-built ulib and krmllib
# - --cache_dir, to avoid polluting our generated build artifacts outside o
# - --cache_dir, to place checked files there

FSTAR_NO_FLAGS = $(FSTAR_EXE) --ext context_pruning \
--odir obj --cache_checked_modules $(FSTAR_INCLUDES) --cmi \
--odir obj $(FSTAR_INCLUDES) --cmi \
--already_cached 'Prims FStar LowStar C Spec.Loops TestLib WasmSupport' --warn_error '+241@247+285' \
--cache_dir obj

Expand All @@ -72,7 +71,7 @@ FSTAR_ROOTS = $(wildcard $(addsuffix /*.fsti,$(SOURCE_DIRS))) \
# mtime of the moved files.
ifndef MAKE_RESTARTS
.depend: .FORCE
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) --output_deps_to $@
$(FSTAR_NO_FLAGS) --dep full $(notdir $(FSTAR_ROOTS)) $(FSTAR_EXTRACT) -o $@

.PHONY: .FORCE
.FORCE:
Expand Down Expand Up @@ -115,32 +114,22 @@ obj:
# up-to-date (checksum matches, file unchanged), but this will confuse
# make and result in endless rebuilds. So, we touch that file.
%.checked: | obj
$(FSTAR) $< $(FSTAR_FLAGS) && touch -c $@
$(FSTAR) $(FSTAR_FLAGS) -c $< -o $@ && touch -c $@

# Extraction
# ----------

# A few mismatches here between the dependencies present in the .depend and the
# expected F* invocation. In .depend:
#
# obj/Bignum_Impl.ml: obj/Bignum.Impl.fst.checked ... more dependencies ...
#
# But F* wants (remember that F* searches for source files anywhere on the
# include path):
#
# fstar Bignum.Impl.fst --extract_module BigNum.Impl
#
# We use basename because we may also extract krml files from .fsti.checked
# files (not true for OCaml, we don't extract mlis from fstis).
.PRECIOUS: obj/%.ml
obj/%.ml:
$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen OCaml \
--extract_module $(basename $(notdir $(subst .checked,,$<)))
$(FSTAR) --codegen OCaml $< -o $@

# By default, krml extraction in F* will extract every module into a
# single out.krml file. Make sure to extract the single module we want.
.PRECIOUS: obj/%.krml
obj/%.krml:
$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<)))
$(FSTAR) $< --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
-o $@

obj/Specs_Driver.ml: specs/ml/Specs_Driver.ml
# This ensures that all the source directories are not polluted with
Expand Down
10 changes: 5 additions & 5 deletions krmllib/Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ ifneq ($(RESOURCEMONITOR),)
RUNLIM = runlim -p -o $@.runlim
endif

FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_checked_modules --cache_dir obj \
FSTAR = $(RUNLIM) $(FSTAR_EXE) $(FSTAR_OPTIONS) --cache_dir obj \
$(addprefix --include , $(INCLUDE_PATHS)) --cmi \
--already_cached 'Prims FStar -FStar.Krml.Endianness LowStar -LowStar.Lib'

Expand Down Expand Up @@ -64,7 +64,7 @@ FSTAR_EXTRACT+=-FStar.Stubs # This namespace is for interfaces into the compiler
ifndef NODEPEND
ifndef MAKE_RESTARTS
.depend: .FORCE obj
$(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) --output_deps_to $@
$(FSTAR) $(OTHERFLAGS) --extract '$(FSTAR_EXTRACT)' --dep full $(ROOTS) -o $@

.PHONY: .FORCE
.FORCE:
Expand All @@ -77,15 +77,15 @@ obj:
mkdir $@

%.checked: | obj
$(FSTAR) $(OTHERFLAGS) $< && \
$(FSTAR) $(OTHERFLAGS) -c $< -o $@ && \
touch $@

verify-all: $(ALL_CHECKED_FILES)

$(EXTRACT_DIR)/%.krml: | .depend
$(FSTAR) $(OTHERFLAGS) --codegen krml \
$(FSTAR) $(OTHERFLAGS) $< --codegen krml \
--extract_module $(basename $(notdir $(subst .checked,,$<))) \
$(notdir $(subst .checked,,$<)) && \
-o $@ && \
touch -c $@

# We don't extract LowStar.Lib as everything is generic data structures that
Expand Down
180 changes: 123 additions & 57 deletions lib/Driver.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,34 +6,40 @@

open Warn

(* Abstracting over - (dash) for msvc. vs. gcc-like. *)
(** These three filled in by [detect_cc] and others *)
let cc = ref ""
let cc_args = ref []
let cc_flavor = ref Options.Generic

(* Abstracting over - (dash) for msvc. vs. gcc-like. This module
reads cc_flavor. *)
module Dash = struct
let i dir =
if !Options.cc = "msvc" then
if !cc_flavor = MSVC then
[ "/I"; dir ]
else
[ "-I"; dir ]

let c file =
if !Options.cc = "msvc" then
if !cc_flavor = MSVC then
[ "/c"; file ]
else
[ "-c"; file ]

let d opt =
if !Options.cc = "msvc" then
if !cc_flavor = MSVC then
"/D" ^ opt
else
"-D" ^ opt

let o_obj file =
if !Options.cc = "msvc" then
if !cc_flavor = MSVC then
[ "/Fo:"; file ]
else
[ "-o"; file ]

let o_exe file =
if !Options.cc = "msvc" then
if !cc_flavor = MSVC then
[ "/Fe:"; file ]
else
[ "-o"; file ]
Expand All @@ -44,6 +50,8 @@ module P = Process
(* Note: don't open [Process], otherwise any reference to [Output] will be
* understood as a cyclic dependency on our own [Output] module. *)

let cc_flavor_callback = ref (fun (_ : Options.compiler_flavor) -> ())

(** These three variables filled in by [detect_fstar] *)
let fstar = Options.fstar
let fstar_lib = ref ""
Expand All @@ -57,10 +65,6 @@ let include_dir = ref ""
let misc_dir = ref ""
let krml_rev = ref "<unknown>"

(** These two filled in by [detect_gcc] and others *)
let cc = ref ""
let cc_args = ref []

(** The base tools *)
let readlink = ref ""

Expand Down Expand Up @@ -339,41 +343,46 @@ let run_fstar verify skip_extract skip_translate files =
exit 0;
!Options.tmpdir ^^ "out.krml"

let detect_gnu flavor =
if not !Options.silent then
KPrint.bprintf "%s⚙ KaRaMeL will drive the C compiler.%s Here's what we found:\n" Ansi.blue Ansi.reset;
let rec search = function
| fmt :: rest ->
let cmd = KPrint.bsprintf fmt flavor in
if success "which" [| cmd |] then
cc := cmd
else
search rest
| [] ->
Warn.fatal_error "gcc not found in path!";
let detect_compiler_flavor cc =
let is_gcc () =
try
(* If cc points to gcc, cc --version will say "cc version ...", instead of
gcc. So use -v instead, but that prints to stderr. *)
let rc = Process.run cc [| "-v" |] in
let lines = rc.stderr in
List.exists (fun l -> KString.starts_with l "gcc version") lines
with | _ -> false
in
let crosscc = if !Options.m32 then format_of_string "i686-w64-mingw32-%s" else format_of_string "x86_64-w64-mingw32-%s" in
search [ "%s-10"; "%s-9"; "%s-8"; "%s-7"; "%s-6"; "%s-5"; crosscc; "%s" ];

if not !Options.silent then
KPrint.bprintf "%sgcc is:%s %s\n" Ansi.underline Ansi.reset !cc;

if !Options.m32 then
cc_args := "-m32" :: !cc_args;
if not !Options.silent then
KPrint.bprintf "%s%s options are:%s %s\n" Ansi.underline !cc Ansi.reset
(String.concat " " !cc_args)


let detect_compcert () =
if success "which" [| "ccomp" |] then
cc := "ccomp"
else
Warn.fatal_error "ccomp not found in path!"

let is_clang () =
try
let lines = Process.read_stdout cc [| "--version" |] in
List.exists (fun l -> KString.exists l "clang version") lines
with | _ -> false
in
let is_compcert () =
try
let lines = Process.read_stdout cc [| "--version" |] in
List.exists (fun l -> KString.exists l "CompCert") lines
with | _ -> false
in
let is_msvc () =
try
let rc = Process.run cc [| |] in
let lines = rc.stderr in
List.exists (fun l -> KString.exists l "Microsoft") lines
with | _ -> false
in
if is_gcc () then Options.GCC
else if is_clang () then Options.Clang
else if is_compcert () then Options.Compcert
else if is_msvc () then Options.MSVC
else (
Warn.maybe_fatal_error ("detect_compiler_flavor", UnrecognizedCCompiler cc);
Generic
)

let fill_cc_args () =
(** For the side-effect of filling in [Options.include] *)
(** For the side-effect of filling in [Options.includes] *)
detect_karamel_if ();

cc_args :=
Expand All @@ -383,26 +392,83 @@ let fill_cc_args () =
@ List.rev !Options.ccopts
@ !cc_args

(* Sets cc, cc_flavor *)
let auto_detect_cc () =
(* !cc can be relative or absolute, `which` handles both. *)
if not (success "which" [| !cc |]) then
Warn.fatal_error "C compiler '%s' not found!" !cc;

if not !Options.silent then begin
(* If not absolute print realpath too *)
let real =
if KString.starts_with !cc "/" then
""
else
match
read_one_line !readlink [| "-f"; read_one_line "which" [| !cc |] |]
with
| exception _ -> " (couldn't resolve?)"
| s -> " (= " ^ s ^ ")"
in
KPrint.bprintf "%scc is:%s %s%s\n" Ansi.underline Ansi.reset !cc real
end;
match !Options.cc_flavor with
| Some f -> cc_flavor := f
| None -> cc_flavor := detect_compiler_flavor !cc

let detect_cc () =
detect_base_tools_if ();

if not !Options.silent then
KPrint.bprintf "%s⚙ KaRaMeL will drive the C compiler.%s Here's what we found:\n" Ansi.blue Ansi.reset;

(* Use Options.cc if passed, otherwise CC from env, otherwise "cc" *)
let cc_name =
if !Options.cc <> ""
then !Options.cc
else
match Sys.getenv "CC" with
| s -> s
| exception _ -> "cc"
in

if cc_name = "msvc" then (
(* We special-case "msvc" and use this wrapper script to find it
and set its environment up, it's not really feasible to
just find the cl.exe *)
KPrint.bprintf "%scc is:%s MSVC (will use cl-wrapper script)\n" Ansi.underline Ansi.reset;
cc := !misc_dir ^^ "cl-wrapper.bat";
cc_flavor := MSVC
) else (
(* Otherwise cc_name is a normal command or path like gcc/clang,
auto-detect its flavor. *)
cc := cc_name;
auto_detect_cc ()
);

if not !Options.silent then
KPrint.bprintf "%scc flavor is:%s %s\n" Ansi.underline Ansi.reset
(Options.string_of_compiler_flavor !cc_flavor);

(* Now that we detected the flavor, call this callback to
right default arguments for the compiler filled in. *)
!cc_flavor_callback !cc_flavor;

let detect_cc_if () =
fill_cc_args ();

if !cc_flavor = GCC && !Options.m32 then
cc_args := "-m32" :: !cc_args;

if not !Options.silent then
KPrint.bprintf "%scc options are:%s %s\n" Ansi.underline Ansi.reset
(String.concat " " !cc_args)

let detect_cc_if () =
if !cc = "" then
match !Options.cc with
| "gcc" ->
detect_gnu "gcc"
| "compcert" ->
detect_compcert ()
| "g++" ->
detect_gnu "g++"
| "clang" ->
detect_gnu "clang"
| "msvc" ->
cc := !misc_dir ^^ "cl-wrapper.bat";
| _ ->
fatal_error "Unrecognized value for -cc: %s" !Options.cc
detect_cc ()

let o_of_c f =
let dot_o = if !Options.cc = "msvc" then ".obj" else ".o" in
let dot_o = if !cc_flavor = MSVC then ".obj" else ".o" in
!Options.tmpdir ^^ Filename.chop_suffix (Filename.basename f) ".c" ^ dot_o


Expand Down
1 change: 1 addition & 0 deletions lib/Error.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ and raw_error =
| IfDefOnGlobal of lident
| NotLowStarCast of expr
| LibraryPointerAmbiguity of lident * expr
| UnrecognizedCCompiler of string

and location =
string
Expand Down
Loading

0 comments on commit 2a00494

Please sign in to comment.