Skip to content

Commit

Permalink
remove python instrumentation and fix some inline annotations to work
Browse files Browse the repository at this point in the history
with 5.2
  • Loading branch information
zapashcanon committed May 28, 2024
1 parent 3fbe3e8 commit 6d6a571
Show file tree
Hide file tree
Showing 10 changed files with 16 additions and 100 deletions.
2 changes: 0 additions & 2 deletions dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -73,8 +73,6 @@
(tyxml :dev)
digestif
xmlm
pyml
re2
(hc (>= 0.3))
dune-site)
(sites (share pyc) (share binc) (share libc)))
2 changes: 0 additions & 2 deletions owi.opam
Original file line number Diff line number Diff line change
Expand Up @@ -41,8 +41,6 @@ depends: [
"tyxml" {dev}
"digestif"
"xmlm"
"pyml"
"re2"
"hc" {>= "0.3"}
"dune-site"
]
Expand Down
23 changes: 0 additions & 23 deletions src/c_processing/c_instrumentor.ml

This file was deleted.

65 changes: 5 additions & 60 deletions src/cmd/cmd_c.ml
Original file line number Diff line number Diff line change
Expand Up @@ -11,66 +11,15 @@ type metadata =
; files : Fpath.t list
}

let pre_patterns : (Re2.t * string) array =
Array.map
(fun (regex, template) -> (Re2.create_exn regex, template))
[| ( "void\\s+reach_error\\(\\)\\s*\\{.*\\}"
, "void reach_error() { owi_assert(0); }" )
(* ugly: Hack to solve duplicate errors on compilation *)
(* ; ("void\\s+(assert|assume)\\(", "void old_\\1(") *)
|]

let patch_with_regex ~patterns (data : string) : string =
Array.fold_left
(fun data (regex, template) -> Re2.rewrite_exn regex ~template data)
data patterns

let patch ~src ~dst : unit Result.t =
let* data = OS.File.read src in
let data = patch_with_regex ~patterns:pre_patterns data in
let data =
String.concat "\n"
[ "#define __attribute__(x)"
; "#define __extension__"
; "#define __restrict"
; "#define __inline"
; "#include <owi.h>"
; data
]
in
OS.File.write dst data

let copy ~src ~dst : Fpath.t Result.t =
let* data = OS.File.read src in
let+ () = OS.File.write dst data in
dst

let instrument_file ?(skip = false) ~includes ~workspace file : Fpath.t Result.t
=
(* TODO: remove this copy ? *)
let instrument_file ~workspace file : Fpath.t Result.t =
let dst = Fpath.(workspace // base (file -+ ".c")) in
if skip then copy ~src:file ~dst
else begin
Logs.app (fun m -> m "instrumenting %a" Fpath.pp file);
let* () = patch ~src:file ~dst in
let pypath =
Format.asprintf "%a"
(Format.pp_list
~pp_sep:(fun fmt () -> Format.pp_char fmt ':')
Fpath.pp )
C_share.py_location
in
let+ () = OS.Env.set_var "PYTHONPATH" (Some pypath) in
begin
try
Py.initialize ();
C_instrumentor.instrument dst includes;
Py.finalize ()
with Py.E (errtype, errvalue) ->
let pp = Py.Object.format in
Logs.warn (fun m -> m "instrumentor: %a: %a" pp errtype pp errvalue)
end;
dst
end
copy ~src:file ~dst

let compile ~includes ~opt_lvl (files : Fpath.t list) : Fpath.t Result.t =
let flags =
Expand Down Expand Up @@ -154,18 +103,14 @@ let metadata ~workspace arch property files : unit Result.t =
let* res = OS.File.with_oc fpath out_metadata { arch; property; files } in
res

let cmd debug arch property testcomp workspace workers opt_lvl includes files
let cmd debug arch property _testcomp workspace workers opt_lvl includes files
profiling unsafe optimize no_stop_at_failure no_values
deterministic_result_order concolic : unit Result.t =
if debug then Logs.set_level (Some Debug);
let workspace = Fpath.v workspace in
let includes = C_share.lib_location @ includes in
let* (_exists : bool) = OS.Dir.create ~path:true workspace in
(* skip instrumentation if not in test-comp mode *)
let skip = (not testcomp) || Sys.getenv_opt "RUNNER_OS" = Some "macOS" in
let* (nfiles : Fpath.t list) =
list_map (instrument_file ~skip ~includes ~workspace) files
in
let* (nfiles : Fpath.t list) = list_map (instrument_file ~workspace) files in
let* modul = compile ~includes ~opt_lvl nfiles in
let* () = metadata ~workspace arch property files in
let workspace = Fpath.(workspace / "test-suite") in
Expand Down
2 changes: 0 additions & 2 deletions src/dune
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
binary_parser
binary_to_text
binary_types
c_instrumentor
c_share
c_share_site
check
Expand Down Expand Up @@ -97,7 +96,6 @@
menhirLib
ocaml_intrinsics
ppxlib
pyml
re2
sedlex
uutf
Expand Down
10 changes: 5 additions & 5 deletions src/interpret/interpret.ml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ module Make (P : Interpret_intf.P) :
open P
open Value
open Choice
module Stack = Stack.Make (Value) [@@inlined hint]
module Stack = Stack.Make [@inlined hint] (Value)

module I32 = struct
include I32
Expand Down Expand Up @@ -1584,7 +1584,7 @@ module Make (P : Interpret_intf.P) :
type value = Value.t
end

module Concrete = Make (Concrete) [@@inlined hint]
module SymbolicP = Make (Symbolic.P) [@@inlined hint]
module SymbolicM = Make (Symbolic.M) [@@inlined hint]
module Concolic = Make (Concolic.P) [@@inlined hint]
module Concrete = Make [@inlined hint] (Concrete)
module SymbolicP = Make [@inlined hint] (Symbolic.P)
module SymbolicM = Make [@inlined hint] (Symbolic.M)
module Concolic = Make [@inlined hint] (Concolic.P)
2 changes: 1 addition & 1 deletion src/link/link.ml
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,7 @@ let load_global (ls : 'f state) (import : binary global_type Imported.t) :
else Ok global

module Eval_const = struct
module Stack = Stack.Make (V) [@@inlined hint]
module Stack = Stack.Make [@inlined hint] (V)

(* TODO: const ibinop *)
let ibinop stack nn (op : ibinop) =
Expand Down
2 changes: 1 addition & 1 deletion src/script/script.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@

open Types
open Syntax
module Stack = Stack.Make (V) [@@inlined hint]
module Stack = Stack.Make [@inlined hint] (V)

module Host_externref = struct
type t = int
Expand Down
4 changes: 2 additions & 2 deletions src/symbolic/symbolic.ml
Original file line number Diff line number Diff line change
Expand Up @@ -182,12 +182,12 @@ struct
end

module P = struct
include MakeP (Thread) (Symbolic_choice.Multicore) [@@inlined hint]
include MakeP [@inlined hint] (Thread) (Symbolic_choice.Multicore)
module Choice = Symbolic_choice.Multicore
end

module M = struct
include MakeP (Thread) (Symbolic_choice.Minimalist) [@@inlined hint]
include MakeP [@inlined hint] (Thread) (Symbolic_choice.Minimalist)
module Choice = Symbolic_choice.Minimalist
end

Expand Down
4 changes: 2 additions & 2 deletions test/script/gc.t
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@
Raised at Owi__Typecheck.typecheck_instr in file "src/typecheck/typecheck.ml", line 478, characters 4-16
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Owi__Typecheck.typecheck_expr in file "src/typecheck/typecheck.ml", line 490, characters 15-59
Called from Owi__Typecheck.typecheck_function in file "src/typecheck/typecheck.ml", line 512, characters 6-112
Called from Owi__Typecheck.typecheck_function in file "src/typecheck/typecheck.ml", lines 512-514, characters 6-17
Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
Called from Owi__Compile.Text.until_typecheck in file "src/compile.ml", line 26, characters 16-33
Called from Owi__Compile.Text.until_optimize in file "src/compile.ml", line 30, characters 13-38
Expand All @@ -36,7 +36,7 @@
Called from Owi__Script.exec in file "src/script/script.ml", line 260, characters 21-56
Called from Owi__Syntax.list_iter.(fun) in file "src/utils/syntax.ml", line 22, characters 14-17
Called from Stdlib__List.iter in file "list.ml", line 112, characters 12-15
Called from Owi__Syntax.list_iter in file "src/utils/syntax.ml", line 20, characters 4-157
Called from Owi__Syntax.list_iter in file "src/utils/syntax.ml", lines 20-27, characters 4-7
Called from Cmdliner_term.app.(fun) in file "cmdliner_term.ml", line 24, characters 19-24
Called from Cmdliner_eval.run_parser in file "cmdliner_eval.ml", line 35, characters 37-44
[125]
Expand Down

0 comments on commit 6d6a571

Please sign in to comment.