/*

 * Solaris X consolidation configuration for Parfait static analysis

 * This file provides additional information about functions that Parfait

 * can use to make more accurate analysis.

 */

/*

 * Copyright (c) 2012, 2015, Oracle and/or its affiliates. All rights reserved.

 *

 * Permission is hereby granted, free of charge, to any person obtaining a

 * copy of this software and associated documentation files (the "Software"),

 * to deal in the Software without restriction, including without limitation

 * the rights to use, copy, modify, merge, publish, distribute, sublicense,

 * and/or sell copies of the Software, and to permit persons to whom the

 * Software is furnished to do so, subject to the following conditions:

 *

 * The above copyright notice and this permission notice (including the next

 * paragraph) shall be included in all copies or substantial portions of the

 * Software.

 *

 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR

 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,

 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.  IN NO EVENT SHALL

 * THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER

 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING

 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER

 * DEALINGS IN THE SOFTWARE.

 */

include 'std.conf';

/* Define custom bug types for common precondition assertions */

bugtype "null-pointer-deref-call-X"(ptr) : "null-pointer-deref" {

   name="Null Pointer Dereference in X function";

   priority="error";

   enabled="true";

   message="Null pointer dereference in call to ", callee_name(), ". Pointer ", name(ptr), " may be dereferenced";

}

bugtype "unchecked-result-call-X"(val) : "unchecked-result" {

   name="Unchecked result";

   priority="error";

   enabled="true";

   message="Unchecked return value from call to ", callee_name(), ". Value " , name(val), " must be checked to ensure this function was successful.";

}

bugtype "pointer-size-mismatch-kernel"(ptr,size) {

   name="Pointer size mismatch in kernel function";

   priority="error";

   enabled="true";

   message="Incorrect pointer size in call to ", callee_name(), ". Pointer ", name(ptr), " given as size ", size;

}

/*************************************************************************

 * Client side functions

 */

/** libX11 **/

bugtype "X-resource-leak"(xid) {

    name="X Resource Leak";

    priority="error";

    enabled="true";

    message="Leaked X Resource ", name(xid);

}

resource <x-resource> {

    name="X Resource";

    "X-resource-leak"(resource): noleak(resource);

    resource == 0 => !isa(resource);

}

/* Listed pretty much in same order as <X11/Xlib.h> */

/* Todo: XLoadQueryFont...XNewModifiermap */

XCreateImage(const display, v, dp, f, o, data, w, h, bp, bpl) {

    "null-pointer-deref-call-X"(display) : display != 0;

    if (result != 0) {

        result == new(undefined);

        may_write(result);

        escape(data);

    }

}

XDestroyImage(p) { /* actually in <X11/Xutil.h> */

    "null-pointer-deref-call-X"(p) : p != 0;

    delete(p);

}

/* Todo: XInitImage, XGetImage, XGetSubImage */

XOpenDisplay(const d) : noescape {

    "unchecked-result-call-X"(result): is_checked(result);

    if (result != 0) {

        result == new(size(*result));

        may_write(result);

    }

}

XFetchBuffer(d, n, b) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "null-pointer-deref-call-X"(n) : n != 0;

    if (result != 0) {

        *n == size(result);

        result == new(*n);

        may_write(result);

    }

}

XFetchBytes(d, n) : XFetchBuffer(d, n, 0);

XGetAtomName(d, a) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    if (result != 0) {

        result == new(undefined);

        may_write(result);

    }

}

/* Todo: XGetAtomNames, XGetDefault, XDisplayName, XKeysymToString,

   XInternAtom, XInternAtoms */

XCopyColormapAndFree(d, c) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

XCreateColormap(d, w, v, a) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

XCreatePixmapCursor(d, s, m, fg, bg, x, y) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

XCreateGlyphCursor(d, sf, mf, sc, mc, fg, bg) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

XCreateFontCursor(d, s) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

XLoadFont(d, const c) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

XCreateGC(d, dr, const vm, v) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    if (result != 0) {

        result == new(112); /* sizeof(struct _XGC) */

        may_write(result);

    } else {

        @errno != 0;

    }

}

/* Todo: XGContextFromGC, XFlushGC */

XCreatePixmap(d, dr, w, h, dp) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

XCreateBitmapFromData(d, dr, dt, w, h) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    if (result != 0) {

        init<x-resource>(result);

    } else {

        @errno != 0;

    }

}

XCreatePixmapFromBitmapData(d, dr, dt, w, h, fg, bg, dp) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    if (result != 0) {

        init<x-resource>(result);

    } else {

        @errno != 0;

    }

}

XCreateSimpleWindow(d,p,x,y,w,h,bw,b,bg) {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

/* Todo: XGetSelectionOwner */

XCreateWindow(d,p,x,y,w,h,bw,dp,c,v,const vm,a) {

    "null-pointer-deref-call-X"(d) : d != 0;

    result != 0;

    init<x-resource>(result);

}

/* Todo: XListInstalledColormaps, XListFonts, XListFontsWithInfo, XGetFontPath */

XListExtensions(d, n) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "null-pointer-deref-call-X"(n) : n != 0;

    if (result != 0) {

        result == new(undefined); /* n * char* + extension strings */

        may_write(n);

        may_write(result);

    }

}

XListProperties(d, w, n) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    if (result != 0) {

        result == new(n * 4);

        may_write(n);

        may_write(result);

    }

}

XListHosts(d, n, enabled) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    if (result != 0) {

        result == new(undefined); /* n * char* + host strings */

        may_write(n);

        may_write(enabled);

        may_write(result);

    }

}

XKeycodeToKeysym(d, k, i) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

}

XLookupKeysym(e, const i) : noescape {

    "null-pointer-deref-call-X"(e) : e != 0;

}

XGetKeyboardMapping(d, fk, kc, ks) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "null-pointer-deref-call-X"(ks) : ks != 0;

    if (result != 0) {

        result == new(kc * ks);

        may_write(ks);

        may_write(result);

    }

}

XStringToKeysym(const s) : noescape {

    "null-pointer-deref-call-X"(s) : s != 0;

}

XMaxRequestSize(const d) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

}

XExtendedMaxRequestSize(const d) : XMaxRequestSize(d);

XScreenResourceString(const s) : noescape {

    "null-pointer-deref-call-X"(s) : s != 0;

}

XDisplayMotionBufferSize(const d) : XMaxRequestSize(d);

XVisualIdFromVisual(v) : noescape {

    /* Todo: visual resource id? */

    "null-pointer-deref-call-X"(v) : v != 0;

}

XLockDisplay(d) : XMaxRequestSize(d);

XUnlockDisplay(d) : XMaxRequestSize(d);

XAddExtension(d) {

    "null-pointer-deref-call-X"(d) : d != 0;

    if (result != 0) {

        result == new(size(*result));

        may_write(result);

        escape(result);

    }

}

XInitExtension(d, const n) : XAddExtension(d);

XFindOnExtensionList(s, n) {

    "null-pointer-deref-call-X"(s) : s != 0;

}

/* these are routines for which there are also macros */

XDefaultRootWindow(const d) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

}

XRootWindow(const d, const n) : XDefaultRootWindow(d);

XRootWindowOfScreen(const s) : XDefaultRootWindow(s);

XDefaultVisual(const d, const n) : XDefaultRootWindow(d);

XDefaultVisualOfScreen(const s) : XDefaultRootWindow(s);

XDefaultGC(const d, const n) : XDefaultRootWindow(d);

XDefaultGCOfScreen(const s) : XDefaultRootWindow(s);

XBlackPixel(const d, const n) : XDefaultRootWindow(d);

XWhitePixel(const d, const n) : XDefaultRootWindow(d);

XBlackPixelOfScreen(const s) : XDefaultRootWindow(s);

XWhitePixelOfScreen(const s) : XDefaultRootWindow(s);

XNextRequest(const d) : XDefaultRootWindow(d);

XLastKnownRequestProcessed(const d) : XDefaultRootWindow(d);

XServerVendor(const d) : XDefaultRootWindow(d);

XDisplayString(const d) : XDefaultRootWindow(d);

XDefaultColormap(const d, const n) : noescape {

    /* Todo: colormap resource id? */

    "null-pointer-deref-call-X"(d) : d != 0;

}

XDefaultColormapOfScreen(const s) : XDefaultColormap(s, 0);

XDisplayOfScreen(const s) : XDefaultRootWindow(s);

XScreenOfDisplay(const d, const n) : XDefaultRootWindow(d);

XDefaultScreenOfDisplay(const d) : XDefaultRootWindow(d);

XEventMaskOfScreen(const s) : XDefaultRootWindow(s);

XScreenNumberOfScreen(const s) : XDefaultRootWindow(s);

/* Todo: XSetErrorHandler, XSetIOErrorHandler */

XListPixmapFormats(d, c) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "null-pointer-deref-call-X"(c) : c != 0;

    if (result != 0) {

        result == new(c * 12);  /* sizeof(XPixmapFormatValues) */

        may_write(c);

        may_write(result);

    } else {

        @errno != 0;

    }

}

XListDepths(d, s, c) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "null-pointer-deref-call-X"(c) : c != 0;

    if (result != 0) {

        result == new(c * 4);  /* sizeof(int) */

        may_write(c);

        may_write(result);

    } else {

        @errno != 0;

    }

}

/* Todo: ICCCM routines - XReconfigureWMWindow...XSetWMColormapWindows,

   XSetTransientForHint */

XFreeStringList(l) : free(l);

XActivateScreenSaver(d) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

}

XAddHost(d, const h) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "null-pointer-deref-call-X"(h) : h != 0;

}

XAddHosts(d, const h, const n) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "null-pointer-deref-call-X"(h) : h != 0;

}

/* Todo: XAddToExtensionList...XClearWindow */

XCloseDisplay(d) {

    "null-pointer-deref-call-X"(d) : d != 0;

    delete(d);

}

/* Todo: XConfigureWindow...XDeleteProperty */

XDestroyWindow(d, w) {

    "null-pointer-deref-call-X"(d) : d != 0;

    destroy<x-resource>(w);

}

XDestroySubwindows(d, w) : XDestroyWindow(d, w); /* Todo: subwindows? */

/* Todo: XDoesBackingStore...XDisplayHeightMM */

XDisplayKeycodes(d, min, max) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    may_write(min);

    may_write(max);

    min >= 8;

    max <= 255;

}

/* Todo: XDisplayPlanes...XEventsQueued */

XFetchName(d, w, name) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    may_write(name);

    (result == 0) => (name == 0);

    if (name != 0) {

        name == new(undefined);

        may_write(result);

        result == 1;

    }

}

/* Todo: XFillArcs...XForceScreenSaver */

XFree(p) : free(p);

XFreeColormap(d, c) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    destroy<x-resource>(c);

}

/* Todo: XFreeColors */

XFreeCursor(d, c) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    destroy<x-resource>(c);

}

XFreeExtensionList(l) : free(l);

XFreeFont(d, f) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    destroy<x-resource>(f);

}

XFreeFontInfo(names, info, count) : noescape {

    /* Todo: free contents of names & info */

    (names != 0) => delete(names);

    (info != 0) => delete(info);

}

XFreeFontNames(l) : free(l);

XFreeFontPath(l) : free(l);

XFreeGC(d, gc) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    destroy<x-resource>(gc);

    delete(gc);

}

XFreeModifierMap(m) : free(m);

XFreePixmap(d, p) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    destroy<x-resource>(p);

}

/* Todo: XGeometry...XGetGeometry */

XGetIconName(d, w, name) : XFetchName(d, w, name);

/* Todo: XGetInputFocus...XGetTransientForHint */

XGetWindowProperty(d, w, p, lo, ll, del, rt, at, af, n, bar, prop) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "unchecked-result-call-X"(result): is_checked(result);

    result == 0 => prop != 0;

    prop == 0 => result != 0;

    if (result == 0) {

        may_write(at);

        may_write(af);

        may_write(n);

        may_write(bar);

        may_write(prop);

    }

    if (prop != 0) {

        prop == new(undefined);

        may_write(prop);

        result == 0;

    }

}

/* Todo: XGetWindowAttributes...XQueryColors */

XQueryExtension(d, const n, op, ev, er) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    may_write(op);

    may_write(ev);

    may_write(er);

    if (result != 0) {

       op >= 128;

       op <= 255;

    }

}

/* Todo: XQueryKeymap...XQueryTextExtents16 */

XQueryTree(d, w, r, p, c, nc) : noescape {

    "null-pointer-deref-call-X"(d) : d != 0;

    "null-pointer-deref-call-X"(c) : c != 0;

    may_write(r);

    may_write(p);

    may_write(c);

    may_write(nc);

    if (result != 0) {

        c == new(nc * size(w));

    }

}

/* Todo: XRaiseWindow...XRemoveFromSaveSet */

XRemoveHost(d, const h) : XAddHost(d, h);

XRemoveHosts(d, const h, const n) : XAddHosts(d, h, n);

/* Todo: XReparentWindow...XFreeEventData */

/* Allocation functions from <X11/Xutil.h> */

XAllocClassHint() : calloc(1, size(*result));

XAllocIconSize() : calloc(1, size(*result));

XAllocSizeHints() : calloc(1, size(*result));

XAllocStandardColormap() : calloc(1, size(*result));

XAllocWMHints() : calloc(1, size(*result));

/** libXt

 * Functions from Xt's Alloc.c - like libc ones, except exit on failure,

 * instead of return NULL

 */

XtAsprintf(p,const fmt,args...) : printf(fmt,args), noescape {

    *p == new(result + 1);

    strlen(*p) == result;

    may_write(*p);

}

XtMalloc(s) {

    result == new(s);

}

XtRealloc(p,s) {

    delete(p);

    result == new(s);

    result[0..(size(PRE p) < s ? size(PRE p) : s)] == PRE p[0..(size(PRE p) < s ? size(PRE p) : s)];

}

XtCalloc(n,s) {

    result == new(n*s);

    result[0 .. (n * s)] == bytes(0, (n * s));

}

XtFree(p) : free(p);

/* libXcursor private function */

XcursorScanTheme(theme, name) : noescape {

   (theme == 0 || name == 0) => result == 0;

   (result != 0 && result != 1) => init<file-ptr>(result);

}

/*************************************************************************

 * Server side functions

 */

/* include/misc.h: byte swapping */

          /* XXX - does not work! */

bugtype "wrong-size-swap"(ptr,funcsize) {

    name="Wrong size Xserver swap function used";

    priority="error";

    enabled="true";

    message="Wrong size swap function used: ", callee_name(), " expects ", funcsize, "-byte variable, got ", size(ptr),"-byte ", name(ptr), " instead.";

}

swap_uint32(x) : noescape {

    "wrong-size-swap"(x,4): size(*x) == 4;

}

swap_uint16(x) : noescape {

    "wrong-size-swap"(x,2): size(*x) == 4;

}

SwapLongs(x,count) : noescape {

    "wrong-size-swap"(x,4): size(x) == 4;