autocorres: demangle variable names better

Not perfect yet, but does fix issue VER-351.

tools/autocorres/program_info.ML

@@ -117,23 +117,24 @@ end
 
 (*
  * Demangle a name mangled by the C parser.
- *
- *    c___ret_int => c
- *    ret_eret_2 => ret2
  *)
 fun demangle_name m =
-let
-  (* Remove everything after "__". *)
-  val n = (Substring.position "__" (Substring.full m) |> fst) |> Substring.string
+  if NameGeneration.rmUScoreSafety m <> m
+  then (* ignore the "StrictC'" prefix when decoding, but we need to re-mangle it in
+        * so that the resulting name is legal in Isabelle *)
+       NameGeneration.mkIdentUScoreSafe (demangle_name (NameGeneration.rmUScoreSafety m))
+  else case NameGeneration.dest_embret (MString.mk m) of
+           (* Return variable for function f *)
+           SOME (f, n) => "ret" ^ (if n > 1 then string_of_int n else "")
+           (* Ordinary variable. Split the type suffix off if there is one. *)
+         | NONE => let
+             val delim = "___" (* NameGeneration.tag_name_with_type *)
+             val (prefix, suffix) = apply2 Substring.string (Utils.positionr delim (Substring.full m))
+             in prefix end
 
-  (* Clean up "_eret_" names. *)
-  val (_, v') = Substring.position "_eret_" (Substring.full n)
-in
-  if (Substring.isEmpty v') then
-    n
-  else
-    ("ret" ^ ((Substring.taker (fn x => x <> #"_") v') |> Substring.string))
-end
+val _ = assert (demangle_name "c___ret_int" = "c") ""
+val _ = assert (demangle_name "ret_eret_2" = "ret2") ""
+val _ = assert (demangle_name "StrictC'__reserved___int" = "StrictC'__reserved") ""
 
 
 (*

tools/autocorres/tests/proof-tests/badnames.c

@@ -31,3 +31,7 @@ int bad_names(void)
 int bad_vars(int symbol_table) {
   return symbol_table;
 }
+
+/* Testcase for VER-351. The C parser generates some StrictC'__assert_fail_foo param names
+ * which we need to demangle carefully. */
+void __assert_fail (const char *, const char *, int, const char *);

tools/autocorres/tests/proof-tests/badnames.thy

@@ -0,0 +1,20 @@
+(*
+ * Copyright 2016, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+(*
+ * Test handling of C idents that are unusual or at risk of conflicting with other names.
+ *)
+theory badnames imports "../../AutoCorres" begin
+
+declare [[allow_underscore_idents]]
+install_C_file "badnames.c"
+autocorres "badnames.c"
+
+end

tools/autocorres/utils.ML

@@ -1002,6 +1002,21 @@ fun mk_simproc' ctxt (name : string, pats : string list, proc : Proof.context ->
  * so that user-added rules can override the built-in ones. *)
 fun get_rules ctxt = Named_Theorems.get ctxt #> rev
 
+(* As Substring.position but searches from the end *)
+fun positionr pat s = let
+  val (s0, begin0, size0) = Substring.base s
+  fun search i = if i < begin0 then
+                   (s, Substring.substring (s0, begin0 + size0, 0)) (* not found *)
+                 else if Substring.isPrefix pat (Substring.substring (s0, i, size0 - i)) then
+                   (Substring.substring (s0, begin0, i), (* found *)
+                    Substring.substring (s0, begin0 + i, size0 - i))
+                 else search (i - 1)
+  in search size0 end
+val _ = assert (apply2 Substring.string (positionr "br" (Substring.full "abracadabra"))
+                 = ("abracada", "bra")) ""
+val _ = assert (apply2 Substring.string (positionr "xx" (Substring.full "abracadabra"))
+                 = ("abracadabra", "")) ""
+
 end
 
 (* Insist the the given tactic solves a subgoal. *)