solvuu / phat

Strongly typed file path and file system operations.
ISC License
27 stars 4 forks source link

check for cycles #4

Open agarwal opened 9 years ago

agarwal commented 9 years ago

Symbolic links lead to the possibility of cycles. Cycles are not necessarily wrong, so we don't consider them ill-formed at construction time. However, some operations will lead to an infinite loop, so we need to check for them in:

pveber commented 8 years ago

Indeed not all loops are a problem. If we view a one-step resolution of a path (choose a link, and replace it by its target) as a rewriting, then we have a problem with paths such that there is no finite sequence of rewritings that leads to a link-free path. In 8f1749f we detect such cases at link creation and define them as broken links. Note that the detection is easy because all rewriting sequences are confluent.

As a result, resolve is now cycle-safe (normalize was safe to begin with because we don't normalize the target of a link), as well as typ_of and equal.

As for reify and fold, that's a different story since we have to "discover" a path and build it incrementally.

agarwal commented 8 years ago

Can you give examples of links that are supposed to be ruled out by 8f1749f1db2ab48685cd83e612ffed5afff81f93. I considered that x in the following two cases might be, but both return `Ok.

utop # let x = Item.link (name_exn "foo") (Item (Item.file (name_exn "foo")));;
val x : [ `Broken of (rel, link) item | `Ok of (rel, file) item ] =
  `Ok (Link ("foo", Item (File "foo")))
utop # let l =
  match Item.link (name_exn "foo") (Item (Item.file (name_exn "bar"))) with
  | `Broken _ -> assert false
  | `Ok x -> x;;
val l : (rel, file) item = Link ("foo", Item (File "bar"))

utop # let x = Item.link (name_exn "foo") (Item l);;
val x : [ `Broken of (rel, link) item | `Ok of (rel, file) item ] =                             
  `Ok (Link ("foo", Item (Link ("foo", Item (File "bar")))))
pveber commented 8 years ago

These examples are not cyclic but certainly wrong since they imply the existence of two different objects with the same path. However I think this verification is more on of the filesystem duty, isn't it? At the very least in both cases you can eventually resolve the links to a file, the only problem is that you can't build a tree directory with those paths.

What I mean by cyclic in this issue really boils down to cyclic ocaml values.

pveber commented 8 years ago

See the commit above, saying:

we adopt the simple (and more common) design where paths which are cyclic ocaml values are not supported and not checked. In particular, some functions may not terminate when called with such values.

This answers issue #4, which dealt with possible non termination of functions of the pure library: all legal paths are acyclic ocaml values, and as our functions on Path.t values in the pure library simply traverse them, there is no risk of infinite loop, hence no particular precaution to take.

Note that there is no danger of non-termination when dealing with the file system either:

agarwal commented 8 years ago

IIUC correctly, you are saying we entirely can do away with our own logic for testing for cycles, except indirectly by outsourcing the work to a system call that figures it out for us. Can you confirm. If so, I can close this issue.

pveber commented 8 years ago

Comment from 1d80c25:

"By merging this branch, we have implementations for [reify] and [fold] that can cope with cycles. The first one does so by counting on the file system to detect cases where a step-by-step discovery of link targets would loop forever; the second one uses [reify] and a set of visited nodes to avoid infinite loops."