Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
F
frama-c
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Deploy
Releases
Container Registry
Model registry
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
pub
frama-c
Commits
43fa28fc
Commit
43fa28fc
authored
4 years ago
by
Allan Blanchard
Browse files
Options
Downloads
Patches
Plain Diff
[wp] Fixes cache directory getter
parent
01bc9783
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/plugins/wp/Cache.ml
+43
-24
43 additions, 24 deletions
src/plugins/wp/Cache.ml
with
43 additions
and
24 deletions
src/plugins/wp/Cache.ml
+
43
−
24
View file @
43fa28fc
...
@@ -62,6 +62,23 @@ module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit)
...
@@ -62,6 +62,23 @@ module CACHEDIR = WpContext.StaticGenerator(Datatype.Unit)
let
get_dir
()
=
(
CACHEDIR
.
get
()
:>
string
)
let
get_dir
()
=
(
CACHEDIR
.
get
()
:>
string
)
let
is_session_dir
path
=
0
=
Filepath
.
Normalized
.
compare
path
(
Wp_parameters
.
get_session_dir
~
force
:
false
"cache"
)
let
get_usable_dir
?
(
make
=
false
)
()
=
let
path
=
CACHEDIR
.
get
()
in
let
parents
=
is_session_dir
path
in
let
path
=
(
path
:>
string
)
in
if
not
(
Sys
.
file_exists
path
)
&&
make
then
Extlib
.
mkdir
~
parents
path
0o755
;
if
not
(
Sys
.
is_directory
path
)
then
begin
Wp_parameters
.
warning
~
current
:
false
~
once
:
true
"Cache path is not a directory"
;
raise
Not_found
end
;
path
let
has_dir
()
=
let
has_dir
()
=
try
try
if
not
(
Wp_parameters
.
CacheEnv
.
get
()
)
then
if
not
(
Wp_parameters
.
CacheEnv
.
get
()
)
then
...
@@ -177,10 +194,8 @@ let get_cache_result ~mode hash =
...
@@ -177,10 +194,8 @@ let get_cache_result ~mode hash =
match
mode
with
match
mode
with
|
NoCache
|
Rebuild
->
VCS
.
no_result
|
NoCache
|
Rebuild
->
VCS
.
no_result
|
Update
|
Cleanup
|
Replay
|
Offline
->
|
Update
|
Cleanup
|
Replay
|
Offline
->
let
dir
=
get_dir
()
in
try
if
not
(
Sys
.
file_exists
dir
&&
Sys
.
is_directory
dir
)
then
let
dir
=
get_usable_dir
~
make
:
true
()
in
VCS
.
no_result
else
let
hash
=
Lazy
.
force
hash
in
let
hash
=
Lazy
.
force
hash
in
let
file
=
Printf
.
sprintf
"%s/%s.json"
dir
hash
in
let
file
=
Printf
.
sprintf
"%s/%s.json"
dir
hash
in
if
not
(
Sys
.
file_exists
file
)
then
VCS
.
no_result
if
not
(
Sys
.
file_exists
file
)
then
VCS
.
no_result
...
@@ -192,15 +207,16 @@ let get_cache_result ~mode hash =
...
@@ -192,15 +207,16 @@ let get_cache_result ~mode hash =
Wp_parameters
.
warning
~
current
:
false
~
once
:
true
Wp_parameters
.
warning
~
current
:
false
~
once
:
true
"invalid cache entry (%s)"
(
Printexc
.
to_string
err
)
;
"invalid cache entry (%s)"
(
Printexc
.
to_string
err
)
;
VCS
.
no_result
VCS
.
no_result
with
Not_found
->
VCS
.
no_result
let
set_cache_result
~
mode
hash
prover
result
=
let
set_cache_result
~
mode
hash
prover
result
=
match
mode
with
match
mode
with
|
NoCache
|
Replay
|
Offline
->
()
|
NoCache
|
Replay
|
Offline
->
()
|
Rebuild
|
Update
|
Cleanup
->
|
Rebuild
|
Update
|
Cleanup
->
let
dir
=
CACHEDIR
.
get
()
in
let
hash
=
Lazy
.
force
hash
in
let
hash
=
Lazy
.
force
hash
in
let
file
=
Printf
.
sprintf
"%s/%s.json"
(
dir
:>
string
)
hash
in
try
try
let
dir
=
get_usable_dir
~
make
:
true
()
in
let
file
=
Printf
.
sprintf
"%s/%s.json"
dir
hash
in
mark_cache
~
mode
hash
;
mark_cache
~
mode
hash
;
ProofScript
.
json_of_result
(
VCS
.
Why3
prover
)
result
ProofScript
.
json_of_result
(
VCS
.
Why3
prover
)
result
|>
Json
.
save_file
file
|>
Json
.
save_file
file
...
@@ -211,26 +227,29 @@ let set_cache_result ~mode hash prover result =
...
@@ -211,26 +227,29 @@ let set_cache_result ~mode hash prover result =
let
cleanup_cache
()
=
let
cleanup_cache
()
=
let
mode
=
get_mode
()
in
let
mode
=
get_mode
()
in
if
mode
=
Cleanup
&&
(
!
hits
>
0
||
!
miss
>
0
)
then
if
mode
=
Cleanup
&&
(
!
hits
>
0
||
!
miss
>
0
)
then
let
dir
=
get_dir
()
in
try
if
is_global_cache
()
the
n
let
dir
=
get_usable_dir
()
i
n
Wp_parameters
.
warning
~
current
:
false
~
once
:
true
if
is_global_cache
()
then
"Cleanup mode deactivated with global cache."
Wp_parameters
.
warning
~
current
:
false
~
once
:
true
else
"Cleanup mode deactivated with global cache."
try
else
if
Sys
.
file_exists
dir
&&
Sys
.
is_directory
dir
then
Array
.
iter
Array
.
iter
(
fun
f
->
(
fun
f
->
if
Filename
.
check_suffix
f
".json"
then
if
Filename
.
ch
eck
_suffix
f
".json"
the
n
let
hash
=
Filename
.
ch
op
_suffix
f
".json"
i
n
let
hash
=
Filename
.
chop_suffix
f
".json"
i
n
if
not
(
Hashtbl
.
mem
cleanup
hash
)
the
n
if
not
(
Hashtbl
.
mem
cleanup
hash
)
the
n
begi
n
begin
incr
removed
;
incr
removed
;
Extlib
.
safe_remove
(
Printf
.
sprintf
"%s/%s"
dir
f
)
;
Extlib
.
safe_remove
(
Printf
.
sprintf
"%s/%s"
dir
f
)
;
end
end
)
(
Sys
.
readdir
dir
)
;
)
(
Sys
.
readdir
dir
)
;
with
with
Unix
.
Unix_error
_
as
exn
->
|
Unix
.
Unix_error
_
as
exn
->
Wp_parameters
.
warning
~
current
:
false
Wp_parameters
.
warning
~
current
:
false
"Can not cleanup cache (%s)"
(
Printexc
.
to_string
exn
)
"Can not cleanup cache (%s)"
(
Printexc
.
to_string
exn
)
|
Not_found
->
Wp_parameters
.
warning
~
current
:
false
"Cannot cleanup cache"
type
runner
=
type
runner
=
timeout
:
int
option
->
steplimit
:
int
option
->
timeout
:
int
option
->
steplimit
:
int
option
->
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment